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

0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
  ↳7 QDP
    ↳8 UsableRulesProof (⇔)
    ↳9 QDP
    ↳10 QReductionProof (⇔)
    ↳11 QDP
    ↳12 QDPSizeChangeProof (⇔)
    ↳13 TRUE
  ↳14 QDP
    ↳15 UsableRulesProof (⇔)
    ↳16 QDP
    ↳17 QReductionProof (⇔)
    ↳18 QDP
      ↳19 Instantiation (⇔)
        ↳20 QDP
      ↳21 NonInfProof (⇔)
        ↳22 AND
          ↳23 QDP
            ↳24 Instantiation (⇔)
              ↳25 QDP
            ↳26 NonInfProof (⇔)
              ↳27 AND
                ↳28 QDP
                  ↳29 DependencyGraphProof (⇔)
                  ↳30 TRUE
                ↳31 QDP
                  ↳32 DependencyGraphProof (⇔)
                  ↳33 TRUE
          ↳34 QDP
            ↳35 DependencyGraphProof (⇔)
            ↳36 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) TRUE

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

By instantiating [LPAR04] the rule IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v) we obtained the following new rules [LPAR04]:

IF(false, z0, s(z1), z2, z3, z4) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3), z4)

(20) 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)
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))
IF(false, z0, s(z1), z2, z3, z4) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3), z4)

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.

(21) 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, x, y, z, u, v) → QUOTITER(x, y, z, u, v), QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v) 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, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v)), QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v) which results in the following constraint:

    (3)    (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 (3) using rules (I), (II), (III) which results in the following new constraint:

    (4)    (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(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) which results in the following constraint:

    (5)    (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 (5) using rules (I), (II), (III) which results in the following new constraint:

    (6)    (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 (6) using rule (V) (with possible (I) afterwards) using induction on le(x30, x32)=false which results in the following new constraints:

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


    (8)    (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 (7) 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 σ = [x110 / x34, x109 / x33, x108 / x31] which results in the following new constraint:

    (9)    (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 (8) using rules (I), (II) which results in the following new constraint:

    (10)    (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, 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) which results in the following constraint:

    (11)    (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 (11) using rules (I), (II), (III), (VII) which results in the following new constraint:

    (12)    (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 (12) using rule (V) (with possible (I) afterwards) using induction on le(x61, x112)=false which results in the following new constraints:

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


    (14)    (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 (13) using rules (I), (II), (III), (IV) which results in the following new constraint:

    (15)    (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 (14) using rules (I), (II).We simplified constraint (15) using rule (V) (with possible (I) afterwards) using induction on le(x115, x114)=false which results in the following new constraints:

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


    (17)    (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 (16) 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 σ = [x125 / x62, x126 / x64, x124 / x60] which results in the following new constraint:

    (18)    (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 (17) using rules (I), (II) which results in the following new constraint:

    (19)    (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, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v), IF2(true, x, y, z, u, v) → QUOTITER(x, y, z, 0, s(v)) which results in the following constraint:

    (20)    (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 (20) using rules (I), (II), (III), (VII) which results in the following new constraint:

    (21)    (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 (21) using rule (V) (with possible (I) afterwards) using induction on le(x86, x128)=true which results in the following new constraints:

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


    (23)    (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 (22) using rules (I), (II), (IV) which results in the following new constraint:

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



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

    (25)    (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 (25) using rule (V) (with possible (I) afterwards) using induction on le(x131, x130)=true which results in the following new constraints:

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


    (27)    (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 (26) using rules (I), (II) which results in the following new constraint:

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



    We simplified constraint (27) 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, x142 / x89, x141 / x87] which results in the following new constraint:

    (29)    (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 Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF(x1, x2, x3, x4, x5, x6)) = -1 - x1 + x2 - x4 + x5   
POL(IF2(x1, x2, x3, x4, x5, x6)) = -1 - x1 + x2 - x4 + x5   
POL(QUOTITER(x1, x2, x3, x4, x5)) = -1 + x1 - x3 + x4   
POL(c) = -1   
POL(false) = 0   
POL(le(x1, x2)) = 0   
POL(s(x1)) = 1 + x1   
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 Pbound:

IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
The following rules are usable:

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

(22) Complex Obligation (AND)

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

(24) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v) we obtained the following new rules [LPAR04]:

IF(false, z0, s(z1), z2, z3, z4) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3), z4)

(25) 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)
IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
IF(false, z0, s(z1), z2, z3, z4) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3), z4)

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.

(26) 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, x, y, z, u, v) → QUOTITER(x, y, z, u, v), QUOTITER(x, s(y), z, u, v) → IF(le(x, z), x, s(y), z, u, v) 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))







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(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) which results in the following constraint:

    (3)    (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 (3) using rules (I), (II), (III) which results in the following new constraint:

    (4)    (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 (4) using rule (V) (with possible (I) afterwards) using induction on le(x30, x32)=false which results in the following new constraints:

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


    (6)    (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 (5) 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 σ = [x110 / x34, x109 / x33, x108 / x31] which results in the following new constraint:

    (7)    (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 (6) using rules (I), (II) which results in the following new constraint:

    (8)    (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, 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) which results in the following constraint:

    (9)    (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 (9) using rules (I), (II), (III), (VII) which results in the following new constraint:

    (10)    (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 (10) using rule (V) (with possible (I) afterwards) using induction on le(x61, x112)=false which results in the following new constraints:

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


    (12)    (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 (11) using rules (I), (II), (III), (IV) which results in the following new constraint:

    (13)    (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 (12) using rules (I), (II).We simplified constraint (13) using rule (V) (with possible (I) afterwards) using induction on le(x115, x114)=false which results in the following new constraints:

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


    (15)    (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 (14) 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 σ = [x125 / x62, x126 / x64, x124 / x60] which results in the following new constraint:

    (16)    (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 (15) using rules (I), (II) which results in the following new constraint:

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







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

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




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF(x1, x2, x3, x4, x5, x6)) = -1 - x1 + x3 - x5   
POL(IF2(x1, x2, x3, x4, x5, x6)) = -1 - x1 + x3 - x5   
POL(QUOTITER(x1, x2, x3, x4, x5)) = -1 + x2 - x4   
POL(c) = -1   
POL(false) = 0   
POL(le(x1, x2)) = 0   
POL(s(x1)) = 1 + x1   
POL(true) = 1   

The following pairs are in P>:

IF(false, x, y, z, u, v) → IF2(le(y, s(u)), x, y, s(z), s(u), v)
The following pairs are in Pbound:

IF2(false, x, y, z, u, v) → QUOTITER(x, y, z, u, v)
The following rules are usable:

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

(27) Complex Obligation (AND)

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

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

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

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.

(32) DependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

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

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE