YES
(VAR x y z)
(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)))
)

Proving termination of rewriting for tree:

-> Dependency pairs:
nF_+(0(x),0(y)) -> nF_0(+(x,y))
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(0(x),1(y)) -> nF_+(x,y)
nF_+(1(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_0(+(+(x,y),1(#)))
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(x,+(y,z)) -> nF_+(+(x,y),z)
nF_+(x,+(y,z)) -> nF_+(x,y)
nF_-(0(x),0(y)) -> nF_0(-(x,y))
nF_-(0(x),0(y)) -> nF_-(x,y)
nF_-(0(x),1(y)) -> nF_-(-(x,y),1(#))
nF_-(0(x),1(y)) -> nF_-(x,y)
nF_-(1(x),0(y)) -> nF_-(x,y)
nF_-(1(x),1(y)) -> nF_0(-(x,y))
nF_-(1(x),1(y)) -> nF_-(x,y)
nF_ge(0(x),0(y)) -> nF_ge(x,y)
nF_ge(0(x),1(y)) -> nF_not(ge(y,x))
nF_ge(0(x),1(y)) -> nF_ge(y,x)
nF_ge(1(x),0(y)) -> nF_ge(x,y)
nF_ge(1(x),1(y)) -> nF_ge(x,y)
nF_ge(#,0(x)) -> nF_ge(#,x)
nF_min(n(x,y,z)) -> nF_min(y)
nF_max(n(x,y,z)) -> nF_max(z)
nF_bs(n(x,y,z)) -> nF_and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
nF_bs(n(x,y,z)) -> nF_and(ge(x,max(y)),ge(min(z),x))
nF_bs(n(x,y,z)) -> nF_ge(x,max(y))
nF_bs(n(x,y,z)) -> nF_max(y)
nF_bs(n(x,y,z)) -> nF_ge(min(z),x)
nF_bs(n(x,y,z)) -> nF_min(z)
nF_bs(n(x,y,z)) -> nF_and(bs(y),bs(z))
nF_bs(n(x,y,z)) -> nF_bs(y)
nF_bs(n(x,y,z)) -> nF_bs(z)
nF_size(n(x,y,z)) -> nF_+(+(size(x),size(y)),1(#))
nF_size(n(x,y,z)) -> nF_+(size(x),size(y))
nF_size(n(x,y,z)) -> nF_size(x)
nF_size(n(x,y,z)) -> nF_size(y)
nF_wb(n(x,y,z)) -> nF_and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z)))
nF_wb(n(x,y,z)) -> nF_if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y))))
nF_wb(n(x,y,z)) -> nF_ge(size(y),size(z))
nF_wb(n(x,y,z)) -> nF_size(y)
nF_wb(n(x,y,z)) -> nF_size(z)
nF_wb(n(x,y,z)) -> nF_ge(1(#),-(size(y),size(z)))
nF_wb(n(x,y,z)) -> nF_-(size(y),size(z))
nF_wb(n(x,y,z)) -> nF_ge(1(#),-(size(z),size(y)))
nF_wb(n(x,y,z)) -> nF_-(size(z),size(y))
nF_wb(n(x,y,z)) -> nF_and(wb(y),wb(z))
nF_wb(n(x,y,z)) -> nF_wb(y)
nF_wb(n(x,y,z)) -> nF_wb(z)

-> Proof of termination for tree_1_1:
-> -> Dependency pairs in cycle:
nF_wb(n(x,y,z)) -> nF_wb(y)
nF_wb(n(x,y,z)) -> nF_wb(z)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_2:
-> -> Dependency pairs in cycle:
nF_size(n(x,y,z)) -> nF_size(x)
nF_size(n(x,y,z)) -> nF_size(y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_3:
-> -> Dependency pairs in cycle:
nF_bs(n(x,y,z)) -> nF_bs(y)
nF_bs(n(x,y,z)) -> nF_bs(z)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_4:
-> -> Dependency pairs in cycle:
nF_max(n(x,y,z)) -> nF_max(z)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_5:
-> -> Dependency pairs in cycle:
nF_min(n(x,y,z)) -> nF_min(y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_6:
-> -> Dependency pairs in cycle:
nF_ge(0(x),0(y)) -> nF_ge(x,y)
nF_ge(1(x),1(y)) -> nF_ge(x,y)
nF_ge(1(x),0(y)) -> nF_ge(x,y)
nF_ge(0(x),1(y)) -> nF_ge(y,x)

There are no usable rules.

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = 0
[1](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_ge](X1,X2) = X1 + X2

TIME: 5.9438e-2

-> -> Dependency pairs in cycle:
nF_ge(0(x),0(y)) -> nF_ge(x,y)
nF_ge(1(x),0(y)) -> nF_ge(x,y)
nF_ge(1(x),1(y)) -> nF_ge(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_7:
-> -> Dependency pairs in cycle:
nF_ge(#,0(x)) -> nF_ge(#,x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_8:
-> -> Dependency pairs in cycle:
nF_-(0(x),0(y)) -> nF_-(x,y)
nF_-(1(x),1(y)) -> nF_-(x,y)
nF_-(1(x),0(y)) -> nF_-(x,y)
nF_-(0(x),1(y)) -> nF_-(x,y)
nF_-(0(x),1(y)) -> nF_-(-(x,y),1(#))

UsableRules:
0(#) -> #
-(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))

Polynomial Interpretation:

[0](X) = X + 1
[#] = 1
[+](X1,X2) = 0
[1](X) = X + 1
[-](X1,X2) = X1
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_-](X1,X2) = X1

TIME: 6.1481e-2

-> -> Dependency pairs in cycle:
nF_-(0(x),0(y)) -> nF_-(x,y)
nF_-(0(x),1(y)) -> nF_-(x,y)
nF_-(1(x),0(y)) -> nF_-(x,y)
nF_-(1(x),1(y)) -> nF_-(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for tree_1_9:
-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(x,+(y,z)) -> nF_+(x,y)
nF_+(x,+(y,z)) -> nF_+(+(x,y),z)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(1(x),0(y)) -> nF_+(x,y)
nF_+(0(x),1(y)) -> nF_+(x,y)

UsableRules:
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)

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = X1 + X2
[1](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_+](X1,X2) = X2

TIME: 6.2816e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(x,+(y,z)) -> nF_+(+(x,y),z)
nF_+(x,+(y,z)) -> nF_+(x,y)

UsableRules:
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)

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = X1 + X2 + 1
[1](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_+](X1,X2) = X2

TIME: 6.1825e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(x,+(y,z)) -> nF_+(+(x,y),z)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(1(x),0(y)) -> nF_+(x,y)

UsableRules:
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)

Polynomial Interpretation:

[0](X) = X + 1
[#] = 0
[+](X1,X2) = X1 + X2
[1](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_+](X1,X2) = X2

TIME: 6.166e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(x,+(y,z)) -> nF_+(+(x,y),z)

UsableRules:
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)

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = X1 + X2 + 1
[1](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_+](X1,X2) = X2

TIME: 5.941e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))

UsableRules:
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)

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = X1 + X2
[1](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[false] = 0
[true] = 0
[and](X1,X2) = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[val](X) = 0
[l](X) = 0
[n](X1,X2,X3) = 0
[min](X) = 0
[max](X) = 0
[bs](X) = 0
[size](X) = 0
[wb](X) = 0
[nF_+](X1,X2) = X1 + X2

TIME: 4.6519e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.