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

The program

(VAR x y z x1 x2 x3 x4)
(RULES
f1() -> g1()
f1() -> g2()
f2() -> g1()
f2() -> g2()
g1() -> h1()
g1() -> h2()
g2() -> h1()
g2() -> h2()
e1(h1(),h2(),x,y,z) -> e2(x,x,y,z,z)
e2(f1(),x,y,z,f2()) -> e3(x,y,x,y,y,z,y,z,x,y,z)
e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)
e4(g1(),x1,g2(),x1,g1(),x1,g2(),x1,x,y,z) -> e1(x1,x1,x,y,z)
)
(COMMENT Example 4 (variant of TRS $\RR_1$) in \cite{O95})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend