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

0 QTRS
↳1 QTRSToCSRProof (⇔)
↳2 CSR
↳3 CSDependencyPairsProof (⇔)
↳4 QCSDP
↳5 QCSDependencyGraphProof (⇔)
↳6 AND
  ↳7 QCSDP
    ↳8 QCSDPSubtermProof (⇔)
    ↳9 QCSDP
    ↳10 PIsEmptyProof (⇔)
    ↳11 TRUE
  ↳12 QCSDP
    ↳13 QCSDPSubtermProof (⇔)
    ↳14 QCSDP
    ↳15 PIsEmptyProof (⇔)
    ↳16 TRUE
  ↳17 QCSDP
    ↳18 QCSDPSubtermProof (⇔)
    ↳19 QCSDP
    ↳20 PIsEmptyProof (⇔)
    ↳21 TRUE
  ↳22 QCSDP
    ↳23 QCSDPForwardInstantiationProcessor (⇔)
    ↳24 QCSDP
    ↳25 QCSDPForwardInstantiationProcessor (⇔)
    ↳26 QCSDP
    ↳27 QCSDependencyGraphProof (⇔)
    ↳28 AND
      ↳29 QCSDP
        ↳30 QCSDPSubtermProof (⇔)
        ↳31 QCSDP
        ↳32 PIsEmptyProof (⇔)
        ↳33 TRUE
      ↳34 QCSDP
        ↳35 QCSDPReductionPairProof (⇔)
        ↳36 QCSDP
        ↳37 QCSDependencyGraphProof (⇔)
        ↳38 QCSDP
        ↳39 QCSDPSubtermProof (⇔)
        ↳40 QCSDP
        ↳41 PIsEmptyProof (⇔)
        ↳42 TRUE
  ↳43 QCSDP
    ↳44 QCSDPSubtermProof (⇔)
    ↳45 QCSDP
    ↳46 PIsEmptyProof (⇔)
    ↳47 TRUE
  ↳48 QCSDP
    ↳49 QCSUsableRulesProof (⇔)
    ↳50 QCSDP
    ↳51 QCSDPMuMonotonicPoloProof (⇔)
    ↳52 QCSDP
    ↳53 PIsEmptyProof (⇔)
    ↳54 TRUE
  ↳55 QCSDP
    ↳56 QCSDPSubtermProof (⇔)
    ↳57 QCSDP
    ↳58 PIsEmptyProof (⇔)
    ↳59 TRUE

(0) Obligation:

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

