/home/nowonder/forschung/aprove/TPDB05/TRS/D33/20.trs

The program

(VAR x y)
(RULES
 not(not(x)) -> x
 not(or(x,y)) -> and(not(not(not(x))),not(not(not(y))))
 not(and(x,y)) -> or(not(not(not(x))),not(not(not(y))))
)

(COMMENT Example 20 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend