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
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

DBL(s(X)) -> S(ns(ndbl(activate(X))))
DBL(s(X)) -> ACTIVATE(X)
DBLS(cons(X, Y)) -> ACTIVATE(X)
DBLS(cons(X, Y)) -> ACTIVATE(Y)
SEL(0, cons(X, Y)) -> ACTIVATE(X)
SEL(s(X), cons(Y, Z)) -> SEL(activate(X), activate(Z))
SEL(s(X), cons(Y, Z)) -> ACTIVATE(X)
SEL(s(X), cons(Y, Z)) -> ACTIVATE(Z)
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)
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)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Forward Instantiation Transformation


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

DBLS(cons(X, Y)) -> ACTIVATE(X)
four new Dependency Pairs are created:

DBLS(cons(ndbls(X''), Y)) -> ACTIVATE(ndbls(X''))
DBLS(cons(nsel(X1'', X2''), Y)) -> ACTIVATE(nsel(X1'', X2''))
DBLS(cons(nindx(X1'', X2''), Y)) -> ACTIVATE(nindx(X1'', X2''))
DBLS(cons(nfrom(X''), Y)) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳Forward Instantiation Transformation


Dependency Pairs:

DBLS(cons(nfrom(X''), Y)) -> ACTIVATE(nfrom(X''))
DBLS(cons(nindx(X1'', X2''), Y)) -> ACTIVATE(nindx(X1'', X2''))
DBLS(cons(nsel(X1'', X2''), Y)) -> ACTIVATE(nsel(X1'', X2''))
DBLS(cons(ndbls(X''), Y)) -> ACTIVATE(ndbls(X''))
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)
INDX(cons(X, Y), Z) -> ACTIVATE(Y)


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

DBLS(cons(X, Y)) -> ACTIVATE(Y)
four new Dependency Pairs are created:

DBLS(cons(X, ndbls(X''))) -> ACTIVATE(ndbls(X''))
DBLS(cons(X, nsel(X1'', X2''))) -> ACTIVATE(nsel(X1'', X2''))
DBLS(cons(X, nindx(X1'', X2''))) -> ACTIVATE(nindx(X1'', X2''))
DBLS(cons(X, nfrom(X''))) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 3
                 ↳Forward Instantiation Transformation


Dependency Pairs:

DBLS(cons(X, nfrom(X''))) -> ACTIVATE(nfrom(X''))
DBLS(cons(X, nindx(X1'', X2''))) -> ACTIVATE(nindx(X1'', X2''))
DBLS(cons(X, nsel(X1'', X2''))) -> ACTIVATE(nsel(X1'', X2''))
DBLS(cons(X, ndbls(X''))) -> ACTIVATE(ndbls(X''))
DBLS(cons(nindx(X1'', X2''), Y)) -> ACTIVATE(nindx(X1'', X2''))
INDX(cons(X, Y), Z) -> ACTIVATE(Y)
INDX(cons(X, Y), Z) -> ACTIVATE(Z)
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(nsel(X1'', X2''), Y)) -> ACTIVATE(nsel(X1'', X2''))
DBLS(cons(ndbls(X''), Y)) -> ACTIVATE(ndbls(X''))
ACTIVATE(ndbls(X)) -> DBLS(X)
FROM(X) -> ACTIVATE(X)
ACTIVATE(nfrom(X)) -> FROM(X)
DBLS(cons(nfrom(X''), Y)) -> ACTIVATE(nfrom(X''))


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

SEL(0, cons(X, Y)) -> ACTIVATE(X)
four new Dependency Pairs are created:

SEL(0, cons(ndbls(X''), Y)) -> ACTIVATE(ndbls(X''))
SEL(0, cons(nsel(X1'', X2''), Y)) -> ACTIVATE(nsel(X1'', X2''))
SEL(0, cons(nindx(X1'', X2''), Y)) -> ACTIVATE(nindx(X1'', X2''))
SEL(0, cons(nfrom(X''), Y)) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 4
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

INDX(cons(X, Y), Z) -> ACTIVATE(X)
four new Dependency Pairs are created:

INDX(cons(ndbls(X''), Y), Z) -> ACTIVATE(ndbls(X''))
INDX(cons(nsel(X1'', X2''), Y), Z) -> ACTIVATE(nsel(X1'', X2''))
INDX(cons(nindx(X1'', X2''), Y), Z) -> ACTIVATE(nindx(X1'', X2''))
INDX(cons(nfrom(X''), Y), Z) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 5
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

INDX(cons(X, Y), Z) -> ACTIVATE(Z)
four new Dependency Pairs are created:

INDX(cons(X, Y), ndbls(X'')) -> ACTIVATE(ndbls(X''))
INDX(cons(X, Y), nsel(X1'', X2'')) -> ACTIVATE(nsel(X1'', X2''))
INDX(cons(X, Y), nindx(X1'', X2'')) -> ACTIVATE(nindx(X1'', X2''))
INDX(cons(X, Y), nfrom(X'')) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 6
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

INDX(cons(X, Y), Z) -> ACTIVATE(Y)
four new Dependency Pairs are created:

INDX(cons(X, ndbls(X'')), Z) -> ACTIVATE(ndbls(X''))
INDX(cons(X, nsel(X1'', X2'')), Z) -> ACTIVATE(nsel(X1'', X2''))
INDX(cons(X, nindx(X1'', X2'')), Z) -> ACTIVATE(nindx(X1'', X2''))
INDX(cons(X, nfrom(X'')), Z) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 7
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

FROM(X) -> ACTIVATE(X)
four new Dependency Pairs are created:

FROM(ndbls(X'')) -> ACTIVATE(ndbls(X''))
FROM(nsel(X1'', X2'')) -> ACTIVATE(nsel(X1'', X2''))
FROM(nindx(X1'', X2'')) -> ACTIVATE(nindx(X1'', X2''))
FROM(nfrom(X'')) -> ACTIVATE(nfrom(X''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 8
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACTIVATE(ndbls(X)) -> DBLS(X)
eight new Dependency Pairs are created:

ACTIVATE(ndbls(cons(ndbls(X''''), Y''))) -> DBLS(cons(ndbls(X''''), Y''))
ACTIVATE(ndbls(cons(nsel(X1'''', X2''''), Y''))) -> DBLS(cons(nsel(X1'''', X2''''), Y''))
ACTIVATE(ndbls(cons(nindx(X1'''', X2''''), Y''))) -> DBLS(cons(nindx(X1'''', X2''''), Y''))
ACTIVATE(ndbls(cons(nfrom(X''''), Y''))) -> DBLS(cons(nfrom(X''''), Y''))
ACTIVATE(ndbls(cons(X'', ndbls(X'''')))) -> DBLS(cons(X'', ndbls(X'''')))
ACTIVATE(ndbls(cons(X'', nsel(X1'''', X2'''')))) -> DBLS(cons(X'', nsel(X1'''', X2'''')))
ACTIVATE(ndbls(cons(X'', nindx(X1'''', X2'''')))) -> DBLS(cons(X'', nindx(X1'''', X2'''')))
ACTIVATE(ndbls(cons(X'', nfrom(X'''')))) -> DBLS(cons(X'', nfrom(X'''')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 9
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACTIVATE(nsel(X1, X2)) -> SEL(X1, X2)
four new Dependency Pairs are created:

ACTIVATE(nsel(0, cons(ndbls(X''''), Y''))) -> SEL(0, cons(ndbls(X''''), Y''))
ACTIVATE(nsel(0, cons(nsel(X1'''', X2''''), Y''))) -> SEL(0, cons(nsel(X1'''', X2''''), Y''))
ACTIVATE(nsel(0, cons(nindx(X1'''', X2''''), Y''))) -> SEL(0, cons(nindx(X1'''', X2''''), Y''))
ACTIVATE(nsel(0, cons(nfrom(X''''), Y''))) -> SEL(0, cons(nfrom(X''''), Y''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 10
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACTIVATE(nindx(X1, X2)) -> INDX(X1, X2)
12 new Dependency Pairs are created:

ACTIVATE(nindx(cons(ndbls(X''''), Y''), X2')) -> INDX(cons(ndbls(X''''), Y''), X2')
ACTIVATE(nindx(cons(nsel(X1'''', X2''''), Y''), X2')) -> INDX(cons(nsel(X1'''', X2''''), Y''), X2')
ACTIVATE(nindx(cons(nindx(X1'''', X2''''), Y''), X2')) -> INDX(cons(nindx(X1'''', X2''''), Y''), X2')
ACTIVATE(nindx(cons(nfrom(X''''), Y''), X2')) -> INDX(cons(nfrom(X''''), Y''), X2')
ACTIVATE(nindx(cons(X'', Y''), ndbls(X''''))) -> INDX(cons(X'', Y''), ndbls(X''''))
ACTIVATE(nindx(cons(X'', Y''), nsel(X1'''', X2''''))) -> INDX(cons(X'', Y''), nsel(X1'''', X2''''))
ACTIVATE(nindx(cons(X'', Y''), nindx(X1'''', X2''''))) -> INDX(cons(X'', Y''), nindx(X1'''', X2''''))
ACTIVATE(nindx(cons(X'', Y''), nfrom(X''''))) -> INDX(cons(X'', Y''), nfrom(X''''))
ACTIVATE(nindx(cons(X'', ndbls(X'''')), X2')) -> INDX(cons(X'', ndbls(X'''')), X2')
ACTIVATE(nindx(cons(X'', nsel(X1'''', X2'''')), X2')) -> INDX(cons(X'', nsel(X1'''', X2'''')), X2')
ACTIVATE(nindx(cons(X'', nindx(X1'''', X2'''')), X2')) -> INDX(cons(X'', nindx(X1'''', X2'''')), X2')
ACTIVATE(nindx(cons(X'', nfrom(X'''')), X2')) -> INDX(cons(X'', nfrom(X'''')), X2')

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 11
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACTIVATE(nfrom(X)) -> FROM(X)
four new Dependency Pairs are created:

ACTIVATE(nfrom(ndbls(X''''))) -> FROM(ndbls(X''''))
ACTIVATE(nfrom(nsel(X1'''', X2''''))) -> FROM(nsel(X1'''', X2''''))
ACTIVATE(nfrom(nindx(X1'''', X2''''))) -> FROM(nindx(X1'''', X2''''))
ACTIVATE(nfrom(nfrom(X''''))) -> FROM(nfrom(X''''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 12
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

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


Rules:


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


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:49 minutes