Termination w.r.t. Q proof of AProVE_07

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

0 QTRS

↳1 AAECC Innermost (⇔, 8 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 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 QDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 QDP

        ↳24 QReductionProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 QDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 QDP

        ↳31 QReductionProof (⇔, 0 ms)

        ↳32 QDP

        ↳33 NonInfProof (⇔, 18 ms)

        ↳34 QDP

        ↳35 NonInfProof (⇔, 7 ms)

        ↳36 QDP

        ↳37 PisEmptyProof (⇔, 0 ms)

        ↳38 YES

(0) Obligation:

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

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)

The TRS R 2 is

triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The signature Sigma is {triple, if, true}

(2) Obligation:

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

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

(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(0, y, z) → GREATER(y, z)
LE(s(x), s(y), s(z)) → LE(x, y, z)
GREATER(s(x), s(y)) → GREATER(x, y)
DOUBLE(s(x)) → DOUBLE(x)
TRIPLE(x) → IF(le(x, x, double(x)), x, 0, 0)
TRIPLE(x) → LE(x, x, double(x))
TRIPLE(x) → DOUBLE(x)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
IF(first, x, y, z) → LE(s(x), y, s(z))
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(second, x, y, z) → LE(s(x), s(y), z)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

DOUBLE(s(x)) → DOUBLE(x)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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:

DOUBLE(s(x)) → DOUBLE(x)

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

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

(11) Obligation:

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

DOUBLE(s(x)) → DOUBLE(x)

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:

DOUBLE(s(x)) → DOUBLE(x)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

GREATER(s(x), s(y)) → GREATER(x, y)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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:

GREATER(s(x), s(y)) → GREATER(x, y)

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

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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].

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

(18) Obligation:

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

GREATER(s(x), s(y)) → GREATER(x, y)

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

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

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

(20) YES

(21) Obligation:

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

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

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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

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

(23) Obligation:

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

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

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

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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

(24) 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, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

(25) Obligation:

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

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

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

(26) 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), s(z)) → LE(x, y, z)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3

(27) YES

(28) Obligation:

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

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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

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

(30) Obligation:

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

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))

The TRS R consists of the following rules:

le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)

The set Q consists of the following terms:

le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

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

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

double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)

(32) Obligation:

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

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))

The TRS R consists of the following rules:

le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)

The set Q consists of the following terms:

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

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

(33) 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 IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z) the following chains were created:

We consider the chain IF(second, x0, x1, x2) → IF(le(s(x0), s(x1), x2), s(x0), s(x1), x2), IF(second, x3, x4, x5) → IF(le(s(x3), s(x4), x5), s(x3), s(x4), x5) which results in the following constraint:

(1) (IF(le(s(x0), s(x1), x2), s(x0), s(x1), x2)=IF(second, x3, x4, x5) ⇒ IF(second, x3, x4, x5)≥IF(le(s(x3), s(x4), x5), s(x3), s(x4), x5))

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

(2) (s(x0)=x24∧s(x1)=x25∧le(x24, x25, x2)=second ⇒ IF(second, s(x0), s(x1), x2)≥IF(le(s(s(x0)), s(s(x1)), x2), s(s(x0)), s(s(x1)), x2))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x24, x25, x2)=second which results in the following new constraints:

(3) (le(x30, x29, x28)=second∧s(x0)=s(x30)∧s(x1)=s(x29)∧(∀x31,x32:le(x30, x29, x28)=second∧s(x31)=x30∧s(x32)=x29 ⇒ IF(second, s(x31), s(x32), x28)≥IF(le(s(s(x31)), s(s(x32)), x28), s(s(x31)), s(s(x32)), x28)) ⇒ IF(second, s(x0), s(x1), s(x28))≥IF(le(s(s(x0)), s(s(x1)), s(x28)), s(s(x0)), s(s(x1)), s(x28)))

(4) (greater(x34, x33)=second∧s(x0)=0∧s(x1)=x34 ⇒ IF(second, s(x0), s(x1), x33)≥IF(le(s(s(x0)), s(s(x1)), x33), s(s(x0)), s(s(x1)), x33))

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

(5) (le(x30, x29, x28)=second ⇒ IF(second, s(x30), s(x29), s(x28))≥IF(le(s(s(x30)), s(s(x29)), s(x28)), s(s(x30)), s(s(x29)), s(x28)))

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

(6) (le(x41, x40, x39)=second∧(le(x41, x40, x39)=second ⇒ IF(second, s(x41), s(x40), s(x39))≥IF(le(s(s(x41)), s(s(x40)), s(x39)), s(s(x41)), s(s(x40)), s(x39))) ⇒ IF(second, s(s(x41)), s(s(x40)), s(s(x39)))≥IF(le(s(s(s(x41))), s(s(s(x40))), s(s(x39))), s(s(s(x41))), s(s(s(x40))), s(s(x39))))

(7) (greater(x43, x42)=second ⇒ IF(second, s(0), s(x43), s(x42))≥IF(le(s(s(0)), s(s(x43)), s(x42)), s(s(0)), s(s(x43)), s(x42)))

We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (le(x41, x40, x39)=second ⇒ IF(second, s(x41), s(x40), s(x39))≥IF(le(s(s(x41)), s(s(x40)), s(x39)), s(s(x41)), s(s(x40)), s(x39))) with σ = [ ] which results in the following new constraint:

(8) (IF(second, s(x41), s(x40), s(x39))≥IF(le(s(s(x41)), s(s(x40)), s(x39)), s(s(x41)), s(s(x40)), s(x39)) ⇒ IF(second, s(s(x41)), s(s(x40)), s(s(x39)))≥IF(le(s(s(s(x41))), s(s(s(x40))), s(s(x39))), s(s(s(x41))), s(s(s(x40))), s(s(x39))))

We simplified constraint (7) using rule (IV) which results in the following new constraint:

(9) (IF(second, s(0), s(x43), s(x42))≥IF(le(s(s(0)), s(s(x43)), s(x42)), s(s(0)), s(s(x43)), s(x42)))

We consider the chain IF(first, x6, x7, x8) → IF(le(s(x6), x7, s(x8)), s(x6), x7, s(x8)), IF(second, x9, x10, x11) → IF(le(s(x9), s(x10), x11), s(x9), s(x10), x11) which results in the following constraint:

(1) (IF(le(s(x6), x7, s(x8)), s(x6), x7, s(x8))=IF(second, x9, x10, x11) ⇒ IF(second, x9, x10, x11)≥IF(le(s(x9), s(x10), x11), s(x9), s(x10), x11))

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

(2) (s(x6)=x46∧s(x8)=x47∧le(x46, x7, x47)=second ⇒ IF(second, s(x6), x7, s(x8))≥IF(le(s(s(x6)), s(x7), s(x8)), s(s(x6)), s(x7), s(x8)))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x46, x7, x47)=second which results in the following new constraints:

(3) (le(x52, x51, x50)=second∧s(x6)=s(x52)∧s(x8)=s(x50)∧(∀x53,x54:le(x52, x51, x50)=second∧s(x53)=x52∧s(x54)=x50 ⇒ IF(second, s(x53), x51, s(x54))≥IF(le(s(s(x53)), s(x51), s(x54)), s(s(x53)), s(x51), s(x54))) ⇒ IF(second, s(x6), s(x51), s(x8))≥IF(le(s(s(x6)), s(s(x51)), s(x8)), s(s(x6)), s(s(x51)), s(x8)))

(4) (greater(x56, x55)=second∧s(x6)=0∧s(x8)=x55 ⇒ IF(second, s(x6), x56, s(x8))≥IF(le(s(s(x6)), s(x56), s(x8)), s(s(x6)), s(x56), s(x8)))

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

(5) (le(x52, x51, x50)=second ⇒ IF(second, s(x52), s(x51), s(x50))≥IF(le(s(s(x52)), s(s(x51)), s(x50)), s(s(x52)), s(s(x51)), s(x50)))

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

(6) (le(x63, x62, x61)=second∧(le(x63, x62, x61)=second ⇒ IF(second, s(x63), s(x62), s(x61))≥IF(le(s(s(x63)), s(s(x62)), s(x61)), s(s(x63)), s(s(x62)), s(x61))) ⇒ IF(second, s(s(x63)), s(s(x62)), s(s(x61)))≥IF(le(s(s(s(x63))), s(s(s(x62))), s(s(x61))), s(s(s(x63))), s(s(s(x62))), s(s(x61))))

(7) (greater(x65, x64)=second ⇒ IF(second, s(0), s(x65), s(x64))≥IF(le(s(s(0)), s(s(x65)), s(x64)), s(s(0)), s(s(x65)), s(x64)))

We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (le(x63, x62, x61)=second ⇒ IF(second, s(x63), s(x62), s(x61))≥IF(le(s(s(x63)), s(s(x62)), s(x61)), s(s(x63)), s(s(x62)), s(x61))) with σ = [ ] which results in the following new constraint:

(8) (IF(second, s(x63), s(x62), s(x61))≥IF(le(s(s(x63)), s(s(x62)), s(x61)), s(s(x63)), s(s(x62)), s(x61)) ⇒ IF(second, s(s(x63)), s(s(x62)), s(s(x61)))≥IF(le(s(s(s(x63))), s(s(s(x62))), s(s(x61))), s(s(s(x63))), s(s(s(x62))), s(s(x61))))

We simplified constraint (7) using rule (IV) which results in the following new constraint:

(9) (IF(second, s(0), s(x65), s(x64))≥IF(le(s(s(0)), s(s(x65)), s(x64)), s(s(0)), s(s(x65)), s(x64)))

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

We consider the chain IF(second, x12, x13, x14) → IF(le(s(x12), s(x13), x14), s(x12), s(x13), x14), IF(first, x15, x16, x17) → IF(le(s(x15), x16, s(x17)), s(x15), x16, s(x17)) which results in the following constraint:

(1) (IF(le(s(x12), s(x13), x14), s(x12), s(x13), x14)=IF(first, x15, x16, x17) ⇒ IF(first, x15, x16, x17)≥IF(le(s(x15), x16, s(x17)), s(x15), x16, s(x17)))

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

(2) (s(x12)=x68∧s(x13)=x69∧le(x68, x69, x14)=first ⇒ IF(first, s(x12), s(x13), x14)≥IF(le(s(s(x12)), s(x13), s(x14)), s(s(x12)), s(x13), s(x14)))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x68, x69, x14)=first which results in the following new constraints:

(3) (le(x74, x73, x72)=first∧s(x12)=s(x74)∧s(x13)=s(x73)∧(∀x75,x76:le(x74, x73, x72)=first∧s(x75)=x74∧s(x76)=x73 ⇒ IF(first, s(x75), s(x76), x72)≥IF(le(s(s(x75)), s(x76), s(x72)), s(s(x75)), s(x76), s(x72))) ⇒ IF(first, s(x12), s(x13), s(x72))≥IF(le(s(s(x12)), s(x13), s(s(x72))), s(s(x12)), s(x13), s(s(x72))))

(4) (greater(x78, x77)=first∧s(x12)=0∧s(x13)=x78 ⇒ IF(first, s(x12), s(x13), x77)≥IF(le(s(s(x12)), s(x13), s(x77)), s(s(x12)), s(x13), s(x77)))

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

(5) (le(x74, x73, x72)=first ⇒ IF(first, s(x74), s(x73), s(x72))≥IF(le(s(s(x74)), s(x73), s(s(x72))), s(s(x74)), s(x73), s(s(x72))))

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

(6) (le(x85, x84, x83)=first∧(le(x85, x84, x83)=first ⇒ IF(first, s(x85), s(x84), s(x83))≥IF(le(s(s(x85)), s(x84), s(s(x83))), s(s(x85)), s(x84), s(s(x83)))) ⇒ IF(first, s(s(x85)), s(s(x84)), s(s(x83)))≥IF(le(s(s(s(x85))), s(s(x84)), s(s(s(x83)))), s(s(s(x85))), s(s(x84)), s(s(s(x83)))))

(7) (greater(x87, x86)=first ⇒ IF(first, s(0), s(x87), s(x86))≥IF(le(s(s(0)), s(x87), s(s(x86))), s(s(0)), s(x87), s(s(x86))))

We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (le(x85, x84, x83)=first ⇒ IF(first, s(x85), s(x84), s(x83))≥IF(le(s(s(x85)), s(x84), s(s(x83))), s(s(x85)), s(x84), s(s(x83)))) with σ = [ ] which results in the following new constraint:

(8) (IF(first, s(x85), s(x84), s(x83))≥IF(le(s(s(x85)), s(x84), s(s(x83))), s(s(x85)), s(x84), s(s(x83))) ⇒ IF(first, s(s(x85)), s(s(x84)), s(s(x83)))≥IF(le(s(s(s(x85))), s(s(x84)), s(s(s(x83)))), s(s(s(x85))), s(s(x84)), s(s(s(x83)))))

We simplified constraint (7) using rule (IV) which results in the following new constraint:

(9) (IF(first, s(0), s(x87), s(x86))≥IF(le(s(s(0)), s(x87), s(s(x86))), s(s(0)), s(x87), s(s(x86))))

We consider the chain IF(first, x18, x19, x20) → IF(le(s(x18), x19, s(x20)), s(x18), x19, s(x20)), IF(first, x21, x22, x23) → IF(le(s(x21), x22, s(x23)), s(x21), x22, s(x23)) which results in the following constraint:

(1) (IF(le(s(x18), x19, s(x20)), s(x18), x19, s(x20))=IF(first, x21, x22, x23) ⇒ IF(first, x21, x22, x23)≥IF(le(s(x21), x22, s(x23)), s(x21), x22, s(x23)))

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

(2) (s(x18)=x90∧s(x20)=x91∧le(x90, x19, x91)=first ⇒ IF(first, s(x18), x19, s(x20))≥IF(le(s(s(x18)), x19, s(s(x20))), s(s(x18)), x19, s(s(x20))))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x90, x19, x91)=first which results in the following new constraints:

(3) (le(x96, x95, x94)=first∧s(x18)=s(x96)∧s(x20)=s(x94)∧(∀x97,x98:le(x96, x95, x94)=first∧s(x97)=x96∧s(x98)=x94 ⇒ IF(first, s(x97), x95, s(x98))≥IF(le(s(s(x97)), x95, s(s(x98))), s(s(x97)), x95, s(s(x98)))) ⇒ IF(first, s(x18), s(x95), s(x20))≥IF(le(s(s(x18)), s(x95), s(s(x20))), s(s(x18)), s(x95), s(s(x20))))

(4) (greater(x100, x99)=first∧s(x18)=0∧s(x20)=x99 ⇒ IF(first, s(x18), x100, s(x20))≥IF(le(s(s(x18)), x100, s(s(x20))), s(s(x18)), x100, s(s(x20))))

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

(5) (le(x96, x95, x94)=first ⇒ IF(first, s(x96), s(x95), s(x94))≥IF(le(s(s(x96)), s(x95), s(s(x94))), s(s(x96)), s(x95), s(s(x94))))

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

(6) (le(x107, x106, x105)=first∧(le(x107, x106, x105)=first ⇒ IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105)))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))

(7) (greater(x109, x108)=first ⇒ IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))

We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (le(x107, x106, x105)=first ⇒ IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105)))) with σ = [ ] which results in the following new constraint:

(8) (IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))

We simplified constraint (7) using rule (IV) which results in the following new constraint:

(9) (IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))

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

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
- (IF(second, s(x41), s(x40), s(x39))≥IF(le(s(s(x41)), s(s(x40)), s(x39)), s(s(x41)), s(s(x40)), s(x39)) ⇒ IF(second, s(s(x41)), s(s(x40)), s(s(x39)))≥IF(le(s(s(s(x41))), s(s(s(x40))), s(s(x39))), s(s(s(x41))), s(s(s(x40))), s(s(x39))))
- (IF(second, s(0), s(x43), s(x42))≥IF(le(s(s(0)), s(s(x43)), s(x42)), s(s(0)), s(s(x43)), s(x42)))
- (IF(second, s(x63), s(x62), s(x61))≥IF(le(s(s(x63)), s(s(x62)), s(x61)), s(s(x63)), s(s(x62)), s(x61)) ⇒ IF(second, s(s(x63)), s(s(x62)), s(s(x61)))≥IF(le(s(s(s(x63))), s(s(s(x62))), s(s(x61))), s(s(s(x63))), s(s(s(x62))), s(s(x61))))
- (IF(second, s(0), s(x65), s(x64))≥IF(le(s(s(0)), s(s(x65)), s(x64)), s(s(0)), s(s(x65)), s(x64)))
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
- (IF(first, s(x85), s(x84), s(x83))≥IF(le(s(s(x85)), s(x84), s(s(x83))), s(s(x85)), s(x84), s(s(x83))) ⇒ IF(first, s(s(x85)), s(s(x84)), s(s(x83)))≥IF(le(s(s(s(x85))), s(s(x84)), s(s(s(x83)))), s(s(s(x85))), s(s(x84)), s(s(s(x83)))))
- (IF(first, s(0), s(x87), s(x86))≥IF(le(s(s(0)), s(x87), s(s(x86))), s(s(0)), s(x87), s(s(x86))))
- (IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))
- (IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))

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) = 1
POL(IF(x₁, x₂, x₃, x₄)) = -1 - x₁ - x₂ + x₃
POL(c) = -2
POL(false) = 1
POL(first) = 0
POL(greater(x₁, x₂)) = 0
POL(le(x₁, x₂, x₃)) = 0
POL(s(x₁)) = 1 + x₁
POL(second) = 0

The following pairs are in P_>:

IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))

The following pairs are in P_bound:

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))

The following rules are usable:

le(x, y, z) → le(s(x), s(y), s(z))
false → le(s(x), s(y), 0)
false → le(s(x), 0, z)
greater(y, z) → le(0, y, z)
first → greater(x, 0)
second → greater(0, s(y))
greater(x, y) → greater(s(x), s(y))

(34) Obligation:

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

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)

The TRS R consists of the following rules:

le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)

The set Q consists of the following terms:

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

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

(35) NonInfProof (EQUIVALENT transformation)