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 QDPSizeChangeProof (⇔)
    ↳34 TRUE
  ↳35 QDP
    ↳36 UsableRulesProof (⇔)
    ↳37 QDP
    ↳38 QReductionProof (⇔)
    ↳39 QDP
      ↳40 Instantiation (⇔)
        ↳41 QDP
      ↳42 NonInfProof (⇔)
        ↳43 AND
          ↳44 QDP
            ↳45 DependencyGraphProof (⇔)
            ↳46 TRUE
          ↳47 QDP
            ↳48 DependencyGraphProof (⇔)
            ↳49 TRUE
  ↳50 QDP
    ↳51 UsableRulesProof (⇔)
    ↳52 QDP
    ↳53 QReductionProof (⇔)
    ↳54 QDP
      ↳55 Instantiation (⇔)
        ↳56 QDP
      ↳57 Narrowing (⇔)
        ↳58 QDP
        ↳59 DependencyGraphProof (⇔)
        ↳60 QDP
        ↳61 UsableRulesProof (⇔)
        ↳62 QDP
        ↳63 QReductionProof (⇔)
        ↳64 QDP
        ↳65 QDPOrderProof (⇔)
        ↳66 QDP
        ↳67 DependencyGraphProof (⇔)
        ↳68 TRUE

(0) Obligation:

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

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

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)))
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)

The TRS R 2 is

a → b
a → c

The signature Sigma is {c, a, b}

(2) Obligation:

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

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

(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)
DOUBLE(s(x)) → DOUBLE(x)
LOG(s(x)) → LOOP(s(x), s(0), 0)
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
LOOP(x, s(y), z) → LE(x, s(y))
IF(false, x, y, z) → LOOP(x, double(y), s(z))
IF(false, x, y, z) → DOUBLE(y)
MAPLOG(xs) → MAPITER(xs, nil)
MAPITER(xs, ys) → IFMAP(isempty(xs), xs, ys)
MAPITER(xs, ys) → ISEMPTY(xs)
IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
IFMAP(false, xs, ys) → DROPLAST(xs)
IFMAP(false, xs, ys) → LOG(last(xs))
IFMAP(false, xs, ys) → LAST(xs)
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
DROPLAST(cons(x, cons(y, xs))) → DROPLAST(cons(y, xs))

The TRS R consists of the following rules:

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

DROPLAST(cons(x, cons(y, xs))) → DROPLAST(cons(y, xs))

The TRS R consists of the following rules:

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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:

DROPLAST(cons(x, cons(y, xs))) → DROPLAST(cons(y, xs))

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

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

(11) Obligation:

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

DROPLAST(cons(x, cons(y, xs))) → DROPLAST(cons(y, xs))

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:

  • DROPLAST(cons(x, cons(y, xs))) → DROPLAST(cons(y, xs))
    The graph contains the following edges 1 > 1

(13) TRUE

(14) Obligation:

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

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

The TRS R consists of the following rules:

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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:

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

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

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

(18) Obligation:

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

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

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:

  • LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
    The graph contains the following edges 1 > 1

(20) TRUE

(21) 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(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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:

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

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

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

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

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

(27) TRUE

(28) 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(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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:

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

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

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

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

(34) TRUE

(35) Obligation:

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

LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
IF(false, x, y, z) → LOOP(x, double(y), s(z))

The TRS R consists of the following rules:

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

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

(37) Obligation:

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

LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
IF(false, x, y, z) → LOOP(x, double(y), s(z))

The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

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

log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

(39) Obligation:

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

LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
IF(false, x, y, z) → LOOP(x, double(y), s(z))

The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))

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

(40) Instantiation (EQUIVALENT transformation)

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

LOOP(z0, s(x1), s(z2)) → IF(le(z0, s(x1)), z0, s(x1), s(z2))

(41) Obligation:

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

IF(false, x, y, z) → LOOP(x, double(y), s(z))
LOOP(z0, s(x1), s(z2)) → IF(le(z0, s(x1)), z0, s(x1), s(z2))

The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))

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

(42) 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 LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z) the following chains were created:
  • We consider the chain LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z), IF(false, x, y, z) → LOOP(x, double(y), s(z)) which results in the following constraint:

    (1)    (IF(le(x3, s(x4)), x3, s(x4), x5)=IF(false, x6, x7, x8) ⇒ LOOP(x3, s(x4), x5)≥IF(le(x3, s(x4)), x3, s(x4), x5))



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

    (2)    (s(x4)=x18∧le(x3, x18)=false ⇒ LOOP(x3, s(x4), x5)≥IF(le(x3, s(x4)), x3, s(x4), x5))



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

    (3)    (le(x21, x20)=false∧s(x4)=s(x20)∧(∀x22,x23:le(x21, x20)=false∧s(x22)=x20 ⇒ LOOP(x21, s(x22), x23)≥IF(le(x21, s(x22)), x21, s(x22), x23)) ⇒ LOOP(s(x21), s(x4), x5)≥IF(le(s(x21), s(x4)), s(x21), s(x4), x5))


    (4)    (false=false∧s(x4)=0 ⇒ LOOP(s(x24), s(x4), x5)≥IF(le(s(x24), s(x4)), s(x24), s(x4), x5))



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

    (5)    (le(x21, x20)=false ⇒ LOOP(s(x21), s(x20), x5)≥IF(le(s(x21), s(x20)), s(x21), s(x20), x5))



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

    (6)    (le(x27, x26)=false∧(∀x28:le(x27, x26)=false ⇒ LOOP(s(x27), s(x26), x28)≥IF(le(s(x27), s(x26)), s(x27), s(x26), x28)) ⇒ LOOP(s(s(x27)), s(s(x26)), x5)≥IF(le(s(s(x27)), s(s(x26))), s(s(x27)), s(s(x26)), x5))


    (7)    (false=false ⇒ LOOP(s(s(x29)), s(0), x5)≥IF(le(s(s(x29)), s(0)), s(s(x29)), s(0), x5))



    We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (∀x28:le(x27, x26)=false ⇒ LOOP(s(x27), s(x26), x28)≥IF(le(s(x27), s(x26)), s(x27), s(x26), x28)) with σ = [x28 / x5] which results in the following new constraint:

    (8)    (LOOP(s(x27), s(x26), x5)≥IF(le(s(x27), s(x26)), s(x27), s(x26), x5) ⇒ LOOP(s(s(x27)), s(s(x26)), x5)≥IF(le(s(s(x27)), s(s(x26))), s(s(x27)), s(s(x26)), x5))



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

    (9)    (LOOP(s(s(x29)), s(0), x5)≥IF(le(s(s(x29)), s(0)), s(s(x29)), s(0), x5))







For Pair IF(false, x, y, z) → LOOP(x, double(y), s(z)) the following chains were created:
  • We consider the chain IF(false, x, y, z) → LOOP(x, double(y), s(z)), LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z) which results in the following constraint:

    (10)    (LOOP(x9, double(x10), s(x11))=LOOP(x12, s(x13), x14) ⇒ IF(false, x9, x10, x11)≥LOOP(x9, double(x10), s(x11)))



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

    (11)    (double(x10)=s(x13) ⇒ IF(false, x9, x10, x11)≥LOOP(x9, double(x10), s(x11)))



    We simplified constraint (11) using rule (V) (with possible (I) afterwards) using induction on double(x10)=s(x13) which results in the following new constraint:

    (12)    (s(s(double(x30)))=s(x13)∧(∀x31,x32,x33:double(x30)=s(x31) ⇒ IF(false, x32, x30, x33)≥LOOP(x32, double(x30), s(x33))) ⇒ IF(false, x9, s(x30), x11)≥LOOP(x9, double(s(x30)), s(x11)))



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

    (13)    (IF(false, x9, s(x30), x11)≥LOOP(x9, double(s(x30)), s(x11)))







To summarize, we get the following constraints P≥ for the following pairs.
  • LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
    • (LOOP(s(x27), s(x26), x5)≥IF(le(s(x27), s(x26)), s(x27), s(x26), x5) ⇒ LOOP(s(s(x27)), s(s(x26)), x5)≥IF(le(s(s(x27)), s(s(x26))), s(s(x27)), s(s(x26)), x5))
    • (LOOP(s(s(x29)), s(0), x5)≥IF(le(s(s(x29)), s(0)), s(s(x29)), s(0), x5))

  • IF(false, x, y, z) → LOOP(x, double(y), s(z))
    • (IF(false, x9, s(x30), x11)≥LOOP(x9, double(s(x30)), s(x11)))




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(LOOP(x1, x2, x3)) = -1 + x1 - x2   
POL(c) = -4   
POL(double(x1)) = 2·x1   
POL(false) = 1   
POL(le(x1, x2)) = 0   
POL(s(x1)) = 2 + x1   
POL(true) = 0   

The following pairs are in P>:

IF(false, x, y, z) → LOOP(x, double(y), s(z))
The following pairs are in Pbound:

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

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

(43) Complex Obligation (AND)

(44) Obligation:

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

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

The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))

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

(45) DependencyGraphProof (EQUIVALENT transformation)

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

(46) TRUE

(47) Obligation:

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

IF(false, x, y, z) → LOOP(x, double(y), s(z))

The TRS R consists of the following rules:

double(0) → 0
double(s(x)) → s(s(double(x)))
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(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))

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

(48) DependencyGraphProof (EQUIVALENT transformation)

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

(49) TRUE

(50) Obligation:

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

IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
MAPITER(xs, ys) → IFMAP(isempty(xs), xs, ys)

The TRS R consists of the following rules:

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

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

(52) Obligation:

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

IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
MAPITER(xs, ys) → IFMAP(isempty(xs), xs, ys)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(cons(x, xs)) → false
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))
a

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

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

maplog(x0)
mapIter(x0, x1)
ifmap(true, x0, x1)
ifmap(false, x0, x1)
a

(54) Obligation:

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

IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
MAPITER(xs, ys) → IFMAP(isempty(xs), xs, ys)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(cons(x, xs)) → false
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

(55) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule MAPITER(xs, ys) → IFMAP(isempty(xs), xs, ys) we obtained the following new rules [LPAR04]:

MAPITER(y_0, cons(y_2, z1)) → IFMAP(isempty(y_0), y_0, cons(y_2, z1))

(56) Obligation:

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

IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
MAPITER(y_0, cons(y_2, z1)) → IFMAP(isempty(y_0), y_0, cons(y_2, z1))

The TRS R consists of the following rules:

isempty(nil) → true
isempty(cons(x, xs)) → false
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

(57) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MAPITER(xs, ys) → IFMAP(isempty(xs), xs, ys) at position [0] we obtained the following new rules [LPAR04]:

MAPITER(nil, y1) → IFMAP(true, nil, y1)
MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)

(58) Obligation:

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

IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
MAPITER(nil, y1) → IFMAP(true, nil, y1)
MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(cons(x, xs)) → false
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

(59) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(60) Obligation:

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

MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)
IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))

The TRS R consists of the following rules:

isempty(nil) → true
isempty(cons(x, xs)) → false
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

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

(62) Obligation:

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

MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)
IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))

The TRS R consists of the following rules:

droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
double(0) → 0
double(s(x)) → s(s(double(x)))
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

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

isempty(nil)
isempty(cons(x0, x1))

(64) Obligation:

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

MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)
IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))

The TRS R consists of the following rules:

droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
double(0) → 0
double(s(x)) → s(s(double(x)))
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


IFMAP(false, xs, ys) → MAPITER(droplast(xs), cons(log(last(xs)), ys))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(MAPITER(x1, x2)) =
/0\
\0/
 +
/01\
\01/
·x1 +
/00\
\00/
·x2

POL(cons(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/01\
\01/
·x2

POL(IFMAP(x1, x2, x3)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/10\
\10/
·x2 +
/00\
\00/
·x3

POL(false) =
/1\
\1/

POL(droplast(x1)) =
/0\
\0/
 +
/10\
\10/
·x1

POL(log(x1)) =
/0\
\1/
 +
/00\
\10/
·x1

POL(last(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(le(x1, x2)) =
/0\
\0/
 +
/01\
\11/
·x1 +
/10\
\11/
·x2

POL(s(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(0) =
/1\
\0/

POL(double(x1)) =
/0\
\1/
 +
/00\
\01/
·x1

POL(if(x1, x2, x3, x4)) =
/0\
\0/
 +
/11\
\11/
·x1 +
/00\
\10/
·x2 +
/10\
\01/
·x3 +
/10\
\10/
·x4

POL(true) =
/1\
\1/

POL(loop(x1, x2, x3)) =
/0\
\1/
 +
/01\
\01/
·x1 +
/01\
\00/
·x2 +
/10\
\00/
·x3

POL(logError) =
/1\
\1/

POL(nil) =
/0\
\0/

POL(error) =
/1\
\1/

The following usable rules [FROCOS05] were oriented:

droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
droplast(cons(x, nil)) → nil
droplast(nil) → nil

(66) Obligation:

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

MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)

The TRS R consists of the following rules:

droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
if(false, x, y, z) → loop(x, double(y), s(z))
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
le(0, y) → true
le(s(x), s(y)) → le(x, y)
if(true, x, y, z) → z
double(0) → 0
double(s(x)) → s(s(double(x)))
le(s(x), 0) → false

The set Q consists of the following terms:

le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
droplast(nil)
droplast(cons(x0, nil))
droplast(cons(x0, cons(x1, x2)))

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

(67) DependencyGraphProof (EQUIVALENT transformation)

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

(68) TRUE