(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
)