(VAR x y z )
(RULES 
        ++(nil, y) -> y
        ++(x, nil) -> x
        ++(.(x, y), z) -> .(x, ++(y, z))
        ++(++(x, y), z) -> ++(x, ++(y, z))
        
)