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