(VAR x y z )
(RULES 
        .(.(x,y),z) -> .(x,.(y,z))
        a(f(x)) -> f(a(x))
        a(.(x,y)) -> .(a(x),y)
        a(b1(x)) -> b1(a(x))
        f(b(x)) -> b(f(x))
        .(b(x),y) -> b(.(x,y))
        b1(b(x)) -> b(b(x))
        a(f(.(0,x))) -> b1(.(f(.(0,x)),.(0,f(x))))
        a(f(0)) -> b1(.(f(0),0))
        f(.(0,x)) -> b(.(0,f(x)))
        f(0) -> b(0)
        c(b(x)) -> c(a(x))
        a(b(x)) -> b(a(x))
        
)