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

The program

(VAR x y)
(RULES
f(x,y) -> h(x,y)
f(x,y) -> h(y,x)
h(x,x) -> x
)
(COMMENT Example 4 (variant of TRS $\RR_2$) in \cite{O95})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend