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

The program

(VAR x y)
(RULES
g(f(x,y)) -> f(f(g(g(x)),g(g(y))),f(g(g(x)),g(g(y))))
)
(COMMENT Example 4.54 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend