/home/nowonder/forschung/aprove/TPDB05/TRS/uncurried/D33/17.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
.(.(x,y),z) -> .(x,.(y,z))
i(.(x,y)) -> .(i(y),i(x))
)

(COMMENT Example 17 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend