(VAR k l x y z )
(RULES 
        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), l))
        a(h, h, x) -> s(x)
        a(x, s(y), h) -> a(x, y, s(h))
        a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
        a(s(x), h, z) -> a(x, z, z)
        
)