Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following 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)))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(0(x), 0(y)) → 0¹(+(x, y))
+¹(0(x), 0(y)) → +¹(x, y)
+¹(0(x), 1(y)) → +¹(x, y)
+¹(1(x), 0(y)) → +¹(x, y)
+¹(1(x), 1(y)) → 0¹(+(+(x, y), 1(#)))
+¹(1(x), 1(y)) → +¹(+(x, y), 1(#))
+¹(1(x), 1(y)) → +¹(x, y)
+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)
-¹(0(x), 0(y)) → 0¹(-(x, y))
-¹(0(x), 0(y)) → -¹(x, y)
-¹(0(x), 1(y)) → -¹(-(x, y), 1(#))
-¹(0(x), 1(y)) → -¹(x, y)
-¹(1(x), 0(y)) → -¹(x, y)
-¹(1(x), 1(y)) → 0¹(-(x, y))
-¹(1(x), 1(y)) → -¹(x, y)
GE(0(x), 0(y)) → GE(x, y)
GE(0(x), 1(y)) → NOT(ge(y, x))
GE(0(x), 1(y)) → GE(y, x)
GE(1(x), 0(y)) → GE(x, y)
GE(1(x), 1(y)) → GE(x, y)
GE(#, 0(x)) → GE(#, x)
MIN(n(x, y, z)) → MIN(y)
MAX(n(x, y, z)) → MAX(z)
BS(n(x, y, z)) → AND(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
BS(n(x, y, z)) → AND(ge(x, max(y)), ge(min(z), x))
BS(n(x, y, z)) → GE(x, max(y))
BS(n(x, y, z)) → MAX(y)
BS(n(x, y, z)) → GE(min(z), x)
BS(n(x, y, z)) → MIN(z)
BS(n(x, y, z)) → AND(bs(y), bs(z))
BS(n(x, y, z)) → BS(y)
BS(n(x, y, z)) → BS(z)
SIZE(n(x, y, z)) → +¹(+(size(x), size(y)), 1(#))
SIZE(n(x, y, z)) → +¹(size(x), size(y))
SIZE(n(x, y, z)) → SIZE(x)
SIZE(n(x, y, z)) → SIZE(y)
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)))
WB(n(x, y, z)) → IF(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y))))
WB(n(x, y, z)) → GE(size(y), size(z))
WB(n(x, y, z)) → SIZE(y)
WB(n(x, y, z)) → SIZE(z)
WB(n(x, y, z)) → GE(1(#), -(size(y), size(z)))
WB(n(x, y, z)) → -¹(size(y), size(z))
WB(n(x, y, z)) → GE(1(#), -(size(z), size(y)))
WB(n(x, y, z)) → -¹(size(z), size(y))
WB(n(x, y, z)) → AND(wb(y), wb(z))
WB(n(x, y, z)) → WB(y)
WB(n(x, y, z)) → WB(z)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 9 SCCs with 24 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MAX(n(x, y, z)) → MAX(z)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MAX(n(x, y, z)) → MAX(z)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
MAX(x0, x1)  =  MAX(x1)

Tags:
MAX has argument tags [1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(MAX(x₁)) = 0   
POL(n(x₁, x₂, x₃)) = 1 + x₃   

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(9) TRUE

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MIN(n(x, y, z)) → MIN(y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MIN(n(x, y, z)) → MIN(y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
MIN(x0, x1)  =  MIN(x1)

Tags:
MIN has argument tags [1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(MIN(x₁)) = 0   
POL(n(x₁, x₂, x₃)) = 1 + x₂   

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(14) TRUE

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(#, 0(x)) → GE(#, x)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(#, 0(x)) → GE(#, x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2)  =  GE(x2)

Tags:
GE has argument tags [0,3,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 1   
POL(0(x₁)) = 1 + x₁   
POL(GE(x₁, x₂)) = x₁   

The following usable rules [FROCOS05] were oriented: none

(17) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(19) TRUE

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)
GE(1(x), 1(y)) → GE(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(1(x), 1(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2)  =  GE(x1, x2)

Tags:
GE has argument tags [1,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   
POL(GE(x₁, x₂)) = 0   

The following usable rules [FROCOS05] were oriented: none

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(0(x), 1(y)) → GE(y, x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2)  =  GE(x1, x2)

Tags:
GE has argument tags [2,1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   
POL(GE(x₁, x₂)) = 1   

The following usable rules [FROCOS05] were oriented: none

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(0(x), 0(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2)  =  GE(x1)

Tags:
GE has argument tags [2,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0(x₁)) = 1 + x₁   
POL(1(x₁)) = x₁   
POL(GE(x₁, x₂)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented: none

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(1(x), 0(y)) → GE(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(1(x), 0(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2)  =  GE(x1)

Tags:
GE has argument tags [3,3,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0(x₁)) = 0   
POL(1(x₁)) = 1 + x₁   
POL(GE(x₁, x₂)) = 0   

The following usable rules [FROCOS05] were oriented: none

(28) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(30) TRUE

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BS(n(x, y, z)) → BS(z)
BS(n(x, y, z)) → BS(y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(32) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

BS(n(x, y, z)) → BS(z)
BS(n(x, y, z)) → BS(y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
BS(x0, x1)  =  BS(x1)

Tags:
BS has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(BS(x₁)) = 0   
POL(n(x₁, x₂, x₃)) = 1 + x₂ + x₃   

The following usable rules [FROCOS05] were oriented: none

(33) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(34) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(35) TRUE

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-¹(0(x), 1(y)) → -¹(-(x, y), 1(#))
-¹(0(x), 1(y)) → -¹(x, y)
-¹(0(x), 0(y)) → -¹(x, y)
-¹(1(x), 0(y)) → -¹(x, y)
-¹(1(x), 1(y)) → -¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(37) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(0(x), 1(y)) → -¹(x, y)
-¹(1(x), 1(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2)  =  -¹(x0, x2)

Tags:
-¹ has argument tags [2,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(-(x₁, x₂)) = 0   
POL(-¹(x₁, x₂)) = 1 + x₂   
POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented: none

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-¹(0(x), 1(y)) → -¹(-(x, y), 1(#))
-¹(0(x), 0(y)) → -¹(x, y)
-¹(1(x), 0(y)) → -¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(39) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(40) Complex Obligation (AND)

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-¹(0(x), 1(y)) → -¹(-(x, y), 1(#))

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(0(x), 1(y)) → -¹(-(x, y), 1(#))

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2)  =  -¹(x1)

Tags:
-¹ has argument tags [0,0,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(-(x₁, x₂)) = x₁   
POL(-¹(x₁, x₂)) = 1 + x₂   
POL(0(x₁)) = 1 + x₁   
POL(1(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented: none

(43) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(44) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(45) TRUE

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-¹(1(x), 0(y)) → -¹(x, y)
-¹(0(x), 0(y)) → -¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(47) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(1(x), 0(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2)  =  -¹(x0, x2)

Tags:
-¹ has argument tags [0,3,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(-¹(x₁, x₂)) = x₁ + x₂   
POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented: none

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-¹(0(x), 0(y)) → -¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(0(x), 0(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2)  =  -¹(x0, x1, x2)

Tags:
-¹ has argument tags [2,3,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(-¹(x₁, x₂)) = 1   
POL(0(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented: none

(50) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(51) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(52) TRUE

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(0(x), 1(y)) → +¹(x, y)
+¹(0(x), 0(y)) → +¹(x, y)
+¹(1(x), 0(y)) → +¹(x, y)
+¹(1(x), 1(y)) → +¹(+(x, y), 1(#))
+¹(1(x), 1(y)) → +¹(x, y)
+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(0(x), 1(y)) → +¹(x, y)
+¹(1(x), 1(y)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2)  =  +¹(x2)

Tags:
+¹ has argument tags [1,2,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(+¹(x₁, x₂)) = 0   
POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented: none

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(0(x), 0(y)) → +¹(x, y)
+¹(1(x), 0(y)) → +¹(x, y)
+¹(1(x), 1(y)) → +¹(+(x, y), 1(#))
+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(56) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(57) Complex Obligation (AND)

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(1(x), 1(y)) → +¹(+(x, y), 1(#))

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(59) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(1(x), 1(y)) → +¹(+(x, y), 1(#))

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2)  =  +¹(x0)

Tags:
+¹ has argument tags [3,3,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(+¹(x₁, x₂)) = x₁ + x₂   
POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented:

+(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)
0(#) → #

(60) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(61) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(62) TRUE

(63) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(1(x), 0(y)) → +¹(x, y)
+¹(0(x), 0(y)) → +¹(x, y)
+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(64) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(1(x), 0(y)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2)  =  +¹(x0, x1, x2)

Tags:
+¹ has argument tags [0,0,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(+¹(x₁, x₂)) = x₁ + x₂   
POL(0(x₁)) = x₁   
POL(1(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] were oriented:

+(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)
0(#) → #

(65) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(0(x), 0(y)) → +¹(x, y)
+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(66) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(0(x), 0(y)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2)  =  +¹(x2)

Tags:
+¹ has argument tags [0,0,2] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 1   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(+¹(x₁, x₂)) = 0   
POL(0(x₁)) = 1 + x₁   
POL(1(x₁)) = x₁   

The following usable rules [FROCOS05] were oriented: none

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(68) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(x, +(y, z)) → +¹(+(x, y), z)
+¹(x, +(y, z)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2)  =  +¹(x2)

Tags:
+¹ has argument tags [3,3,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(#) = 0   
POL(+(x₁, x₂)) = 1 + x₁ + x₂   
POL(+¹(x₁, x₂)) = x₁   
POL(0(x₁)) = 0   
POL(1(x₁)) = 0   

The following usable rules [FROCOS05] were oriented:

+(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)
0(#) → #

(69) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(70) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(71) TRUE

(72) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SIZE(n(x, y, z)) → SIZE(y)
SIZE(n(x, y, z)) → SIZE(x)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(73) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SIZE(n(x, y, z)) → SIZE(y)
SIZE(n(x, y, z)) → SIZE(x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
SIZE(x0, x1)  =  SIZE(x1)

Tags:
SIZE has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(SIZE(x₁)) = 0   
POL(n(x₁, x₂, x₃)) = 1 + x₁ + x₂   

The following usable rules [FROCOS05] were oriented: none

(74) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(75) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(76) TRUE

(77) Obligation:

Q DP problem:
The TRS P consists of the following rules:

WB(n(x, y, z)) → WB(z)
WB(n(x, y, z)) → WB(y)

The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(78) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

WB(n(x, y, z)) → WB(z)
WB(n(x, y, z)) → WB(y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
WB(x0, x1)  =  WB(x1)

Tags:
WB has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(WB(x₁)) = 0   
POL(n(x₁, x₂, x₃)) = 1 + x₂ + x₃   

The following usable rules [FROCOS05] were oriented: none

(79) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(80) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(81) TRUE