(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
FIRST(0, Z) → NIL
FIRST(s(X), cons(Y, Z)) → CONS(Y, n__first(X, activate(Z)))
FIRST(s(X), cons(Y, Z)) → ACTIVATE(Z)
FROM(X) → CONS(X, n__from(s(X)))
FROM(X) → S(X)
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
SEL1(s(X), cons(Y, Z)) → ACTIVATE(Z)
SEL1(0, cons(X, Z)) → QUOTE(X)
FIRST1(s(X), cons(Y, Z)) → QUOTE(Y)
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
FIRST1(s(X), cons(Y, Z)) → ACTIVATE(Z)
QUOTE1(n__cons(X, Z)) → QUOTE(activate(X))
QUOTE1(n__cons(X, Z)) → ACTIVATE(X)
QUOTE1(n__cons(X, Z)) → QUOTE1(activate(Z))
QUOTE1(n__cons(X, Z)) → ACTIVATE(Z)
QUOTE(n__s(X)) → QUOTE(activate(X))
QUOTE(n__s(X)) → ACTIVATE(X)
QUOTE(n__sel(X, Z)) → SEL1(activate(X), activate(Z))
QUOTE(n__sel(X, Z)) → ACTIVATE(X)
QUOTE(n__sel(X, Z)) → ACTIVATE(Z)
QUOTE1(n__first(X, Z)) → FIRST1(activate(X), activate(Z))
QUOTE1(n__first(X, Z)) → ACTIVATE(X)
QUOTE1(n__first(X, Z)) → ACTIVATE(Z)
UNQUOTE(01) → 01
UNQUOTE(s1(X)) → S(unquote(X))
UNQUOTE(s1(X)) → UNQUOTE(X)
UNQUOTE1(nil1) → NIL
UNQUOTE1(cons1(X, Z)) → FCONS(unquote(X), unquote1(Z))
UNQUOTE1(cons1(X, Z)) → UNQUOTE(X)
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
FCONS(X, Z) → CONS(X, Z)
ACTIVATE(n__first(X1, X2)) → FIRST(X1, X2)
ACTIVATE(n__from(X)) → FROM(X)
ACTIVATE(n__0) → 01
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__s(X)) → S(X)
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 27 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
UNQUOTE(s1(X)) → UNQUOTE(X)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
UNQUOTE(s1(X)) → UNQUOTE(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- UNQUOTE(s1(X)) → UNQUOTE(X)
The graph contains the following edges 1 > 1
(9) TRUE
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(11) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- UNQUOTE1(cons1(X, Z)) → UNQUOTE1(Z)
The graph contains the following edges 1 > 1
(14) TRUE
(15) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__first(X1, X2)) → FIRST(X1, X2)
FIRST(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(16) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
ACTIVATE(n__first(X1, X2)) → FIRST(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(SEL(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(ACTIVATE(x1)) = | | + | | · | x1 |
POL(n__first(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(FIRST(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__sel(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(first(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(sel(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
activate(X) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
activate(n__from(X)) → from(X)
activate(n__0) → 0
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
sel(0, cons(X, Z)) → X
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
s(X) → n__s(X)
nil → n__nil
from(X) → n__from(X)
first(X1, X2) → n__first(X1, X2)
(17) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
FIRST(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(18) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(19) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(20) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 1
POL(ACTIVATE(x1)) = x1
POL(SEL(x1, x2)) = 1 + x2
POL(activate(x1)) = 1 + x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(first(x1, x2)) = 1 + x2
POL(from(x1)) = 1 + x1
POL(n__0) = 0
POL(n__cons(x1, x2)) = x1 + x2
POL(n__first(x1, x2)) = x2
POL(n__from(x1)) = x1
POL(n__nil) = 1
POL(n__s(x1)) = 0
POL(n__sel(x1, x2)) = 1 + x2
POL(nil) = 1
POL(s(x1)) = 0
POL(sel(x1, x2)) = 1 + x2
The following usable rules [FROCOS05] were oriented:
activate(X) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
activate(n__from(X)) → from(X)
activate(n__0) → 0
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
sel(0, cons(X, Z)) → X
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
s(X) → n__s(X)
nil → n__nil
from(X) → n__from(X)
first(X1, X2) → n__first(X1, X2)
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(22) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(24) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
The graph contains the following edges 1 > 1
(25) TRUE
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SEL1(0, cons(X, Z)) → QUOTE(X)
QUOTE(n__s(X)) → QUOTE(activate(X))
QUOTE(n__sel(X, Z)) → SEL1(activate(X), activate(Z))
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
SEL1(0, cons(X, Z)) → QUOTE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(SEL1(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(QUOTE(x1)) = | 0A | + | 0A | · | x1 |
POL(n__s(x1)) = | -I | + | 0A | · | x1 |
POL(activate(x1)) = | -I | + | 0A | · | x1 |
POL(n__sel(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(first(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
POL(n__first(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
POL(from(x1)) = | -I | + | 1A | · | x1 |
POL(n__from(x1)) = | -I | + | 1A | · | x1 |
POL(sel(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(n__cons(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
The following usable rules [FROCOS05] were oriented:
activate(X) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
activate(n__from(X)) → from(X)
activate(n__0) → 0
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
sel(0, cons(X, Z)) → X
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
s(X) → n__s(X)
nil → n__nil
from(X) → n__from(X)
first(X1, X2) → n__first(X1, X2)
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(X)) → QUOTE(activate(X))
QUOTE(n__sel(X, Z)) → SEL1(activate(X), activate(Z))
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 1 less node.
(30) Complex Obligation (AND)
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(32) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SEL1(s(X), cons(Y, Z)) → SEL1(X, activate(Z))
The graph contains the following edges 1 > 1
(33) TRUE
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(X)) → QUOTE(activate(X))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE(
n__s(
X)) →
QUOTE(
activate(
X)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__from(x0))) → QUOTE(from(x0))
QUOTE(n__s(n__0)) → QUOTE(0)
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(cons(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__from(x0))) → QUOTE(from(x0))
QUOTE(n__s(n__0)) → QUOTE(0)
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(cons(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE(
n__s(
n__from(
x0))) →
QUOTE(
from(
x0)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
QUOTE(n__s(n__from(x0))) → QUOTE(n__from(x0))
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__0)) → QUOTE(0)
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(cons(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
QUOTE(n__s(n__from(x0))) → QUOTE(n__from(x0))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__0)) → QUOTE(0)
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(cons(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE(
n__s(
n__0)) →
QUOTE(
0) at position [0] we obtained the following new rules [LPAR04]:
QUOTE(n__s(n__0)) → QUOTE(n__0)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(cons(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
QUOTE(n__s(n__0)) → QUOTE(n__0)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(cons(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(45) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE(
n__s(
n__cons(
x0,
x1))) →
QUOTE(
cons(
x0,
x1)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(n__cons(x0, x1))
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
QUOTE(n__s(n__cons(x0, x1))) → QUOTE(n__cons(x0, x1))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(47) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__nil)) → QUOTE(nil)
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(49) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE(
n__s(
n__nil)) →
QUOTE(
nil) at position [0] we obtained the following new rules [LPAR04]:
QUOTE(n__s(n__nil)) → QUOTE(n__nil)
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
QUOTE(n__s(n__nil)) → QUOTE(n__nil)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(51) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__s(x0))) → QUOTE(s(x0))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(53) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE(
n__s(
n__s(
x0))) →
QUOTE(
s(
x0)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE(n__s(n__s(x0))) → QUOTE(n__s(x0))
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
QUOTE(n__s(n__s(x0))) → QUOTE(n__s(x0))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(55) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
QUOTE(n__s(n__from(x0))) → QUOTE(cons(x0, n__from(s(x0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(QUOTE(x1)) = | | + | / | 0A | 0A | 0A | \ |
| | -I | -I | -I | | |
\ | -I | -I | -I | / |
| · | x1 |
POL(n__s(x1)) = | | + | / | 0A | 0A | 0A | \ |
| | 0A | 0A | 0A | | |
\ | 0A | 0A | 0A | / |
| · | x1 |
POL(n__first(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | 0A | 0A | | |
\ | -I | -I | 0A | / |
| · | x1 | + | / | -I | 0A | 0A | \ |
| | -I | 0A | 0A | | |
\ | -I | -I | 0A | / |
| · | x2 |
POL(first(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | 0A | 0A | | |
\ | -I | -I | 0A | / |
| · | x1 | + | / | -I | 0A | 0A | \ |
| | -I | 0A | 0A | | |
\ | -I | -I | 0A | / |
| · | x2 |
POL(n__sel(x1, x2)) = | | + | / | 0A | -I | -I | \ |
| | 0A | -I | 1A | | |
\ | 0A | -I | 0A | / |
| · | x1 | + | / | -I | 0A | -I | \ |
| | -I | 0A | -I | | |
\ | -I | 0A | -I | / |
| · | x2 |
POL(sel(x1, x2)) = | | + | / | 0A | -I | -I | \ |
| | 0A | -I | 1A | | |
\ | 0A | -I | 0A | / |
| · | x1 | + | / | -I | 0A | -I | \ |
| | -I | 0A | -I | | |
\ | -I | 0A | -I | / |
| · | x2 |
POL(n__from(x1)) = | | + | / | 1A | 1A | 1A | \ |
| | 0A | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x1 |
POL(cons(x1, x2)) = | | + | / | -I | 0A | -I | \ |
| | 0A | 0A | 0A | | |
\ | 0A | 0A | 0A | / |
| · | x1 | + | / | -I | -I | -I | \ |
| | -I | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x2 |
POL(s(x1)) = | | + | / | 0A | 0A | 0A | \ |
| | 0A | 0A | 0A | | |
\ | 0A | 0A | 0A | / |
| · | x1 |
POL(activate(x1)) = | | + | / | 0A | 0A | 0A | \ |
| | -I | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x1 |
POL(from(x1)) = | | + | / | 1A | 1A | 1A | \ |
| | 0A | 0A | 0A | | |
\ | 0A | 0A | 0A | / |
| · | x1 |
POL(n__cons(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | -I | 0A | | |
\ | 0A | 0A | 0A | / |
| · | x1 | + | / | -I | -I | -I | \ |
| | -I | 0A | -I | | |
\ | -I | 0A | 0A | / |
| · | x2 |
The following usable rules [FROCOS05] were oriented:
activate(X) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
activate(n__from(X)) → from(X)
activate(n__0) → 0
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(X1, X2) → n__sel(X1, X2)
sel(0, cons(X, Z)) → X
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
s(X) → n__s(X)
nil → n__nil
from(X) → n__from(X)
first(X1, X2) → n__first(X1, X2)
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__s(x0))) → QUOTE(n__s(x0))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(57) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
QUOTE(n__s(n__sel(x0, x1))) → QUOTE(sel(x0, x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(QUOTE(x1)) = | | + | / | -I | -I | 0A | \ |
| | -I | -I | -I | | |
\ | -I | -I | 0A | / |
| · | x1 |
POL(n__s(x1)) = | | + | / | -I | 0A | 0A | \ |
| | 0A | -I | 0A | | |
\ | 0A | -I | 0A | / |
| · | x1 |
POL(n__first(x1, x2)) = | | + | / | 3A | 0A | 0A | \ |
| | 3A | 1A | 3A | | |
\ | -I | 0A | -I | / |
| · | x1 | + | / | 0A | -I | 0A | \ |
| | -I | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x2 |
POL(first(x1, x2)) = | | + | / | 3A | 1A | 0A | \ |
| | 3A | 1A | 3A | | |
\ | 3A | 0A | -I | / |
| · | x1 | + | / | 0A | -I | 0A | \ |
| | -I | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x2 |
POL(n__sel(x1, x2)) = | | + | / | 2A | 2A | 0A | \ |
| | 1A | -I | 0A | | |
\ | 0A | 1A | -I | / |
| · | x1 | + | / | 1A | 1A | 1A | \ |
| | 0A | 0A | 0A | | |
\ | -I | -I | -I | / |
| · | x2 |
POL(sel(x1, x2)) = | | + | / | 2A | 2A | 0A | \ |
| | 1A | 0A | 0A | | |
\ | 1A | 1A | -I | / |
| · | x1 | + | / | 1A | 1A | 1A | \ |
| | 0A | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x2 |
POL(activate(x1)) = | | + | / | 0A | 0A | -I | \ |
| | -I | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x1 |
POL(s(x1)) = | | + | / | 0A | 0A | 0A | \ |
| | 0A | -I | 0A | | |
\ | 0A | -I | 0A | / |
| · | x1 |
POL(cons(x1, x2)) = | | + | / | 0A | 0A | 0A | \ |
| | -I | 0A | 0A | | |
\ | -I | 0A | 0A | / |
| · | x1 | + | / | -I | -I | 0A | \ |
| | 0A | -I | 0A | | |
\ | -I | 0A | -I | / |
| · | x2 |
POL(from(x1)) = | | + | / | 1A | 0A | 1A | \ |
| | 1A | 0A | 1A | | |
\ | 1A | 1A | 1A | / |
| · | x1 |
POL(n__from(x1)) = | | + | / | -I | -I | -I | \ |
| | 1A | 0A | 1A | | |
\ | -I | 1A | 0A | / |
| · | x1 |
POL(n__cons(x1, x2)) = | | + | / | 0A | 0A | 0A | \ |
| | -I | -I | -I | | |
\ | -I | 0A | 0A | / |
| · | x1 | + | / | -I | -I | 0A | \ |
| | 0A | -I | 0A | | |
\ | -I | 0A | -I | / |
| · | x2 |
The following usable rules [FROCOS05] were oriented:
activate(X) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
activate(n__from(X)) → from(X)
activate(n__0) → 0
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(X1, X2) → n__sel(X1, X2)
sel(0, cons(X, Z)) → X
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
s(X) → n__s(X)
nil → n__nil
from(X) → n__from(X)
first(X1, X2) → n__first(X1, X2)
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__s(x0))) → QUOTE(n__s(x0))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(59) NonMonReductionPairProof (EQUIVALENT transformation)
Using the following max-polynomial ordering, we can orient the general usable rules and all rules from P weakly and some rules from P strictly:
Polynomial interpretation with max [POLO,NEGPOLO,MAXPOLO]:
POL(0) = 0
POL(01) = 1
POL(QUOTE(x1)) = x1
POL(activate(x1)) = 0
POL(cons(x1, x2)) = max(0, -x1 - x2)
POL(cons1(x1, x2)) = 0
POL(fcons(x1, x2)) = max(0, -x1 - x2)
POL(first(x1, x2)) = max(0, -x1 - x2)
POL(first1(x1, x2)) = 0
POL(from(x1)) = 0
POL(n__0) = 0
POL(n__cons(x1, x2)) = 0
POL(n__first(x1, x2)) = 0
POL(n__from(x1)) = 1
POL(n__nil) = 0
POL(n__s(x1)) = 1 + x1
POL(n__sel(x1, x2)) = x2
POL(nil) = 0
POL(nil1) = 0
POL(quote(x1)) = x1
POL(quote1(x1)) = 1
POL(s(x1)) = 0
POL(s1(x1)) = x1
POL(sel(x1, x2)) = max(0, -x1 - x2)
POL(sel1(x1, x2)) = 0
POL(unquote(x1)) = 0
POL(unquote1(x1)) = 0
The following pairs can be oriented strictly and are deleted.
QUOTE(n__s(n__first(x0, x1))) → QUOTE(first(x0, x1))
QUOTE(n__s(x0)) → QUOTE(x0)
QUOTE(n__s(n__s(x0))) → QUOTE(n__s(x0))
The remaining pairs can at least be oriented weakly.
none
The following rules are usable:
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
first(X1, X2) → n__first(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
(60) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(61) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(62) TRUE
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(64) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- FIRST1(s(X), cons(Y, Z)) → FIRST1(X, activate(Z))
The graph contains the following edges 1 > 1
(65) TRUE
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(X, Z)) → QUOTE1(activate(Z))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(67) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE1(
n__cons(
X,
Z)) →
QUOTE1(
activate(
Z)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(from(x0))
QUOTE1(n__cons(y0, n__0)) → QUOTE1(0)
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(from(x0))
QUOTE1(n__cons(y0, n__0)) → QUOTE1(0)
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(69) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE1(
n__cons(
y0,
n__from(
x0))) →
QUOTE1(
from(
x0)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(n__from(x0))
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__0)) → QUOTE1(0)
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(n__from(x0))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(71) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__0)) → QUOTE1(0)
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(73) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE1(
n__cons(
y0,
n__0)) →
QUOTE1(
0) at position [0] we obtained the following new rules [LPAR04]:
QUOTE1(n__cons(y0, n__0)) → QUOTE1(n__0)
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__0)) → QUOTE1(n__0)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(75) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(77) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE1(
n__cons(
y0,
n__cons(
x0,
x1))) →
QUOTE1(
cons(
x0,
x1)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(nil)
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(79) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE1(
n__cons(
y0,
n__nil)) →
QUOTE1(
nil) at position [0] we obtained the following new rules [LPAR04]:
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(n__nil)
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
QUOTE1(n__cons(y0, n__nil)) → QUOTE1(n__nil)
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(81) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(s(x0))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(83) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QUOTE1(
n__cons(
y0,
n__s(
x0))) →
QUOTE1(
s(
x0)) at position [0] we obtained the following new rules [LPAR04]:
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(n__s(x0))
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
QUOTE1(n__cons(y0, n__s(x0))) → QUOTE1(n__s(x0))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(85) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(87) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
QUOTE1(n__cons(y0, n__sel(x0, x1))) → QUOTE1(sel(x0, x1))
QUOTE1(n__cons(y0, x0)) → QUOTE1(x0)
QUOTE1(n__cons(y0, n__cons(x0, x1))) → QUOTE1(n__cons(x0, x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 1
POL(QUOTE1(x1)) = x1
POL(activate(x1)) = 1 + x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(first(x1, x2)) = 1 + x2
POL(from(x1)) = 1 + x1
POL(n__0) = 0
POL(n__cons(x1, x2)) = 1 + x1 + x2
POL(n__first(x1, x2)) = x2
POL(n__from(x1)) = x1
POL(n__nil) = 0
POL(n__s(x1)) = 0
POL(n__sel(x1, x2)) = x2
POL(nil) = 1
POL(s(x1)) = 0
POL(sel(x1, x2)) = x2
The following usable rules [FROCOS05] were oriented:
activate(X) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
activate(n__from(X)) → from(X)
activate(n__0) → 0
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(X1, X2) → n__sel(X1, X2)
sel(0, cons(X, Z)) → X
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
s(X) → n__s(X)
nil → n__nil
from(X) → n__from(X)
first(X1, X2) → n__first(X1, X2)
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE1(n__cons(y0, n__first(x0, x1))) → QUOTE1(first(x0, x1))
QUOTE1(n__cons(y0, n__from(x0))) → QUOTE1(cons(x0, n__from(s(x0))))
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(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)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(89) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
QUOTE1(
cons(
X1,
n__from(
x0))) evaluates to t =
QUOTE1(
cons(
x0,
n__from(
s(
x0))))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [X1 / x0, x0 / s(x0)]
- Semiunifier: [ ]
Rewriting sequenceQUOTE1(cons(X1, n__from(x0))) →
QUOTE1(
n__cons(
X1,
n__from(
x0)))
with rule
cons(
X1',
X2) →
n__cons(
X1',
X2) at position [0] and matcher [
X1' /
X1,
X2 /
n__from(
x0)]
QUOTE1(n__cons(X1, n__from(x0))) →
QUOTE1(
cons(
x0,
n__from(
s(
x0))))
with rule
QUOTE1(
n__cons(
y0,
n__from(
x0))) →
QUOTE1(
cons(
x0,
n__from(
s(
x0))))
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(90) FALSE