Termination of the following Term Rewriting System could be proven:

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}


↳ CSR
  ↳ CSDependencyPairsProof

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}

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

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(X, Z)
from(s(X))

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(X, Z)) → FIRST(X, Z)
U(from(s(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.

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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

Using the Context-Sensitive Forward Instantiation 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))



↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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

Using the Context-Sensitive Forward Instantiation 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))



↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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

The approximation of the Context-Sensitive Dependency Graph 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))). 

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                          ↳ QCSDPSubtermProof
                        ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                          ↳ QCSDPSubtermProof
                            ↳ QCSDP
                              ↳ PIsEmptyProof
                        ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

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

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

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

M( s(x1) ) =
/0\
\0/
+
/01\
\00/
·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,0]
·x2

M( QUOTE(x1) ) = 0+
[1,0]
·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))

could be oriented strictly and thus removed.
The pairs

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)
SEL1(0, cons(sel(z0, z1), y1)) → QUOTE(sel(z0, z1))

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                            ↳ QCSDP
                              ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 1 less node.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                            ↳ QCSDP
                              ↳ QCSDependencyGraphProof
                                ↳ QCSDP
                                  ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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(sel(z0, z1), y1)) → QUOTE(sel(z0, z1))
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.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(QUOTE(x1)) = 1 + 2·x1   
POL(SEL1(x1, x2)) = 2 + 2·x2   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(first(x1, x2)) = 2·x2   
POL(from(x1)) = x1   
POL(nil) = 0   
POL(s(x1)) = 0   
POL(sel(x1, x2)) = 2 + x2   

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

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

could be oriented strictly and thus removed.
The pairs

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

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                            ↳ QCSDP
                              ↳ QCSDependencyGraphProof
                                ↳ QCSDP
                                  ↳ QCSDPReductionPairProof
                                    ↳ QCSDP
                                      ↳ QCSDPSubtermProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPForwardInstantiationProcessor
              ↳ QCSDP
                ↳ QCSDPForwardInstantiationProcessor
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                            ↳ QCSDP
                              ↳ QCSDependencyGraphProof
                                ↳ QCSDP
                                  ↳ QCSDPReductionPairProof
                                    ↳ QCSDP
                                      ↳ QCSDPSubtermProof
                                        ↳ QCSDP
                                          ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

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.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP
          ↳ QCSDP

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP

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.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP

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.

The following rules are not useable 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)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP

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.

Using the order
Polynomial interpretation with max and min functions [25]:

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

the following usable rules
none

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

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

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:

The TRS P consists of the following rules:
none

R is empty.
Q is empty.

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof

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.

We use the subterm processor [20].


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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof

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.

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