(COMMENT 

  Xavier Urbain. Modular & Incremental Automated Termination
  Proofs. Journal of Automated Reasoning

)

(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(false) -> true 
not(true) -> false 
and(x,true) -> x 
and(x,false) -> false 
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(#,1(x)) -> false 
ge(#,0(x)) -> ge(#,x) 
val(l(x)) -> x 
val(n(x,y,z)) -> x 
min(l(x)) -> x 
min(n(x,y,z)) -> min(y) 
max(l(x)) -> x 
max(n(x,y,z)) -> max(z) 
bs(l(x)) -> true 
bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) 
size(l(x)) -> 1(#) 
size(n(x,y,z)) -> +(+(size(x),size(y)),1(#)) 
wb(l(x)) -> true 
wb(n(x,y,z)) -> 
and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),
                                                                 size(y)))),
  and(wb(y),wb(z))) 


)