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

(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: Combined order from the following AFS and order.
MAX(x1)  =  MAX(x1)
n(x1, x2, x3)  =  n(x1, x2, x3)
0(x1)  =  0
#  =  #
+(x1, x2)  =  +(x1, x2)
1(x1)  =  1
-(x1, x2)  =  -(x1)
not(x1)  =  not
false  =  false
true  =  true
and(x1, x2)  =  and(x1)
if(x1, x2, x3)  =  if(x1, x2, x3)
ge(x1, x2)  =  ge
val(x1)  =  val(x1)
l(x1)  =  l(x1)
min(x1)  =  x1
max(x1)  =  x1
bs(x1)  =  bs(x1)
size(x1)  =  size(x1)
wb(x1)  =  wb(x1)

Lexicographic path order with status [LPO].
Precedence:

n₃ > # > ge > not > true > false > MAX₁
n₃ > 1 > ge > not > true > false > MAX₁
n₃ > if₃ > MAX₁
n₃ > bs₁ > and₁ > false > MAX₁
n₃ > bs₁ > ge > not > true > false > MAX₁
val₁ > MAX₁
l₁ > true > false > MAX₁
wb₁ > -₁ > 0 > # > ge > not > true > false > MAX₁
wb₁ > -₁ > 0 > 1 > ge > not > true > false > MAX₁
wb₁ > and₁ > false > MAX₁
wb₁ > if₃ > MAX₁
wb₁ > size₁ > +₂ > 0 > # > ge > not > true > false > MAX₁
wb₁ > size₁ > +₂ > 0 > 1 > ge > not > true > false > MAX₁

Status:

MAX₁: [1]
n₃: [1,2,3]
0: []
#: []
+₂: [2,1]
1: []
-₁: [1]
not: []
false: []
true: []
and₁: [1]
if₃: [1,2,3]
ge: []
val₁: [1]
l₁: [1]
bs₁: [1]
size₁: [1]
wb₁: [1]

The following usable rules [FROCOS05] were oriented:

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

(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: Combined order from the following AFS and order.
MIN(x1)  =  MIN(x1)
n(x1, x2, x3)  =  n(x1, x2, x3)
0(x1)  =  0
#  =  #
+(x1, x2)  =  +(x1, x2)
1(x1)  =  1
-(x1, x2)  =  -(x1)
not(x1)  =  not
false  =  false
true  =  true
and(x1, x2)  =  and(x1)
if(x1, x2, x3)  =  if(x1, x2, x3)
ge(x1, x2)  =  ge
val(x1)  =  val(x1)
l(x1)  =  l(x1)
min(x1)  =  x1
max(x1)  =  x1
bs(x1)  =  bs(x1)
size(x1)  =  size(x1)
wb(x1)  =  wb(x1)

Lexicographic path order with status [LPO].
Precedence:

n₃ > # > ge > not > true > false > MIN₁
n₃ > 1 > ge > not > true > false > MIN₁
n₃ > if₃ > MIN₁
n₃ > bs₁ > and₁ > false > MIN₁
n₃ > bs₁ > ge > not > true > false > MIN₁
val₁ > MIN₁
l₁ > true > false > MIN₁
wb₁ > -₁ > 0 > # > ge > not > true > false > MIN₁
wb₁ > -₁ > 0 > 1 > ge > not > true > false > MIN₁
wb₁ > and₁ > false > MIN₁
wb₁ > if₃ > MIN₁
wb₁ > size₁ > +₂ > 0 > # > ge > not > true > false > MIN₁
wb₁ > size₁ > +₂ > 0 > 1 > ge > not > true > false > MIN₁

Status:

MIN₁: [1]
n₃: [1,2,3]
0: []
#: []
+₂: [2,1]
1: []
-₁: [1]
not: []
false: []
true: []
and₁: [1]
if₃: [1,2,3]
ge: []
val₁: [1]
l₁: [1]
bs₁: [1]
size₁: [1]
wb₁: [1]

The following usable rules [FROCOS05] were oriented:

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

(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) 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.

(17) 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.

(18) 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: Combined order from the following AFS and order.
BS(x1)  =  BS(x1)
n(x1, x2, x3)  =  n(x1, x2, x3)
0(x1)  =  0
#  =  #
+(x1, x2)  =  +(x1, x2)
1(x1)  =  1
-(x1, x2)  =  -(x1)
not(x1)  =  not
false  =  false
true  =  true
and(x1, x2)  =  and(x1)
if(x1, x2, x3)  =  if(x1, x2, x3)
ge(x1, x2)  =  ge
val(x1)  =  val(x1)
l(x1)  =  l(x1)
min(x1)  =  x1
max(x1)  =  x1
bs(x1)  =  bs(x1)
size(x1)  =  size(x1)
wb(x1)  =  wb(x1)

Lexicographic path order with status [LPO].
Precedence:

n₃ > +₂ > 0 > # > false > BS₁
n₃ > +₂ > 0 > # > true > BS₁
n₃ > +₂ > 0 > 1 > false > BS₁
n₃ > ge > # > false > BS₁
n₃ > ge > # > true > BS₁
n₃ > ge > not > false > BS₁
n₃ > ge > not > true > BS₁
n₃ > wb₁ > -₁ > 0 > # > false > BS₁
n₃ > wb₁ > -₁ > 0 > # > true > BS₁
n₃ > wb₁ > -₁ > 0 > 1 > false > BS₁
n₃ > wb₁ > and₁ > false > BS₁
n₃ > wb₁ > if₃ > BS₁
n₃ > wb₁ > size₁ > # > false > BS₁
n₃ > wb₁ > size₁ > # > true > BS₁
n₃ > wb₁ > size₁ > 1 > false > BS₁
val₁ > BS₁
l₁ > BS₁
bs₁ > and₁ > false > BS₁
bs₁ > ge > # > false > BS₁
bs₁ > ge > # > true > BS₁
bs₁ > ge > not > false > BS₁
bs₁ > ge > not > true > BS₁

Status:

BS₁: [1]
n₃: [1,2,3]
0: []
#: []
+₂: [2,1]
1: []
-₁: [1]
not: []
false: []
true: []
and₁: [1]
if₃: [1,2,3]
ge: []
val₁: [1]
l₁: [1]
bs₁: [1]
size₁: [1]
wb₁: [1]

The following usable rules [FROCOS05] were oriented:

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

(19) 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.

(20) PisEmptyProof (EQUIVALENT transformation)

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

(21) TRUE

(22) 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.

(23) 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.

(24) 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.

(25) 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: Combined order from the following AFS and order.
SIZE(x1)  =  SIZE(x1)
n(x1, x2, x3)  =  n(x1, x2, x3)
0(x1)  =  0
#  =  #
+(x1, x2)  =  +(x1, x2)
1(x1)  =  1
-(x1, x2)  =  -(x1)
not(x1)  =  not
false  =  false
true  =  true
and(x1, x2)  =  and(x1)
if(x1, x2, x3)  =  if(x1, x2, x3)
ge(x1, x2)  =  ge
val(x1)  =  val(x1)
l(x1)  =  l(x1)
min(x1)  =  x1
max(x1)  =  x1
bs(x1)  =  bs(x1)
size(x1)  =  size(x1)
wb(x1)  =  wb(x1)

Lexicographic path order with status [LPO].
Precedence:

n₃ > +₂ > 0 > # > false > SIZE₁
n₃ > +₂ > 0 > # > true > SIZE₁
n₃ > +₂ > 0 > 1 > false > SIZE₁
n₃ > ge > # > false > SIZE₁
n₃ > ge > # > true > SIZE₁
n₃ > ge > not > false > SIZE₁
n₃ > ge > not > true > SIZE₁
n₃ > wb₁ > -₁ > 0 > # > false > SIZE₁
n₃ > wb₁ > -₁ > 0 > # > true > SIZE₁
n₃ > wb₁ > -₁ > 0 > 1 > false > SIZE₁
n₃ > wb₁ > and₁ > false > SIZE₁
n₃ > wb₁ > if₃ > SIZE₁
n₃ > wb₁ > size₁ > # > false > SIZE₁
n₃ > wb₁ > size₁ > # > true > SIZE₁
n₃ > wb₁ > size₁ > 1 > false > SIZE₁
val₁ > SIZE₁
l₁ > SIZE₁
bs₁ > and₁ > false > SIZE₁
bs₁ > ge > # > false > SIZE₁
bs₁ > ge > # > true > SIZE₁
bs₁ > ge > not > false > SIZE₁
bs₁ > ge > not > true > SIZE₁

Status:

SIZE₁: [1]
n₃: [1,2,3]
0: []
#: []
+₂: [2,1]
1: []
-₁: [1]
not: []
false: []
true: []
and₁: [1]
if₃: [1,2,3]
ge: []
val₁: [1]
l₁: [1]
bs₁: [1]
size₁: [1]
wb₁: [1]

The following usable rules [FROCOS05] were oriented:

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

(26) 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.

(27) PisEmptyProof (EQUIVALENT transformation)

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

(28) TRUE

(29) 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.

(30) 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: Combined order from the following AFS and order.
WB(x1)  =  WB(x1)
n(x1, x2, x3)  =  n(x1, x2, x3)
0(x1)  =  0
#  =  #
+(x1, x2)  =  +(x1, x2)
1(x1)  =  1
-(x1, x2)  =  -(x1)
not(x1)  =  not
false  =  false
true  =  true
and(x1, x2)  =  and(x1)
if(x1, x2, x3)  =  if(x1, x2, x3)
ge(x1, x2)  =  ge
val(x1)  =  val(x1)
l(x1)  =  l(x1)
min(x1)  =  x1
max(x1)  =  x1
bs(x1)  =  bs(x1)
size(x1)  =  size(x1)
wb(x1)  =  wb(x1)

Lexicographic path order with status [LPO].
Precedence:

n₃ > +₂ > 0 > # > false > WB₁
n₃ > +₂ > 0 > # > true > WB₁
n₃ > +₂ > 0 > 1 > false > WB₁
n₃ > ge > # > false > WB₁
n₃ > ge > # > true > WB₁
n₃ > ge > not > false > WB₁
n₃ > ge > not > true > WB₁
n₃ > wb₁ > -₁ > 0 > # > false > WB₁
n₃ > wb₁ > -₁ > 0 > # > true > WB₁
n₃ > wb₁ > -₁ > 0 > 1 > false > WB₁
n₃ > wb₁ > and₁ > false > WB₁
n₃ > wb₁ > if₃ > WB₁
n₃ > wb₁ > size₁ > # > false > WB₁
n₃ > wb₁ > size₁ > # > true > WB₁
n₃ > wb₁ > size₁ > 1 > false > WB₁
val₁ > WB₁
l₁ > WB₁
bs₁ > and₁ > false > WB₁
bs₁ > ge > # > false > WB₁
bs₁ > ge > # > true > WB₁
bs₁ > ge > not > false > WB₁
bs₁ > ge > not > true > WB₁

Status:

WB₁: [1]
n₃: [1,2,3]
0: []
#: []
+₂: [2,1]
1: []
-₁: [1]
not: []
false: []
true: []
and₁: [1]
if₃: [1,2,3]
ge: []
val₁: [1]
l₁: [1]
bs₁: [1]
size₁: [1]
wb₁: [1]

The following usable rules [FROCOS05] were oriented:

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

(31) 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.

(32) PisEmptyProof (EQUIVALENT transformation)

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

(33) TRUE