(VAR x y z )
(RULES 
        a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
        a(p(x, y), z) -> p(a(x, z), a(y, z))
        a(a(x, y), z) -> a(x, a(y, z))
        a(id, x) -> x
        a(1, id) -> 1
        a(t, id) -> t
        a(1, p(x, y)) -> x
        a(t, p(x, y)) -> y
        
)