bresolve

{bresolve | :bresolve} [<limit>] [all]

Computes all possible variable assignments that render an abstracted term true. The variant with leading colon is for usage during a CITP proof. If an optional argument 'all' is specified, all solutions will be searched. Optional specifies maximal number of variable combination, i.e. if there are 3 variables v1, v2, and v3, and is 2, the following cases are examined: (1) v1 : true/false (2) v2 : true/false (3) v3 : true/false (4) v1/v2 : combinations of true/false of two variables (5) v1/v3 : combinations of true/false of two variables (6) v2/v3 : combinations of true/false of two variables

Example

CafeOBJ> bresolve 2 all

** (1) The following assignment(s) makes the term to be 'true'.
[1] { P-3:Bool |-> true }
where
  p-3 = P4(Y:S)
  
[2] { P-4:Bool |-> true }
where
  p-4 = P1(X:S)
  
** (2) The following assignment(s) makes the term to be 'true'.
[1] { P-1:Bool |-> true, P-2:Bool |-> true }
where
  p-1 = P3(Y:S)
  p-2 = P2(X:S)
...