/home/nowonder/forschung/aprove/TPDB05/TRS/uncurried/D33/02.trs

The program


(VAR x y z)

(RULES
 .(1,x) -> x
 .(x,1) -> x
 .(i(x),x) -> 1
 .(x,i(x)) -> 1
 i(1) -> 1
 i(i(x)) -> x
 .(i(y),.(y,z)) -> z
 .(y,.(i(y),z)) -> z
)

(COMMENT Example 2 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend