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

The program

(from AG01 3.38)
(VAR x y l)
(RULES
rev(nil) -> nil
rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
rev1(0,nil) -> 0
rev1(s(x),nil) -> s(x)
rev1(x,cons(y,l)) -> rev1(y,l)
rev2(x,nil) -> nil
rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend