/home/nowonder/forschung/aprove/TPDB05/TRS/uncurried/AG01/#4.34.trs

The program

(from AG01 4.34)
(VAR x y)
(RULES
f(0) -> true
f(1) -> false
f(s(x)) -> f(x)
if(true,x,y) -> x
if(false,x,y) -> y
g(s(x),s(y)) -> if(f(x),s(x),s(y))
g(x,c(y)) -> g(x,g(s(c(y)),y)))
(STRATEGY INNERMOST)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend