(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:
properThe 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 DP
o 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 DP
c:
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 DP
u 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) ) = | | + | | · | x1 | + | | · | x2 |
M( cons(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
M( first(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( SEL1(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
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