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(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(#)),#)
)

Proving termination of rewriting for log2:

-> 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_+(y,z)
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_log(x) -> nF_-(log'(x),1(#))
nF_log(x) -> nF_log'(x)
nF_log'(1(x)) -> nF_+(log'(x),1(#))
nF_log'(1(x)) -> nF_log'(x)
nF_log'(0(x)) -> nF_if(ge(x,1(#)),+(log'(x),1(#)),#)
nF_log'(0(x)) -> nF_ge(x,1(#))
nF_log'(0(x)) -> nF_+(log'(x),1(#))
nF_log'(0(x)) -> nF_log'(x)

-> Proof of termination for log2_1_1:
-> -> Dependency pairs in cycle:
nF_log'(0(x)) -> nF_log'(x)
nF_log'(1(x)) -> nF_log'(x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for log2_1_2:
-> -> 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
[true] = 0
[false] = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[log](X) = 0
[log'](X) = 0
[nF_ge](X1,X2) = X1 + X2

TIME: 4.6313e-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 log2_1_3:
-> -> Dependency pairs in cycle:
nF_ge(#,0(x)) -> nF_ge(#,x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for log2_1_4:
-> -> 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
[true] = 0
[false] = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[log](X) = 0
[log'](X) = 0
[nF_-](X1,X2) = X1

TIME: 4.9311e-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 log2_1_5:
-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(+(x,y),z) -> nF_+(y,z)
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
[true] = 0
[false] = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[log](X) = 0
[log'](X) = 0
[nF_+](X1,X2) = X1 + X2

TIME: 4.9351000000000034e-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_+(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
[true] = 0
[false] = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[log](X) = 0
[log'](X) = 0
[nF_+](X1,X2) = X1 + X2

TIME: 4.8392e-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),1(#))
nF_+(1(x),1(y)) -> nF_+(x,y)
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
[true] = 0
[false] = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[log](X) = 0
[log'](X) = 0
[nF_+](X1,X2) = X1 + X2

TIME: 4.8213e-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](X) = X + 1
[-](X1,X2) = 0
[not](X) = 0
[true] = 0
[false] = 0
[if](X1,X2,X3) = 0
[ge](X1,X2) = 0
[log](X) = 0
[log'](X) = 0
[nF_+](X1,X2) = X1 + X2

TIME: 4.9683e-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)

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.