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

The program

(from AG01 4.33)
(VAR m n x y)
(RULES
sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y))
sum(cons(0,x),y) -> sum(x,y)
sum(nil,y) -> y
weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0,x)))
weight(cons(n,nil)) -> n
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend