YES Termination w.r.t. Q proof of Secret_07_TRS_aprove06.ari

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

0 QTRS
↳1 AAECC Innermost (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QReductionProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QReductionProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 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 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 QDP
        ↳36 UsableRulesProof (⇔, 0 ms)
        ↳37 QDP
        ↳38 QReductionProof (⇔, 0 ms)
        ↳39 QDP
        ↳40 NonInfProof (⇔, 12 ms)
        ↳41 AND
            ↳42 QDP
                ↳43 DependencyGraphProof (⇔, 0 ms)
                ↳44 TRUE
            ↳45 QDP
                ↳46 DependencyGraphProof (⇔, 0 ms)
                ↳47 TRUE
    ↳48 QDP
        ↳49 UsableRulesProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 QReductionProof (⇔, 3 ms)
        ↳52 QDP
        ↳53 TransformationProof (⇔, 0 ms)
        ↳54 QDP
        ↳55 DependencyGraphProof (⇔, 0 ms)
        ↳56 QDP
        ↳57 UsableRulesProof (⇔, 0 ms)
        ↳58 QDP
        ↳59 QReductionProof (⇔, 0 ms)
        ↳60 QDP
        ↳61 QDPOrderProof (⇔, 30 ms)
        ↳62 QDP
        ↳63 DependencyGraphProof (⇔, 0 ms)
        ↳64 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 {a, b, c}

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

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

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

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

(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) 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(x3, s(x4), x5) → IF(le(x3, s(x4)), x3, s(x4), x5), IF(false, x6, x7, x8) → LOOP(x6, double(x7), s(x8)) 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, x9, x10, x11) → LOOP(x9, double(x10), s(x11)), LOOP(x12, s(x13), x14) → IF(le(x12, s(x13)), x12, s(x13), x14) which results in the following constraint:
    (1)    (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 (1) using rules (I), (II), (IV) which results in the following new constraint:
    (2)    (double(x10)=s(x13) ⇒ IF(false, x9, x10, x11)≥LOOP(x9, double(x10), s(x11)))


    We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on double(x10)=s(x13) which results in the following new constraint:
    (3)    (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 (3) using rules (I), (II), (IV) which results in the following new constraint:
    (4)    (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) = -2   
POL(double(x1)) = 2·x1   
POL(false) = 0   
POL(le(x1, x2)) = 0   
POL(s(x1)) = 1 + 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:

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

(41) Complex Obligation (AND)

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

(43) DependencyGraphProof (EQUIVALENT transformation)

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

(44) TRUE

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

(46) DependencyGraphProof (EQUIVALENT transformation)

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

(47) TRUE

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

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

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

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.

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

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

(53) TransformationProof (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(nil, y1) → IFMAP(true, nil, y1)
MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1) → MAPITER(cons(x0, x1), y1) → IFMAP(false, cons(x0, x1), y1)

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

(55) DependencyGraphProof (EQUIVALENT transformation)

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

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

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

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

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

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

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

(61) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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] to (N^2, +, *, >=, >) :

POL(MAPITER(x1, x2)) = 0 +
[0,1]
·x1 +
[0,0]
·x2

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

POL(IFMAP(x1, x2, x3)) = 1 +
[0,0]
·x1 +
[1,0]
·x2 +
[0,0]
·x3

POL(false) =
/1\
\1/

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

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

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

POL(nil) =
/0\
\0/

POL(error) =
/0\
\0/

POL(0) =
/1\
\1/

POL(logError) =
/0\
\1/

POL(s(x1)) =
/0\
\1/
 +
/11\
\11/
·x1

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

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

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

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

POL(true) =
/0\
\0/

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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

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

(63) DependencyGraphProof (EQUIVALENT transformation)

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

(64) TRUE