/home/nowonder/forschung/aprove/TPDB05/TRS/Zantema/z10.trs

The program

(VAR x y z)
(RULES
a(lambda(x),y) -> lambda(a(x,p(1,a(y,t))))
a(p(x,y),z) -> p(a(x,z),a(y,z))
a(a(x,y),z) -> a(x,a(y,z))
a(id,x) -> x
a(1,id) -> 1
a(t,id) -> t
a(1,p(x,y)) -> x
a(t,p(x,y)) -> y
)
(COMMENT termination of SUBST, see TERESE book page 248)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend