TRS: {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)))))} Fail