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

The program

(VAR x y z)
(RULES
:(:(x,y),z) -> :(x,:(y,z))
:(+(x,y),z) -> +(:(x,z),:(y,z))
:(z,+(x,f(y))) -> :(g(z,y),+(x,a))
)
(COMMENT Example 31 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend