bshow

{bshow | :bshow} [{ tree | grind }]

Shows the abstracted Boolean term computed by binspect. If the argument tree is given, prints out a the abstracted term in tree form. The variant with leading colon is for usage during a CITP proof.

Example

CafeOBJ> bshow
((P-1:Bool and (P-2:Bool and (P-3:Bool and P-4:Bool))) xor ((P-1 and (P-2 and (P-4 and (P-5:Bool and P-3)))) xor ((P-2 and (P-1 and (P-5 and P-3))) xor ((P-5 and P-3) xor ((P-4 and (P-3 and P-5)) xor ((P-4 and P-3) xor (P-2 and P-1)))))))
where
  P-1:Bool |-> p4(Y:S)
  P-2:Bool |-> p1(Y:S)
  P-3:Bool |-> p3(Y:S)
  P-4:Bool |-> p1(X:S)
  P-5:Bool |-> p2(X:S)