/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/AG01/#4.12a.trs

The program

(from AG01 4.12a)
(VAR x y)
(RULES
h(x,y) -> f(x,y,x)
f(0,1,x) -> h(x,x)
g(x,y) -> x
g(x,y) -> y
)


Submit to AProVE Web Frontend

Edit in AProVE Web Frontend