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

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
    ↳5 QDP
        ↳6 MNOCProof (⇔)
        ↳7 QDP
        ↳8 UsableRulesProof (⇔)
        ↳9 QDP
        ↳10 QReductionProof (⇔)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 QDP
        ↳15 MNOCProof (⇔)
        ↳16 QDP
        ↳17 UsableRulesProof (⇔)
        ↳18 QDP
        ↳19 QReductionProof (⇔)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔)
        ↳22 YES
    ↳23 QDP
        ↳24 UsableRulesProof (⇔)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔)
        ↳27 YES
    ↳28 QDP
        ↳29 MNOCProof (⇔)
        ↳30 QDP
        ↳31 UsableRulesProof (⇔)
        ↳32 QDP
        ↳33 QReductionProof (⇔)
        ↳34 QDP
        ↳35 QDPSizeChangeProof (⇔)
        ↳36 YES
    ↳37 QDP
        ↳38 MNOCProof (⇔)
        ↳39 QDP
        ↳40 UsableRulesProof (⇔)
        ↳41 QDP
        ↳42 QReductionProof (⇔)
        ↳43 QDP
        ↳44 QDPSizeChangeProof (⇔)
        ↳45 YES
    ↳46 QDP
        ↳47 MNOCProof (⇔)
        ↳48 QDP
        ↳49 UsableRulesProof (⇔)
        ↳50 QDP
        ↳51 QReductionProof (⇔)
        ↳52 QDP
        ↳53 Instantiation (⇔)
        ↳54 QDP
        ↳55 Instantiation (⇔)
        ↳56 QDP
        ↳57 NonTerminationProof (⇔)
        ↳58 NO
    ↳59 QDP
        ↳60 MNOCProof (⇔)
        ↳61 QDP
        ↳62 UsableRulesProof (⇔)
        ↳63 QDP
        ↳64 QReductionProof (⇔)
        ↳65 QDP
        ↳66 QDPSizeChangeProof (⇔)
        ↳67 YES
    ↳68 QDP
        ↳69 MNOCProof (⇔)
        ↳70 QDP
        ↳71 UsableRulesProof (⇔)
        ↳72 QDP
        ↳73 QReductionProof (⇔)
        ↳74 QDP
        ↳75 QDPSizeChangeProof (⇔)
        ↳76 YES

(0) Obligation:

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

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

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

SEL(s(X), cons(Y, Z)) → SEL(X, Z)
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
FROM(X) → FROM(s(X))
SEL1(s(X), cons(Y, Z)) → SEL1(X, Z)
SEL1(0, cons(X, Z)) → QUOTE(X)
FIRST1(s(X), cons(Y, Z)) → QUOTE(Y)
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)
QUOTE1(cons(X, Z)) → QUOTE(X)
QUOTE1(cons(X, Z)) → QUOTE1(Z)
QUOTE(s(X)) → QUOTE(X)
QUOTE(sel(X, Z)) → SEL1(X, Z)
QUOTE1(first(X, Z)) → FIRST1(X, Z)
UNQUOTE(s1(X)) → UNQUOTE(X)
UNQUOTE1(cons1(X, Z)) → FCONS(unquote(X), unquote1(Z))
UNQUOTE1(cons1(X, Z)) → UNQUOTE(X)
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

UNQUOTE(s1(X)) → UNQUOTE(X)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(6) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(7) Obligation:

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

UNQUOTE(s1(X)) → UNQUOTE(X)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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:

UNQUOTE(s1(X)) → UNQUOTE(X)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(11) Obligation:

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

UNQUOTE(s1(X)) → UNQUOTE(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:

  • UNQUOTE(s1(X)) → UNQUOTE(X)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(15) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(16) Obligation:

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

UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

(18) Obligation:

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

UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(20) Obligation:

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

UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)

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

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

  • UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

