/home/nowonder/forschung/aprove/TPDB05/TRS/AG01/#4.15.trs

The program

(from AG01 4.15)
(VAR x y z)
(RULES
f(0,1,g(x,y),z) -> f(g(x,y),g(x,y),g(x,y),h(x))
g(0,1) -> 0
g(0,1) -> 1
h(g(x,y)) -> h(x)
)
(STRATEGY INNERMOST)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend