Termination w.r.t. Q proof of AProVE_07

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

0 QTRS

↳1 Overlay + Local Confluence (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QReductionProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 QDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QReductionProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 NonInfProof (⇔, 3 ms)

        ↳20 AND

            ↳21 QDP

                ↳22 NonInfProof (⇔, 0 ms)

                ↳23 AND

                    ↳24 QDP

                        ↳25 DependencyGraphProof (⇔, 0 ms)

                        ↳26 TRUE

                    ↳27 QDP

                        ↳28 DependencyGraphProof (⇔, 0 ms)

                        ↳29 TRUE

            ↳30 QDP

                ↳31 DependencyGraphProof (⇔, 0 ms)

                ↳32 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(x, 0) → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0, 0, 0)
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0, s(v))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(x, 0) → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0, 0, 0)
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0, s(v))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

LE(s(x), s(y)) → LE(x, y)
QUOT(x, s(y)) → QUOTITER(x, s(y), 0, 0, 0)
QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v)
QUOTITER(x, s(y), z, u, v) → LE(x, z)
IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
IF(false, x, y, z, u, v) → LE(y, s(u))
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(x, 0) → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0, 0, 0)
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0, s(v))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(x, 0) → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0, 0, 0)
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0, s(v))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

(11) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LE(s(x), s(y)) → LE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v)
IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(x, 0) → quotZeroErro
quot(x, s(y)) → quotIter(x, s(y), 0, 0, 0)
quotIter(x, s(y), z, u, v) → if(le(x, z), x, s(y), z, u, v)
if(true, x, y, z, u, v) → v
if(false, x, y, z, u, v) → if2(le(y, s(u)), x, y, s(z), s(u), v)
if2(false, x, y, z, u, v) → quotIter(x, y, z, u, v)
if2(true, x, y, z, u, v) → quotIter(x, y, z, 0, s(v))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

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

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

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

QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v)
IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

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

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

quot(x0, 0)
quot(x0, s(x1))
quotIter(x0, s(x1), x2, x3, x4)
if(true, x0, x1, x2, x3, x4)
if(false, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3, x4)

(18) Obligation:

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

QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v)
IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(19) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v) the following chains were created:

We consider the chain IF2(false, x10, x11, x12, x13, x14) → QUOTITER(x10, x11, x12, x13, x14), QUOTITER(x15, s(x16), x17, x18, x19) → IF(le(x15, x17), x15, s(x16), x17, x18, x19) which results in the following constraint:
(1) (QUOTITER(x10, x11, x12, x13, x14)=QUOTITER(x15, s(x16), x17, x18, x19) ⇒ QUOTITER(x15, s(x16), x17, x18, x19)≥IF(le(x15, x17), x15, s(x16), x17, x18, x19))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (QUOTITER(x10, s(x16), x12, x13, x14)≥IF(le(x10, x12), x10, s(x16), x12, x13, x14))
We consider the chain IF2(true, x20, x21, x22, x23, x24) → QUOTITER(x20, x21, x22, 0, s(x24)), QUOTITER(x25, s(x26), x27, x28, x29) → IF(le(x25, x27), x25, s(x26), x27, x28, x29) which results in the following constraint:
(1) (QUOTITER(x20, x21, x22, 0, s(x24))=QUOTITER(x25, s(x26), x27, x28, x29) ⇒ QUOTITER(x25, s(x26), x27, x28, x29)≥IF(le(x25, x27), x25, s(x26), x27, x28, x29))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (QUOTITER(x20, s(x26), x22, 0, s(x24))≥IF(le(x20, x22), x20, s(x26), x22, 0, s(x24)))

For Pair IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v) the following chains were created:

We consider the chain QUOTITER(x30, s(x31), x32, x33, x34) → IF(le(x30, x32), x30, s(x31), x32, x33, x34), IF(false, x35, x36, x37, x38, x39) → IF2(le(x36, s(x38)), x35, x36, s(x37), s(x38), x39) which results in the following constraint:

(1) (IF(le(x30, x32), x30, s(x31), x32, x33, x34)=IF(false, x35, x36, x37, x38, x39) ⇒ IF(false, x35, x36, x37, x38, x39)≥IF2(le(x36, s(x38)), x35, x36, s(x37), s(x38), x39))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:

(2) (le(x30, x32)=false ⇒ IF(false, x30, s(x31), x32, x33, x34)≥IF2(le(s(x31), s(x33)), x30, s(x31), s(x32), s(x33), x34))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x30, x32)=false which results in the following new constraints:

(3) (le(x107, x106)=false∧(∀x108,x109,x110:le(x107, x106)=false ⇒ IF(false, x107, s(x108), x106, x109, x110)≥IF2(le(s(x108), s(x109)), x107, s(x108), s(x106), s(x109), x110)) ⇒ IF(false, s(x107), s(x31), s(x106), x33, x34)≥IF2(le(s(x31), s(x33)), s(x107), s(x31), s(s(x106)), s(x33), x34))

(4) (false=false ⇒ IF(false, s(x111), s(x31), 0, x33, x34)≥IF2(le(s(x31), s(x33)), s(x111), s(x31), s(0), s(x33), x34))

We simplified constraint (3) using rule (VI) where we applied the induction hypothesis (∀x108,x109,x110:le(x107, x106)=false ⇒ IF(false, x107, s(x108), x106, x109, x110)≥IF2(le(s(x108), s(x109)), x107, s(x108), s(x106), s(x109), x110)) with σ = [x108 / x31, x109 / x33, x110 / x34] which results in the following new constraint:

(5) (IF(false, x107, s(x31), x106, x33, x34)≥IF2(le(s(x31), s(x33)), x107, s(x31), s(x106), s(x33), x34) ⇒ IF(false, s(x107), s(x31), s(x106), x33, x34)≥IF2(le(s(x31), s(x33)), s(x107), s(x31), s(s(x106)), s(x33), x34))

We simplified constraint (4) using rules (I), (II) which results in the following new constraint:

(6) (IF(false, s(x111), s(x31), 0, x33, x34)≥IF2(le(s(x31), s(x33)), s(x111), s(x31), s(0), s(x33), x34))

For Pair IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v) the following chains were created:

We consider the chain IF(false, x60, x61, x62, x63, x64) → IF2(le(x61, s(x63)), x60, x61, s(x62), s(x63), x64), IF2(false, x65, x66, x67, x68, x69) → QUOTITER(x65, x66, x67, x68, x69) which results in the following constraint:

(1) (IF2(le(x61, s(x63)), x60, x61, s(x62), s(x63), x64)=IF2(false, x65, x66, x67, x68, x69) ⇒ IF2(false, x65, x66, x67, x68, x69)≥QUOTITER(x65, x66, x67, x68, x69))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:

(2) (s(x63)=x112∧le(x61, x112)=false ⇒ IF2(false, x60, x61, s(x62), s(x63), x64)≥QUOTITER(x60, x61, s(x62), s(x63), x64))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x61, x112)=false which results in the following new constraints:

(3) (le(x115, x114)=false∧s(x63)=s(x114)∧(∀x116,x117,x118,x119:le(x115, x114)=false∧s(x116)=x114 ⇒ IF2(false, x117, x115, s(x118), s(x116), x119)≥QUOTITER(x117, x115, s(x118), s(x116), x119)) ⇒ IF2(false, x60, s(x115), s(x62), s(x63), x64)≥QUOTITER(x60, s(x115), s(x62), s(x63), x64))

(4) (false=false∧s(x63)=0 ⇒ IF2(false, x60, s(x120), s(x62), s(x63), x64)≥QUOTITER(x60, s(x120), s(x62), s(x63), x64))

We simplified constraint (3) using rules (I), (II), (III), (IV) which results in the following new constraint:

(5) (le(x115, x114)=false ⇒ IF2(false, x60, s(x115), s(x62), s(x114), x64)≥QUOTITER(x60, s(x115), s(x62), s(x114), x64))

We solved constraint (4) using rules (I), (II).We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on le(x115, x114)=false which results in the following new constraints:

(6) (le(x123, x122)=false∧(∀x124,x125,x126:le(x123, x122)=false ⇒ IF2(false, x124, s(x123), s(x125), s(x122), x126)≥QUOTITER(x124, s(x123), s(x125), s(x122), x126)) ⇒ IF2(false, x60, s(s(x123)), s(x62), s(s(x122)), x64)≥QUOTITER(x60, s(s(x123)), s(x62), s(s(x122)), x64))

(7) (false=false ⇒ IF2(false, x60, s(s(x127)), s(x62), s(0), x64)≥QUOTITER(x60, s(s(x127)), s(x62), s(0), x64))

We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (∀x124,x125,x126:le(x123, x122)=false ⇒ IF2(false, x124, s(x123), s(x125), s(x122), x126)≥QUOTITER(x124, s(x123), s(x125), s(x122), x126)) with σ = [x124 / x60, x125 / x62, x126 / x64] which results in the following new constraint:

(8) (IF2(false, x60, s(x123), s(x62), s(x122), x64)≥QUOTITER(x60, s(x123), s(x62), s(x122), x64) ⇒ IF2(false, x60, s(s(x123)), s(x62), s(s(x122)), x64)≥QUOTITER(x60, s(s(x123)), s(x62), s(s(x122)), x64))

We simplified constraint (7) using rules (I), (II) which results in the following new constraint:

(9) (IF2(false, x60, s(s(x127)), s(x62), s(0), x64)≥QUOTITER(x60, s(s(x127)), s(x62), s(0), x64))

For Pair IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v)) the following chains were created:

We consider the chain IF(false, x85, x86, x87, x88, x89) → IF2(le(x86, s(x88)), x85, x86, s(x87), s(x88), x89), IF2(true, x90, x91, x92, x93, x94) → QUOTITER(x90, x91, x92, 0, s(x94)) which results in the following constraint:

(1) (IF2(le(x86, s(x88)), x85, x86, s(x87), s(x88), x89)=IF2(true, x90, x91, x92, x93, x94) ⇒ IF2(true, x90, x91, x92, x93, x94)≥QUOTITER(x90, x91, x92, 0, s(x94)))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:

(2) (s(x88)=x128∧le(x86, x128)=true ⇒ IF2(true, x85, x86, s(x87), s(x88), x89)≥QUOTITER(x85, x86, s(x87), 0, s(x89)))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x86, x128)=true which results in the following new constraints:

(3) (true=true∧s(x88)=x129 ⇒ IF2(true, x85, 0, s(x87), s(x88), x89)≥QUOTITER(x85, 0, s(x87), 0, s(x89)))

(4) (le(x131, x130)=true∧s(x88)=s(x130)∧(∀x132,x133,x134,x135:le(x131, x130)=true∧s(x132)=x130 ⇒ IF2(true, x133, x131, s(x134), s(x132), x135)≥QUOTITER(x133, x131, s(x134), 0, s(x135))) ⇒ IF2(true, x85, s(x131), s(x87), s(x88), x89)≥QUOTITER(x85, s(x131), s(x87), 0, s(x89)))

We simplified constraint (3) using rules (I), (II), (IV) which results in the following new constraint:

(5) (IF2(true, x85, 0, s(x87), s(x88), x89)≥QUOTITER(x85, 0, s(x87), 0, s(x89)))

We simplified constraint (4) using rules (I), (II), (III), (IV) which results in the following new constraint:

(6) (le(x131, x130)=true ⇒ IF2(true, x85, s(x131), s(x87), s(x130), x89)≥QUOTITER(x85, s(x131), s(x87), 0, s(x89)))

We simplified constraint (6) using rule (V) (with possible (I) afterwards) using induction on le(x131, x130)=true which results in the following new constraints:

(7) (true=true ⇒ IF2(true, x85, s(0), s(x87), s(x137), x89)≥QUOTITER(x85, s(0), s(x87), 0, s(x89)))

(8) (le(x139, x138)=true∧(∀x140,x141,x142:le(x139, x138)=true ⇒ IF2(true, x140, s(x139), s(x141), s(x138), x142)≥QUOTITER(x140, s(x139), s(x141), 0, s(x142))) ⇒ IF2(true, x85, s(s(x139)), s(x87), s(s(x138)), x89)≥QUOTITER(x85, s(s(x139)), s(x87), 0, s(x89)))

We simplified constraint (7) using rules (I), (II) which results in the following new constraint:

(9) (IF2(true, x85, s(0), s(x87), s(x137), x89)≥QUOTITER(x85, s(0), s(x87), 0, s(x89)))

We simplified constraint (8) using rule (VI) where we applied the induction hypothesis (∀x140,x141,x142:le(x139, x138)=true ⇒ IF2(true, x140, s(x139), s(x141), s(x138), x142)≥QUOTITER(x140, s(x139), s(x141), 0, s(x142))) with σ = [x140 / x85, x141 / x87, x142 / x89] which results in the following new constraint:

(10) (IF2(true, x85, s(x139), s(x87), s(x138), x89)≥QUOTITER(x85, s(x139), s(x87), 0, s(x89)) ⇒ IF2(true, x85, s(s(x139)), s(x87), s(s(x138)), x89)≥QUOTITER(x85, s(s(x139)), s(x87), 0, s(x89)))

To summarize, we get the following constraints P_≥ for the following pairs.

QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v)
- (QUOTITER(x10, s(x16), x12, x13, x14)≥IF(le(x10, x12), x10, s(x16), x12, x13, x14))
- (QUOTITER(x20, s(x26), x22, 0, s(x24))≥IF(le(x20, x22), x20, s(x26), x22, 0, s(x24)))
IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
- (IF(false, x107, s(x31), x106, x33, x34)≥IF2(le(s(x31), s(x33)), x107, s(x31), s(x106), s(x33), x34) ⇒ IF(false, s(x107), s(x31), s(x106), x33, x34)≥IF2(le(s(x31), s(x33)), s(x107), s(x31), s(s(x106)), s(x33), x34))
- (IF(false, s(x111), s(x31), 0, x33, x34)≥IF2(le(s(x31), s(x33)), s(x111), s(x31), s(0), s(x33), x34))
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
- (IF2(false, x60, s(x123), s(x62), s(x122), x64)≥QUOTITER(x60, s(x123), s(x62), s(x122), x64) ⇒ IF2(false, x60, s(s(x123)), s(x62), s(s(x122)), x64)≥QUOTITER(x60, s(s(x123)), s(x62), s(s(x122)), x64))
- (IF2(false, x60, s(s(x127)), s(x62), s(0), x64)≥QUOTITER(x60, s(s(x127)), s(x62), s(0), x64))
IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v))
- (IF2(true, x85, 0, s(x87), s(x88), x89)≥QUOTITER(x85, 0, s(x87), 0, s(x89)))
- (IF2(true, x85, s(0), s(x87), s(x137), x89)≥QUOTITER(x85, s(0), s(x87), 0, s(x89)))
- (IF2(true, x85, s(x139), s(x87), s(x138), x89)≥QUOTITER(x85, s(x139), s(x87), 0, s(x89)) ⇒ IF2(true, x85, s(s(x139)), s(x87), s(s(x138)), x89)≥QUOTITER(x85, s(s(x139)), s(x87), 0, s(x89)))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0
POL(IF(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₂ - x₄ + x₅
POL(IF2(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₂ - x₄ + x₅
POL(QUOTITER(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ - x₃ + x₄
POL(c) = -1
POL(false) = 1
POL(le(x₁, x₂)) = 1
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following pairs are in P_>:

IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v))

The following pairs are in P_bound:

IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)

There are no usable rules

(20) Complex Obligation (AND)

(21) Obligation:

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

QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v)
IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

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

(22) NonInfProof (EQUIVALENT transformation)

We consider the chain IF2(false, x10, x11, x12, x13, x14) → QUOTITER(x10, x11, x12, x13, x14), QUOTITER(x15, s(x16), x17, x18, x19) → IF(le(x15, x17), x15, s(x16), x17, x18, x19) which results in the following constraint:
(1) (QUOTITER(x10, x11, x12, x13, x14)=QUOTITER(x15, s(x16), x17, x18, x19) ⇒ QUOTITER(x15, s(x16), x17, x18, x19)≥IF(le(x15, x17), x15, s(x16), x17, x18, x19))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (QUOTITER(x10, s(x16), x12, x13, x14)≥IF(le(x10, x12), x10, s(x16), x12, x13, x14))