active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(sel(0, cons(X, Z))) → mark(X)
active(first(0, Z)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(sel1(0, cons(X, Z))) → mark(quote(X))
active(first1(0, Z)) → mark(nil1)
active(first1(s(X), cons(Y, Z))) → mark(cons1(quote(Y), first1(X, Z)))
active(quote(0)) → mark(01)
active(quote1(cons(X, Z))) → mark(cons1(quote(X), quote1(Z)))
active(quote1(nil)) → mark(nil1)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(sel(X, Z))) → mark(sel1(X, Z))
active(quote1(first(X, Z))) → mark(first1(X, Z))
active(unquote(01)) → mark(0)
active(unquote(s1(X))) → mark(s(unquote(X)))
active(unquote1(nil1)) → mark(nil)
active(unquote1(cons1(X, Z))) → mark(fcons(unquote(X), unquote1(Z)))
active(fcons(X, Z)) → mark(cons(X, Z))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(s(X)) → s(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)
active(first(X1, X2)) → first(X1, active(X2))
active(from(X)) → from(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(first1(X1, X2)) → first1(active(X1), X2)
active(first1(X1, X2)) → first1(X1, active(X2))
active(cons1(X1, X2)) → cons1(active(X1), X2)
active(cons1(X1, X2)) → cons1(X1, active(X2))
active(s1(X)) → s1(active(X))
active(unquote(X)) → unquote(active(X))
active(unquote1(X)) → unquote1(active(X))
active(fcons(X1, X2)) → fcons(active(X1), X2)
active(fcons(X1, X2)) → fcons(X1, active(X2))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
s(mark(X)) → mark(s(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))
from(mark(X)) → mark(from(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
first1(mark(X1), X2) → mark(first1(X1, X2))
first1(X1, mark(X2)) → mark(first1(X1, X2))
cons1(mark(X1), X2) → mark(cons1(X1, X2))
cons1(X1, mark(X2)) → mark(cons1(X1, X2))
s1(mark(X)) → mark(s1(X))
unquote(mark(X)) → mark(unquote(X))
unquote1(mark(X)) → mark(unquote1(X))
fcons(mark(X1), X2) → mark(fcons(X1, X2))
fcons(X1, mark(X2)) → mark(fcons(X1, X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(first(X1, X2)) → first(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(from(X)) → from(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
proper(first1(X1, X2)) → first1(proper(X1), proper(X2))
proper(nil1) → ok(nil1)
proper(cons1(X1, X2)) → cons1(proper(X1), proper(X2))
proper(01) → ok(01)
proper(quote1(X)) → quote1(proper(X))
proper(s1(X)) → s1(proper(X))
proper(unquote(X)) → unquote(proper(X))
proper(unquote1(X)) → unquote1(proper(X))
proper(fcons(X1, X2)) → fcons(proper(X1), proper(X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
first(ok(X1), ok(X2)) → ok(first(X1, X2))
from(ok(X)) → ok(from(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
first1(ok(X1), ok(X2)) → ok(first1(X1, X2))
cons1(ok(X1), ok(X2)) → ok(cons1(X1, X2))
quote1(ok(X)) → ok(quote1(X))
s1(ok(X)) → ok(s1(X))
unquote(ok(X)) → ok(unquote(X))
unquote1(ok(X)) → ok(unquote1(X))
fcons(ok(X1), ok(X2)) → ok(fcons(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

(1) QTRSToCSRProof (EQUIVALENT transformation)

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

active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(sel(0, cons(X, Z))) → mark(X)
active(first(0, Z)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(sel1(0, cons(X, Z))) → mark(quote(X))
active(first1(0, Z)) → mark(nil1)
active(first1(s(X), cons(Y, Z))) → mark(cons1(quote(Y), first1(X, Z)))
active(quote(0)) → mark(01)
active(quote1(cons(X, Z))) → mark(cons1(quote(X), quote1(Z)))
active(quote1(nil)) → mark(nil1)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(sel(X, Z))) → mark(sel1(X, Z))
active(quote1(first(X, Z))) → mark(first1(X, Z))
active(unquote(01)) → mark(0)
active(unquote(s1(X))) → mark(s(unquote(X)))
active(unquote1(nil1)) → mark(nil)
active(unquote1(cons1(X, Z))) → mark(fcons(unquote(X), unquote1(Z)))
active(fcons(X, Z)) → mark(cons(X, Z))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(s(X)) → s(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(first(X1, X2)) → first(active(X1), X2)
active(first(X1, X2)) → first(X1, active(X2))
active(from(X)) → from(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(first1(X1, X2)) → first1(active(X1), X2)
active(first1(X1, X2)) → first1(X1, active(X2))
active(cons1(X1, X2)) → cons1(active(X1), X2)
active(cons1(X1, X2)) → cons1(X1, active(X2))
active(s1(X)) → s1(active(X))
active(unquote(X)) → unquote(active(X))
active(unquote1(X)) → unquote1(active(X))
active(fcons(X1, X2)) → fcons(active(X1), X2)
active(fcons(X1, X2)) → fcons(X1, active(X2))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
s(mark(X)) → mark(s(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
first(mark(X1), X2) → mark(first(X1, X2))
first(X1, mark(X2)) → mark(first(X1, X2))
from(mark(X)) → mark(from(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
first1(mark(X1), X2) → mark(first1(X1, X2))
first1(X1, mark(X2)) → mark(first1(X1, X2))
cons1(mark(X1), X2) → mark(cons1(X1, X2))
cons1(X1, mark(X2)) → mark(cons1(X1, X2))
s1(mark(X)) → mark(s1(X))
unquote(mark(X)) → mark(unquote(X))
unquote1(mark(X)) → mark(unquote1(X))
fcons(mark(X1), X2) → mark(fcons(X1, X2))
fcons(X1, mark(X2)) → mark(fcons(X1, X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(first(X1, X2)) → first(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(from(X)) → from(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
proper(first1(X1, X2)) → first1(proper(X1), proper(X2))
proper(nil1) → ok(nil1)
proper(cons1(X1, X2)) → cons1(proper(X1), proper(X2))
proper(01) → ok(01)
proper(quote1(X)) → quote1(proper(X))
proper(s1(X)) → s1(proper(X))
proper(unquote(X)) → unquote(proper(X))
proper(unquote1(X)) → unquote1(proper(X))
proper(fcons(X1, X2)) → fcons(proper(X1), proper(X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
s(ok(X)) → ok(s(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
first(ok(X1), ok(X2)) → ok(first(X1, X2))
from(ok(X)) → ok(from(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
first1(ok(X1), ok(X2)) → ok(first1(X1, X2))
cons1(ok(X1), ok(X2)) → ok(cons1(X1, X2))
quote1(ok(X)) → ok(quote1(X))
s1(ok(X)) → ok(s1(X))
unquote(ok(X)) → ok(unquote(X))
unquote1(ok(X)) → ok(unquote1(X))
fcons(ok(X1), ok(X2)) → ok(fcons(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
Special symbols used for the transformation (see [GM04]):
top: top, active: active, mark: mark, ok: ok, proper: proper
The replacement map contains the following entries:

sel: {1, 2}
s: {1}
cons: {1}
0: empty set
first: {1, 2}
nil: empty set
from: {1}
sel1: {1, 2}
quote: empty set
first1: {1, 2}
nil1: empty set
cons1: {1, 2}
01: empty set
quote1: empty set
s1: {1}
unquote: {1}
unquote1: {1}
fcons: {1, 2}
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).

(2) Obligation:

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

The replacement map contains the following entries:

sel: {1, 2}
s: {1}
cons: {1}
0: empty set
first: {1, 2}
nil: empty set
from: {1}
sel1: {1, 2}
quote: empty set
first1: {1, 2}
nil1: empty set
cons1: {1, 2}
01: empty set
quote1: empty set
s1: {1}
unquote: {1}
unquote1: {1}
fcons: {1, 2}

(3) CSDependencyPairsProof (EQUIVALENT transformation)

Using Improved CS-DPs [LPAR08] we result in the following initial Q-CSDP problem.

(4) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL, SEL1, FIRST1, UNQUOTE, FCONS, UNQUOTE1, FIRST, FROM} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE, QUOTE1, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

SEL(s(X), cons(Y, Z)) → SEL(X, Z)
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 collapsing dependency pairs are DPc:

SEL(s(X), cons(Y, Z)) → Z
SEL1(s(X), cons(Y, Z)) → Z
FIRST1(s(X), cons(Y, Z)) → Z
QUOTE(sel(X, Z)) → X
QUOTE(sel(X, Z)) → Z
QUOTE1(first(X, Z)) → X
QUOTE1(first(X, Z)) → Z


The hidden terms of R are:

first(x0, x1)
from(s(x0))

Every hiding context is built from:

first on positions {1, 2}
s on positions {1}
from on positions {1}

Hence, the new unhiding pairs DPu are :

SEL(s(X), cons(Y, Z)) → U(Z)
SEL1(s(X), cons(Y, Z)) → U(Z)
FIRST1(s(X), cons(Y, Z)) → U(Z)
QUOTE(sel(X, Z)) → U(X)
QUOTE(sel(X, Z)) → U(Z)
QUOTE1(first(X, Z)) → U(X)
QUOTE1(first(X, Z)) → U(Z)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(first(x0, x1)) → FIRST(x0, x1)
U(from(s(x0))) → FROM(s(x0))

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.

(5) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 7 SCCs with 14 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, U} are not replacing on any position.

The TRS P consists of the following rules:

U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)

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.

(8) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order

(9) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(10) PIsEmptyProof (EQUIVALENT transformation)

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

(11) TRUE

(12) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, UNQUOTE} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

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.

(13) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


UNQUOTE(s1(X)) → UNQUOTE(X)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
UNQUOTE(x1)  =  x1

Subterm Order

(14) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(15) PIsEmptyProof (EQUIVALENT transformation)

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

(16) TRUE

(17) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, UNQUOTE1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

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.

(18) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
UNQUOTE1(x1)  =  x1

Subterm Order

(19) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(20) PIsEmptyProof (EQUIVALENT transformation)

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

(21) TRUE

(22) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE} are not replacing on any position.

The TRS P consists of the following rules:

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

(23) QCSDPForwardInstantiationProcessor (EQUIVALENT transformation)

Using the Context-Sensitive Forward Instantiation[DA_EMMES] Processor
the pair SEL1(0, cons(X, Z)) → QUOTE(X)
was transformed to the following new pairs:

SEL1(0, cons(s(z0), y1)) → QUOTE(s(z0))
SEL1(0, cons(sel(z0, z1), y1)) → QUOTE(sel(z0, z1))

(24) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE} are not replacing on any position.

The TRS P consists of the following rules:

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

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.

(25) QCSDPForwardInstantiationProcessor (EQUIVALENT transformation)

Using the Context-Sensitive Forward Instantiation[DA_EMMES] Processor
the pair QUOTE(s(X)) → QUOTE(X)
was transformed to the following new pairs:

QUOTE(s(s(z0))) → QUOTE(s(z0))
QUOTE(s(sel(z0, z1))) → QUOTE(sel(z0, z1))

(26) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE} are not replacing on any position.

The TRS P consists of the following rules:

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

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.

(27) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 2 SCCs.
The rules QUOTE(s(s(z0))) → QUOTE(s(z0)) and QUOTE(sel(x0, x1)) → SEL1(x0, x1) form no chain, because ECapµ(QUOTE(s(z0))) = QUOTE(s(z0)) does not unify with QUOTE(sel(x0, x1)). The rules QUOTE(s(sel(z0, z1))) → QUOTE(sel(z0, z1)) and QUOTE(s(sel(x0, x1))) → QUOTE(sel(x0, x1)) form no chain, because ECapµ(QUOTE(sel(z0, z1))) = QUOTE(sel(z0, z1)) does not unify with QUOTE(s(sel(x0, x1))).

(28) Complex Obligation (AND)

(29) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE} are not replacing on any position.

The TRS P consists of the following rules:

QUOTE(s(s(z0))) → QUOTE(s(z0))

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.

(30) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


QUOTE(s(s(z0))) → QUOTE(s(z0))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
QUOTE(x1)  =  x1

Subterm Order

(31) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(32) PIsEmptyProof (EQUIVALENT transformation)

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

(33) TRUE

(34) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE} are not replacing on any position.

The TRS P consists of the following rules:

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

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.

(35) QCSDPReductionPairProof (EQUIVALENT transformation)

Using the order
Matrix interpretation [MATRO]:
Non-tuple symbols:
M( sel(x1, x2) ) =
/1\
\0/
+
/00\
\00/
·x1+
/11\
\11/
·x2

M( cons(x1, x2) ) =
/0\
\0/
+
/11\
\00/
·x1+
/01\
\10/
·x2

M( from(x1) ) =
/0\
\0/
+
/11\
\10/
·x1

M( s(x1) ) =
/0\
\0/
+
/00\
\10/
·x1

M( 0 ) =
/0\
\0/

M( first(x1, x2) ) =
/0\
\0/
+
/00\
\00/
·x1+
/10\
\01/
·x2

M( nil ) =
/0\
\0/

Tuple symbols:
M( SEL1(x1, x2) ) = 0+
[0,0]
·x1+
[1,1]
·x2

M( QUOTE(x1) ) = 0+
[0,1]
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


the following usable 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)))

could all be oriented weakly.
Furthermore, the pairs

QUOTE(s(sel(z0, z1))) → QUOTE(sel(z0, z1))
SEL1(0, cons(sel(z0, z1), y1)) → QUOTE(sel(z0, z1))

could be oriented strictly and thus removed by the CS-Reduction Pair Processor [LPAR08,DA_EMMES].

(36) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE} are not replacing on any position.

The TRS P consists of the following rules:

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

(37) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 1 SCC with 2 less nodes.

(38) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:

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.

(39) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


SEL1(s(X), cons(Y, Z)) → SEL1(X, Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SEL1(x1, x2)  =  x1

Subterm Order

(40) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(41) PIsEmptyProof (EQUIVALENT transformation)

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

(42) TRUE

(43) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, FIRST1} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

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.

(44) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


FIRST1(s(X), cons(Y, Z)) → FIRST1(X, Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
FIRST1(x1, x2)  =  x1

Subterm Order

(45) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(46) PIsEmptyProof (EQUIVALENT transformation)

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

(47) TRUE

(48) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1, QUOTE1} are not replacing on any position.

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.

(49) QCSUsableRulesProof (EQUIVALENT transformation)

The following rules are not useable [DA_EMMES] and can be deleted:

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

(50) Obligation:

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {QUOTE1} are not replacing on any position.

The TRS P consists of the following rules:

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

R is empty.
Q is empty.

(51) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

By using the following µ-monotonic polynomial ordering [POLO], at least one Dependency Pair or term rewrite system rule of this Q-CSDP problem can be strictly oriented and thus deleted.
Strictly oriented dependency pairs:

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


Used ordering: POLO with Polynomial interpretation [POLO]:

POL(QUOTE1(x1)) = 2·x1   
POL(cons(x1, x2)) = 1 + x1 + 2·x2   

(52) Obligation:

Q-restricted context-sensitive dependency pair problem:

The TRS P consists of the following rules:
none

R is empty.
Q is empty.

(53) PIsEmptyProof (EQUIVALENT transformation)

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

(54) TRUE

(55) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons, SEL} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

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.

(56) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].


The following pairs can be oriented strictly and are deleted.


SEL(s(X), cons(Y, Z)) → SEL(X, Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SEL(x1, x2)  =  x1

Subterm Order

(57) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {sel, s, first, from, sel1, first1, cons1, s1, unquote, unquote1, fcons} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {quote, quote1} are not replacing on any position.

The TRS P consists of the following rules:
none

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.

(58) PIsEmptyProof (EQUIVALENT transformation)

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

(59) TRUE