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

The program

(VAR x y z)
(RULES
and(x,false) -> false
and(x,not(false)) -> x
not(not(x)) -> x
implies(false,y) -> not(false)
implies(x,false) -> not(x)
implies(not(x),not(y)) -> implies(y,and(x,y))
)
(COMMENT Example 2.35 (Implication) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend