/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.58.trs

The program

(VAR x y z)
(RULES 
f(x,g(y)) -> f(h(x),i(x,y))
i(x,j(0,0)) -> g(0)
i(x,j(y,z)) -> j(g(y),i(x,z))
i(h(x),j(j(y,z),0)) -> j(i(h(x),j(y,z)),i(x,j(y,z)))
j(g(x),g(y)) -> g(j(x,y))
)
(COMMENT Example 4.58 (Battle of Hydra and Hercules) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend