/home/nowonder/forschung/aprove/TPDB05/TRS/various/25.trs

The program

(VAR x y z)
(RULES
g(a) -> g(b)
b -> f(a,a)
f(a,a) -> g(d)
)
(COMMENT Example 5.3.21 in \cite{K00})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend