(COMMENT 

  Xavier Urbain

  Base 2 logarithm. Integers in binary notation.

)

(VAR z  y  x)
(RULES

0(#) -> # 
+(#,x) -> x 
+(x,#) -> x 
+(0(x),0(y)) -> 0(+(x,y)) 
+(0(x),1(y)) -> 1(+(x,y)) 
+(1(x),0(y)) -> 1(+(x,y)) 
+(1(x),1(y)) -> 0(+(+(x,y),1(#))) 
+(+(x,y),z) -> +(x,+(y,z)) 
-(#,x) -> # 
-(x,#) -> x 
-(0(x),0(y)) -> 0(-(x,y)) 
-(0(x),1(y)) -> 1(-(-(x,y),1(#))) 
-(1(x),0(y)) -> 1(-(x,y)) 
-(1(x),1(y)) -> 0(-(x,y)) 
not(true) -> false 
not(false) -> true 
if(true,x,y) -> x 
if(false,x,y) -> y 
ge(0(x),0(y)) -> ge(x,y) 
ge(0(x),1(y)) -> not(ge(y,x)) 
ge(1(x),0(y)) -> ge(x,y) 
ge(1(x),1(y)) -> ge(x,y) 
ge(x,#) -> true 
ge(#,0(x)) -> ge(#,x) 
ge(#,1(x)) -> false 
log(x) -> -(log'(x),1(#)) 
log'(#) -> # 
log'(1(x)) -> +(log'(x),1(#)) 
log'(0(x)) -> if(ge(x,1(#)),+(log'(x),1(#)),#) 

)