-
Notifications
You must be signed in to change notification settings - Fork 6
binspect
Norbert Preining edited this page Oct 6, 2017
·
2 revisions
Start an inspection of a Boolean term, that is, and abstracted
form of the Boolean term is constructed. The abstracted term is shown (like calling bshow
.
CafeOBJ> module BTE { [S]
preds p1 p2 p3 p4 p5 p6 p7 : S
ops a b c : -> S .
}
CafeOBJ> binspect in BTE : (p1(X:S) or p2(X)) and p3(Y:S) or (p4(Y) and p1(Y)) .
...
--> ((p4(Y:S) and p1(Y)) xor ((p3(Y) and p1(X:S)) xor ((p2(X) and (p3(Y) and p1(X))) xor ((p3(Y) and p2(X)) xor ((p3(Y) and (p2(X) and (p4(Y) and p1(Y)))) xor ((p3(Y) and (p2(X) and (p1(X) and (p1(Y) and p4(Y))))) xor (p1(X) and (p3(Y) and (p1(Y) and p4(Y))))))))))
...
CafeOBJ Reference Manual (c) 2015-2018 CafeOBJ Development Team