(VAR 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
        *(h, x) -> h
        *(x, h) -> h
        *(s(x), s(y)) -> s(+(+(*(x, y), x), y))
        
)