(COMMENT harder variant of AG01 4.33)
(VAR m n x y b)
(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
empty(nil) -> true
empty(cons(n,x)) -> false
tail(nil) -> nil
tail(cons(n,x)) -> x
head(cons(n,x)) -> n
weight(x) -> if(empty(x),empty(tail(x)),x)
if(true,b,x) -> weight_undefined_error
if(false,b,x) -> if2(b,x)
if2(true,x) -> head(x)
if2(false,x) -> weight(sum(x,cons(0,tail(tail(x)))))
)