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 TRUE
  ↳14 QDP
    ↳15 MNOCProof (⇔)
    ↳16 QDP
    ↳17 UsableRulesProof (⇔)
    ↳18 QDP
    ↳19 QReductionProof (⇔)
    ↳20 QDP
    ↳21 QDPSizeChangeProof (⇔)
    ↳22 TRUE
  ↳23 QDP
    ↳24 UsableRulesProof (⇔)
    ↳25 QDP
    ↳26 QDPSizeChangeProof (⇔)
    ↳27 TRUE
  ↳28 QDP
    ↳29 MNOCProof (⇔)
    ↳30 QDP
    ↳31 UsableRulesProof (⇔)
    ↳32 QDP
    ↳33 QReductionProof (⇔)
    ↳34 QDP
    ↳35 QDPSizeChangeProof (⇔)
    ↳36 TRUE
  ↳37 QDP
    ↳38 MNOCProof (⇔)
    ↳39 QDP
    ↳40 UsableRulesProof (⇔)
    ↳41 QDP
    ↳42 QReductionProof (⇔)
    ↳43 QDP
    ↳44 QDPSizeChangeProof (⇔)
    ↳45 TRUE
  ↳46 QDP
    ↳47 MNOCProof (⇔)
    ↳48 QDP
    ↳49 UsableRulesProof (⇔)
    ↳50 QDP
    ↳51 QReductionProof (⇔)
    ↳52 QDP
      ↳53 Instantiation (⇔)
        ↳54 QDP
      ↳55 Instantiation (⇔)
        ↳56 QDP
        ↳57 Instantiation (⇔)
        ↳58 QDP
        ↳59 NonTerminationProof (⇔)
        ↳60 FALSE
  ↳61 QDP
    ↳62 MNOCProof (⇔)
    ↳63 QDP
    ↳64 UsableRulesProof (⇔)
    ↳65 QDP
    ↳66 QReductionProof (⇔)
    ↳67 QDP
    ↳68 QDPSizeChangeProof (⇔)
    ↳69 TRUE
  ↳70 QDP
    ↳71 MNOCProof (⇔)
    ↳72 QDP
    ↳73 UsableRulesProof (⇔)
    ↳74 QDP
    ↳75 QReductionProof (⇔)
    ↳76 QDP
    ↳77 QDPSizeChangeProof (⇔)
    ↳78 TRUE

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

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

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

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

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

(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(X) → FROM(s(X)) we obtained the following new rules [LPAR04]:

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

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

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

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

(59) 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:
  • Semiunifier: [ ]
  • Matcher: [z0 / s(z0)]



Rewriting sequence

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



(60) FALSE

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

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

(62) MNOCProof (EQUIVALENT transformation)

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

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

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

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

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

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

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

(69) TRUE

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

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

(71) MNOCProof (EQUIVALENT transformation)

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

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

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

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

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

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

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

(78) TRUE