(VAR k l x y z )
(RULES 
        a(h, h, h, x) -> s(x)
        a(l, x, s(y), h) -> a(l, x, y, s(h))
        a(l, x, s(y), s(z)) -> a(l, x, y, a(l, x, s(y), z))
        a(l, s(x), h, z) -> a(l, x, z, z)
        a(s(l), h, h, z) -> a(l, z, h, z)
        +(x, h) -> x
        +(h, x) -> x
        +(s(x), s(y)) -> s(s(+(x, y)))
        +(+(x, y), z) -> +(x, +(y, z))
        s(h) -> 1
        app(nil, k) -> k
        app(l, nil) -> l
        app(cons(x, l), k) -> cons(x, app(l, k))
        sum(cons(x, nil)) -> cons(x, nil)
        sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h, h), l))
        
)