Termination w.r.t. Q proof of /tmp/tmpmcG9uS/tree.trs

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 PisEmptyProof (⇔)

    ↳9 TRUE

  ↳10 QDP

    ↳11 QDPOrderProof (⇔)

    ↳12 QDP

    ↳13 PisEmptyProof (⇔)

    ↳14 TRUE

  ↳15 QDP

    ↳16 QDPOrderProof (⇔)

    ↳17 QDP

    ↳18 PisEmptyProof (⇔)

    ↳19 TRUE

  ↳20 QDP

    ↳21 QDPOrderProof (⇔)

    ↳22 QDP

    ↳23 QDPOrderProof (⇔)

    ↳24 QDP

    ↳25 PisEmptyProof (⇔)

    ↳26 TRUE

  ↳27 QDP

    ↳28 QDPOrderProof (⇔)

    ↳29 QDP

    ↳30 PisEmptyProof (⇔)

    ↳31 TRUE

  ↳32 QDP

    ↳33 QDPOrderProof (⇔)

    ↳34 QDP

    ↳35 QDPOrderProof (⇔)

    ↳36 QDP

  ↳37 QDP

    ↳38 QDPOrderProof (⇔)

    ↳39 QDP

    ↳40 QDPOrderProof (⇔)

    ↳41 QDP

    ↳42 DependencyGraphProof (⇔)

    ↳43 AND

      ↳44 QDP

      ↳45 QDP

        ↳46 QDPOrderProof (⇔)

        ↳47 QDP

        ↳48 QDPOrderProof (⇔)

        ↳49 QDP

        ↳50 PisEmptyProof (⇔)

        ↳51 TRUE

  ↳52 QDP

    ↳53 QDPOrderProof (⇔)

    ↳54 QDP

    ↳55 PisEmptyProof (⇔)

    ↳56 TRUE

  ↳57 QDP

    ↳58 QDPOrderProof (⇔)

    ↳59 QDP

    ↳60 PisEmptyProof (⇔)

    ↳61 TRUE

(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: Recursive Path Order [RPO].
Precedence:

n₃ > MAX₁

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: Recursive Path Order [RPO].
Precedence:

n₃ > MIN₁

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: Combined order from the following AFS and order.
GE(x1, x2) = GE(x2)
# = #
0(x1) = 0(x1)

Recursive Path Order [RPO].
Precedence:

# > GE₁
0₁ > GE₁

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(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
GE(x1, x2) = GE(x1, x2)
0(x1) = 0(x1)
1(x1) = x1

Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

(22) Obligation:

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

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.

(23) 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: Combined order from the following AFS and order.
GE(x1, x2) = x2
1(x1) = 1(x1)

Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

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

(25) PisEmptyProof (EQUIVALENT transformation)

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

(26) TRUE

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

(28) 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: Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

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

(30) PisEmptyProof (EQUIVALENT transformation)

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

(31) TRUE

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

(33) 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)
-¹(1(x), 0(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
-¹(x1, x2) = -¹(x2)
0(x1) = 0(x1)
1(x1) = x1
-(x1, x2) = -(x2)
# = #

Recursive Path Order [RPO].
Precedence:

-₁ > 0₁ > -^1₁ > #

The following usable rules [FROCOS05] were oriented: none

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

(35) 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: Combined order from the following AFS and order.
-¹(x1, x2) = -¹(x2)
0(x1) = 0
1(x1) = 1(x1)
-(x1, x2) = -
# = #

Recursive Path Order [RPO].
Precedence:

0 > -^1₁ > #
1₁ > -^1₁ > #
- > #

The following usable rules [FROCOS05] were oriented: none

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

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

(38) 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: Combined order from the following AFS and order.
+¹(x1, x2) = +¹(x2)
0(x1) = x1
1(x1) = x1
+(x1, x2) = +(x1, x2)
# = #

Recursive Path Order [RPO].
Precedence:

+₂ > +^1₁ > #

The following usable rules [FROCOS05] were oriented: none

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

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.

(40) 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: Combined order from the following AFS and order.
+¹(x1, x2) = +¹(x2)
0(x1) = x1
1(x1) = 1(x1)
+(x1, x2) = +
# = #

Recursive Path Order [RPO].
Precedence:

+ > 1₁ > +^1₁ > #

The following usable rules [FROCOS05] were oriented: none

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

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) DependencyGraphProof (EQUIVALENT transformation)

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

(43) Complex Obligation (AND)

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

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

(46) 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: Combined order from the following AFS and order.
+¹(x1, x2) = +¹(x1, x2)
1(x1) = 1(x1)
0(x1) = x1

Recursive Path Order [RPO].
Precedence:

1₁ > +^1₂

The following usable rules [FROCOS05] were oriented: none

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

(48) 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: Combined order from the following AFS and order.
+¹(x1, x2) = x2
0(x1) = 0(x1)

Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

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

(50) PisEmptyProof (EQUIVALENT transformation)

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

(51) TRUE

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

(53) 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: Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

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

(55) PisEmptyProof (EQUIVALENT transformation)

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

(56) TRUE

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

(58) 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: Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

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

(60) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) PisEmptyProof (EQUIVALENT transformation)

(9) TRUE

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) PisEmptyProof (EQUIVALENT transformation)

(14) TRUE

(15) Obligation:

(16) QDPOrderProof (EQUIVALENT transformation)

(17) Obligation:

(18) PisEmptyProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) QDPOrderProof (EQUIVALENT transformation)

(24) Obligation:

(25) PisEmptyProof (EQUIVALENT transformation)

(26) TRUE

(27) Obligation:

(28) QDPOrderProof (EQUIVALENT transformation)

(29) Obligation:

(30) PisEmptyProof (EQUIVALENT transformation)

(31) TRUE

(32) Obligation:

(33) QDPOrderProof (EQUIVALENT transformation)

(34) Obligation:

(35) QDPOrderProof (EQUIVALENT transformation)

(36) Obligation:

(37) Obligation:

(38) QDPOrderProof (EQUIVALENT transformation)

(39) Obligation:

(40) QDPOrderProof (EQUIVALENT transformation)

(41) Obligation:

(42) DependencyGraphProof (EQUIVALENT transformation)

(43) Complex Obligation (AND)

(44) Obligation:

(45) Obligation:

(46) QDPOrderProof (EQUIVALENT transformation)

(47) Obligation:

(48) QDPOrderProof (EQUIVALENT transformation)

(49) Obligation:

(50) PisEmptyProof (EQUIVALENT transformation)

(51) TRUE

(52) Obligation:

(53) QDPOrderProof (EQUIVALENT transformation)

(54) Obligation:

(55) PisEmptyProof (EQUIVALENT transformation)

(56) TRUE

(57) Obligation:

(58) QDPOrderProof (EQUIVALENT transformation)

(59) Obligation:

(60) PisEmptyProof (EQUIVALENT transformation)

(61) TRUE