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

The program

(VAR x)
(RULES
f(h(x)) -> f(i(x))
g(i(x)) -> g(h(x))
h(a) -> b
i(a) -> b
)
(COMMENT Example 4.44 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend