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

0 QTRS
↳1 AAECC Innermost (⇔)
↳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 QDPSizeChangeProof (⇔)
    ↳20 TRUE
  ↳21 QDP
    ↳22 UsableRulesProof (⇔)
    ↳23 QDP
    ↳24 QReductionProof (⇔)
    ↳25 QDP
    ↳26 QDPSizeChangeProof (⇔)
    ↳27 TRUE
  ↳28 QDP
    ↳29 UsableRulesProof (⇔)
    ↳30 QDP
    ↳31 QReductionProof (⇔)
    ↳32 QDP
      ↳33 Instantiation (⇔)
        ↳34 QDP
      ↳35 NonInfProof (⇔)
        ↳36 QDP
          ↳37 Instantiation (⇔)
            ↳38 QDP
          ↳39 NonInfProof (⇔)
            ↳40 QDP
            ↳41 PisEmptyProof (⇔)
            ↳42 TRUE

(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 {if, true, triple}

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

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

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

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

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

IF(second, s(z0), s(z1), z2) → IF(le(s(s(z0)), s(s(z1)), z2), s(s(z0)), s(s(z1)), z2)
IF(second, s(z0), z1, s(z2)) → IF(le(s(s(z0)), s(z1), s(z2)), s(s(z0)), s(z1), s(z2))

(34) Obligation:

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

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

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)

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

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

    (11)    (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 (11) using rule (V) (with possible (I) afterwards) using induction on le(x46, x7, x47)=second which results in the following new constraints:

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


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

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

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


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

    (17)    (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 (16) using rule (IV) which results in the following new constraint:

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

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

    (20)    (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 (20) using rule (V) (with possible (I) afterwards) using induction on le(x68, x69, x14)=first which results in the following new constraints:

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


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

    (23)    (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 (22) using rules (I), (II).We simplified constraint (23) using rule (V) (with possible (I) afterwards) using induction on le(x74, x73, x72)=first which results in the following new constraints:

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


    (25)    (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 (24) 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:

    (26)    (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 (25) using rule (IV) which results in the following new constraint:

    (27)    (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, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z)), IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z)) which results in the following constraint:

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

    (29)    (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 (29) using rule (V) (with possible (I) afterwards) using induction on le(x90, x19, x91)=first which results in the following new constraints:

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


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

    (32)    (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 (31) using rules (I), (II).We simplified constraint (32) using rule (V) (with possible (I) afterwards) using induction on le(x96, x95, x94)=first which results in the following new constraints:

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


    (34)    (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 (33) 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:

    (35)    (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 (34) using rule (IV) which results in the following new constraint:

    (36)    (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 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)) = -1 - x1 - x2 + x3   
POL(c) = -1   
POL(false) = 0   
POL(first) = 0   
POL(greater(x1, x2)) = 0   
POL(le(x1, x2, x3)) = 0   
POL(s(x1)) = 1 + x1   
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 Pbound:

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:

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

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

(37) Instantiation (EQUIVALENT transformation)

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

IF(second, s(z0), s(z1), z2) → IF(le(s(s(z0)), s(s(z1)), z2), s(s(z0)), s(s(z1)), z2)

(38) Obligation:

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

IF(second, s(z0), s(z1), z2) → IF(le(s(s(z0)), s(s(z1)), z2), s(s(z0)), s(s(z1)), z2)

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.

(39) 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, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z), IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z) 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)))







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




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)) = -1 - x1 - x2 + x4   
POL(c) = -1   
POL(false) = 1   
POL(first) = 1   
POL(greater(x1, x2)) = 0   
POL(le(x1, x2, x3)) = 0   
POL(s(x1)) = 1 + x1   
POL(second) = 0   

The following pairs are in P>:

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
The following pairs are in Pbound:

IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
The following rules are usable:

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

(40) Obligation:

Q DP problem:
P is empty.
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.

(41) PisEmptyProof (EQUIVALENT transformation)

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

(42) TRUE