SEL1(0, cons(X, Z)) → QUOTE(X)
QUOTE(s(X)) → QUOTE(X)
QUOTE(sel(X, Z)) → SEL1(X, Z)
SEL1(s(X), cons(Y, Z)) → SEL1(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(24) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(25) Obligation:

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

SEL1(0, cons(X, Z)) → QUOTE(X)
QUOTE(s(X)) → QUOTE(X)
QUOTE(sel(X, Z)) → SEL1(X, Z)
SEL1(s(X), cons(Y, Z)) → SEL1(X, 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:

  • QUOTE(sel(X, Z)) → SEL1(X, Z)
    The graph contains the following edges 1 > 1, 1 > 2

  • QUOTE(s(X)) → QUOTE(X)
    The graph contains the following edges 1 > 1

  • SEL1(s(X), cons(Y, Z)) → SEL1(X, Z)
    The graph contains the following edges 1 > 1, 2 > 2

  • SEL1(0, cons(X, Z)) → QUOTE(X)
    The graph contains the following edges 2 > 1

(27) YES

(28) Obligation:

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

FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(29) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(30) Obligation:

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

FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

(32) Obligation:

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

FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(34) Obligation:

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

FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)

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

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

  • FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)
    The graph contains the following edges 1 > 1, 2 > 2

(36) YES

(37) Obligation:

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

QUOTE1(cons(X, Z)) → QUOTE1(Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(38) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(39) Obligation:

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

QUOTE1(cons(X, Z)) → QUOTE1(Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

(41) Obligation:

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

QUOTE1(cons(X, Z)) → QUOTE1(Z)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(43) Obligation:

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

QUOTE1(cons(X, Z)) → QUOTE1(Z)

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

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

  • QUOTE1(cons(X, Z)) → QUOTE1(Z)
    The graph contains the following edges 1 > 1

(45) YES

(46) Obligation:

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

FROM(X) → FROM(s(X))

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(47) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(48) Obligation:

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

FROM(X) → FROM(s(X))

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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:

FROM(X) → FROM(s(X))

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(52) Obligation:

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

FROM(X) → FROM(s(X))

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

(53) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule FROM(X) → FROM(s(X)) we obtained the following new rules [LPAR04]:

FROM(s(z0)) → FROM(s(s(z0)))

(54) Obligation:

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

FROM(s(z0)) → FROM(s(s(z0)))

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

(55) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule FROM(s(z0)) → FROM(s(s(z0))) we obtained the following new rules [LPAR04]:

FROM(s(s(z0))) → FROM(s(s(s(z0))))

(56) Obligation:

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

FROM(s(s(z0))) → FROM(s(s(s(z0))))

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

(57) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = FROM(s(s(z0))) evaluates to t =FROM(s(s(s(z0))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [z0 / s(z0)]
  • Semiunifier: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from FROM(s(s(z0))) to FROM(s(s(s(z0)))).



(58) NO

(59) Obligation:

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

FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(60) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(61) Obligation:

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

FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

(63) Obligation:

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

FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(65) Obligation:

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

FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)

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

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

  • FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
    The graph contains the following edges 1 > 1, 2 > 2

(67) YES

(68) Obligation:

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

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

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

(69) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(70) Obligation:

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

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, Z)
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)

The set Q consists of the following terms:

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

(72) Obligation:

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

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

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

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

sel(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)
sel1(s(x0), cons(x1, x2))
sel1(0, cons(x0, x1))
first1(0, x0)
first1(s(x0), cons(x1, x2))
quote(0)
quote1(cons(x0, x1))
quote1(nil)
quote(s(x0))
quote(sel(x0, x1))
quote1(first(x0, x1))
unquote(01)
unquote(s1(x0))
unquote1(nil1)
unquote1(cons1(x0, x1))
fcons(x0, x1)

(74) Obligation:

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

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

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

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

  • SEL(s(X), cons(Y, Z)) → SEL(X, Z)
    The graph contains the following edges 1 > 1, 2 > 2

(76) YES