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

The program

(from AG01 3.15)
(VAR x y)
(RULES
average(s(x),y) -> average(x,s(y))
average(x,s(s(s(y)))) -> s(average(s(x),y))
average(0,0) -> 0
average(0,s(0)) -> 0
average(0,s(s(0))) -> s(0))

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend