/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/2.37.trs

The program

(VAR x y z)
(RULES
and(not(not(x)),y,not(z)) -> and(y,band(x,z),x)
)

(COMMENT Example 2.37 (Ternary And-Operator) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend