(VAR x y )
(RULES 
        suc(1) -> .0(1)
        suc(.0(x)) -> .1(x)
        suc(.1(x)) -> .0(suc(x))
        add(x,1) -> suc(x)
        add(1,y) -> suc(y)
        add(.0(x),.0(y)) -> .0(add(x,y))
        add(.1(x),.0(y)) -> .1(add(x,y))
        add(.0(x),.1(y)) -> .1(add(x,y))
        add(.1(x),.1(y)) -> .0(suc(add(x,y)))
        C(.0(x)) -> C(x)
        C(.1(x)) -> C(add(.1(x),.1(.1(x))))
        
)