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

The program

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

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend