Term Rewriting System R:
[X, Y, Z, X1, X2]
dbl(0) -> 0
dbl(s(X)) -> s(ns(ndbl(activate(X))))
dbl(X) -> ndbl(X)
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(ndbl(activate(X)), ndbls(activate(Y)))
dbls(X) -> ndbls(X)
sel(0, cons(X, Y)) -> activate(X)
sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z))
sel(X1, X2) -> nsel(X1, X2)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(nsel(activate(X), activate(Z)), nindx(activate(Y), activate(Z)))
indx(X1, X2) -> nindx(X1, X2)
from(X) -> cons(activate(X), nfrom(ns(activate(X))))
from(X) -> nfrom(X)
s(X) -> ns(X)
activate(ns(X)) -> s(X)
activate(ndbl(X)) -> dbl(X)
activate(ndbls(X)) -> dbls(X)
activate(nsel(X1, X2)) -> sel(X1, X2)
activate(nindx(X1, X2)) -> indx(X1, X2)
activate(nfrom(X)) -> from(X)
activate(X) -> X

Innermost Termination of R to be shown. 



   R
     ↳Removing Redundant Rules for Innermost Termination



Removing the following rules from R which left hand sides contain non normal subterms

dbl(s(X)) -> s(ns(ndbl(activate(X))))
sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z))


   R
     ↳RRRI
       →TRS2
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

DBLS(cons(X, Y)) -> ACTIVATE(X)
DBLS(cons(X, Y)) -> ACTIVATE(Y)
ACTIVATE(ns(X)) -> S(X)
ACTIVATE(ndbl(X)) -> DBL(X)
ACTIVATE(ndbls(X)) -> DBLS(X)
ACTIVATE(nsel(X1, X2)) -> SEL(X1, X2)
ACTIVATE(nindx(X1, X2)) -> INDX(X1, X2)
ACTIVATE(nfrom(X)) -> FROM(X)
SEL(0, cons(X, Y)) -> ACTIVATE(X)
INDX(cons(X, Y), Z) -> ACTIVATE(X)
INDX(cons(X, Y), Z) -> ACTIVATE(Z)
INDX(cons(X, Y), Z) -> ACTIVATE(Y)
FROM(X) -> ACTIVATE(X)

Furthermore, R contains one SCC. 


   R
     ↳RRRI
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Size-Change Principle


Dependency Pairs:

INDX(cons(X, Y), Z) -> ACTIVATE(Y)
INDX(cons(X, Y), Z) -> ACTIVATE(Z)
FROM(X) -> ACTIVATE(X)
ACTIVATE(nfrom(X)) -> FROM(X)
INDX(cons(X, Y), Z) -> ACTIVATE(X)
ACTIVATE(nindx(X1, X2)) -> INDX(X1, X2)
SEL(0, cons(X, Y)) -> ACTIVATE(X)
ACTIVATE(nsel(X1, X2)) -> SEL(X1, X2)
DBLS(cons(X, Y)) -> ACTIVATE(Y)
ACTIVATE(ndbls(X)) -> DBLS(X)
DBLS(cons(X, Y)) -> ACTIVATE(X)


Rules:


dbl(0) -> 0
dbl(X) -> ndbl(X)
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(ndbl(activate(X)), ndbls(activate(Y)))
dbls(X) -> ndbls(X)
activate(ns(X)) -> s(X)
activate(ndbl(X)) -> dbl(X)
activate(ndbls(X)) -> dbls(X)
activate(nsel(X1, X2)) -> sel(X1, X2)
activate(nindx(X1, X2)) -> indx(X1, X2)
activate(nfrom(X)) -> from(X)
activate(X) -> X
sel(0, cons(X, Y)) -> activate(X)
sel(X1, X2) -> nsel(X1, X2)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(nsel(activate(X), activate(Z)), nindx(activate(Y), activate(Z)))
indx(X1, X2) -> nindx(X1, X2)
from(X) -> cons(activate(X), nfrom(ns(activate(X))))
from(X) -> nfrom(X)
s(X) -> ns(X)





We number the DPs as follows:
  1. INDX(cons(X, Y), Z) -> ACTIVATE(Y)
  2. INDX(cons(X, Y), Z) -> ACTIVATE(Z)
  3. FROM(X) -> ACTIVATE(X)
  4. ACTIVATE(nfrom(X)) -> FROM(X)
  5. INDX(cons(X, Y), Z) -> ACTIVATE(X)
  6. ACTIVATE(nindx(X1, X2)) -> INDX(X1, X2)
  7. SEL(0, cons(X, Y)) -> ACTIVATE(X)
  8. ACTIVATE(nsel(X1, X2)) -> SEL(X1, X2)
  9. DBLS(cons(X, Y)) -> ACTIVATE(Y)
  10. ACTIVATE(ndbls(X)) -> DBLS(X)
  11. DBLS(cons(X, Y)) -> ACTIVATE(X)
and get the following Size-Change Graph(s):
{5, 2, 1} , {5, 2, 1}
1>1
{5, 2, 1} , {5, 2, 1}
2=1
{3} , {3}
1=1
{4} , {4}
1>1
{6} , {6}
1>1
1>2
{7} , {7}
2>1
{8} , {8}
1>1
1>2
{11, 9} , {11, 9}
1>1
{10} , {10}
1>1

which lead(s) to this/these maximal multigraph(s):
{8} , {7}
1>1
{5, 2, 1} , {6}
1>1
1>2
{3} , {4}
1>1
{6} , {5, 2, 1}
1>1
{11, 9} , {10}
1>1
{5, 2, 1} , {6}
2>1
2>2
{4} , {3}
1>1
{10} , {11, 9}
1>1
{7} , {8}
2>1
2>2
{4} , {5, 2, 1}
1>1
{4} , {11, 9}
1>1
{4} , {7}
1>1
{8} , {11, 9}
1>1
{6} , {7}
1>1
{10} , {7}
1>1
{8} , {3}
1>1
{6} , {11, 9}
1>1
{10} , {5, 2, 1}
1>1
{8} , {5, 2, 1}
1>1
{10} , {3}
1>1
{6} , {3}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
nfrom(x1) -> nfrom(x1)
nindx(x1, x2) -> nindx(x1, x2)
nsel(x1, x2) -> nsel(x1, x2)
cons(x1, x2) -> cons(x1, x2)
ndbls(x1) -> ndbls(x1)

We obtain no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:02 minutes