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

The program

(VAR x y z)
(RULES
not(x) -> xor(x,true)
implies(x,y) -> xor(and(x,y),xor(x,true))
or(x,y) -> xor(and(x,y),xor(x,y))
=(x,y) -> xor(x,xor(y,true))
)

(COMMENT Example 2.30 (Boolean Ring) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend