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

The program

(VAR x y z)
(RULES
a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
a(u(x)) -> x
b(v(x)) -> x
c(w(x)) -> x
)
(COMMENT Example 4.32 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend