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

0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
    ↳5 QDP
        ↳6 QDPSizeChangeProof (⇔, 0 ms)
        ↳7 YES
    ↳8 QDP
        ↳9 QDPSizeChangeProof (⇔, 0 ms)
        ↳10 YES
    ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 NonLoopProof (⇔, 0 ms)
        ↳16 NO
    ↳17 QDP
        ↳18 QDPSizeChangeProof (⇔, 0 ms)
        ↳19 YES
    ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔, 0 ms)
        ↳22 YES
    ↳23 QDP
        ↳24 QDPSizeChangeProof (⇔, 0 ms)
        ↳25 YES
    ↳26 QDP
        ↳27 QDPSizeChangeProof (⇔, 0 ms)
        ↳28 YES

(0) Obligation:

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

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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:

DBL(s(X)) → DBL(X)
DBLS(cons(X, Y)) → DBL(X)
DBLS(cons(X, Y)) → DBLS(Y)
SEL(s(X), cons(Y, Z)) → SEL(X, Z)
INDX(cons(X, Y), Z) → SEL(X, Z)
INDX(cons(X, Y), Z) → INDX(Y, Z)
FROM(X) → FROM(s(X))
DBL1(s(X)) → DBL1(X)
SEL1(s(X), cons(Y, Z)) → SEL1(X, Z)
QUOTE(s(X)) → QUOTE(X)
QUOTE(dbl(X)) → DBL1(X)
QUOTE(sel(X, Y)) → SEL1(X, Y)

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 4 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
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:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

(6) 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, Z)
    The graph contains the following edges 1 > 1, 2 > 2

(7) YES

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DBL1(s(X)) → DBL1(X)

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

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

  • DBL1(s(X)) → DBL1(X)
    The graph contains the following edges 1 > 1

(10) YES

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTE(s(X)) → QUOTE(X)

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTE(s(X)) → QUOTE(X)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FROM(X) → FROM(s(X))

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

(15) NonLoopProof (EQUIVALENT transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [x0 / s(x0)] on the rule
FROM(s(x0))[ ]n[ ] → FROM(s(x0))[ ]n[x0 / s(x0)]
This rule is correct for the QDP as the following derivation shows:

intermediate steps: Equivalent (Simplify mu) - Instantiate mu - Instantiation
FROM(X)[ ]n[ ] → FROM(s(X))[ ]n[ ]
    by OriginalRule from TRS P

(16) NO

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

(18) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SEL(s(X), cons(Y, Z)) → SEL(X, Z)
    The graph contains the following edges 1 > 1, 2 > 2

(19) YES

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INDX(cons(X, Y), Z) → INDX(Y, Z)

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • INDX(cons(X, Y), Z) → INDX(Y, Z)
    The graph contains the following edges 1 > 1, 2 >= 2

(22) YES

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DBL(s(X)) → DBL(X)

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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:

  • DBL(s(X)) → DBL(X)
    The graph contains the following edges 1 > 1

(25) YES

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DBLS(cons(X, Y)) → DBLS(Y)

The TRS R consists of the following rules:

dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
from(X) → cons(X, from(s(X)))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) → X
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
quote(0) → 01
quote(s(X)) → s1(quote(X))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)

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

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

  • DBLS(cons(X, Y)) → DBLS(Y)
    The graph contains the following edges 1 > 1

(28) YES