Term Rewriting System R:
[X, XS, N, X1, X2]
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

2ND(cons(X, XS)) -> HEAD(activate(XS))
2ND(cons(X, XS)) -> ACTIVATE(XS)
TAKE(s(N), cons(X, XS)) -> ACTIVATE(XS)
SEL(s(N), cons(X, XS)) -> SEL(N, activate(XS))
SEL(s(N), cons(X, XS)) -> ACTIVATE(XS)
ACTIVATE(nfrom(X)) -> FROM(X)
ACTIVATE(ntake(X1, X2)) -> TAKE(X1, X2)

Furthermore, R contains two SCCs.


   R
DPs
       →DP Problem 1
Forward Instantiation Transformation
       →DP Problem 2
Nar


Dependency Pairs:

TAKE(s(N), cons(X, XS)) -> ACTIVATE(XS)
ACTIVATE(ntake(X1, X2)) -> TAKE(X1, X2)


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




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

TAKE(s(N), cons(X, XS)) -> ACTIVATE(XS)
one new Dependency Pair is created:

TAKE(s(N), cons(X, ntake(X1'', X2''))) -> ACTIVATE(ntake(X1'', X2''))

The transformation is resulting in one new DP problem:



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


Dependency Pairs:

TAKE(s(N), cons(X, ntake(X1'', X2''))) -> ACTIVATE(ntake(X1'', X2''))
ACTIVATE(ntake(X1, X2)) -> TAKE(X1, X2)


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
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(ntake(X1, X2)) -> TAKE(X1, X2)
one new Dependency Pair is created:

ACTIVATE(ntake(s(N''), cons(X'', ntake(X1'''', X2'''')))) -> TAKE(s(N''), cons(X'', ntake(X1'''', X2'''')))

The transformation is resulting in one new DP problem:



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


Dependency Pairs:

ACTIVATE(ntake(s(N''), cons(X'', ntake(X1'''', X2'''')))) -> TAKE(s(N''), cons(X'', ntake(X1'''', X2'''')))
TAKE(s(N), cons(X, ntake(X1'', X2''))) -> ACTIVATE(ntake(X1'', X2''))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




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

TAKE(s(N), cons(X, ntake(X1'', X2''))) -> ACTIVATE(ntake(X1'', X2''))
one new Dependency Pair is created:

TAKE(s(N), cons(X, ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))) -> ACTIVATE(ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))

The transformation is resulting in one new DP problem:



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


Dependency Pairs:

TAKE(s(N), cons(X, ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))) -> ACTIVATE(ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))
ACTIVATE(ntake(s(N''), cons(X'', ntake(X1'''', X2'''')))) -> TAKE(s(N''), cons(X'', ntake(X1'''', X2'''')))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
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(ntake(s(N''), cons(X'', ntake(X1'''', X2'''')))) -> TAKE(s(N''), cons(X'', ntake(X1'''', X2'''')))
one new Dependency Pair is created:

ACTIVATE(ntake(s(N'''), cons(X''', ntake(s(N''''''), cons(X'''''', ntake(X1'''''''', X2'''''''')))))) -> TAKE(s(N'''), cons(X''', ntake(s(N''''''), cons(X'''''', ntake(X1'''''''', X2'''''''')))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 3
FwdInst
             ...
               →DP Problem 6
Argument Filtering and Ordering
       →DP Problem 2
Nar


Dependency Pairs:

ACTIVATE(ntake(s(N'''), cons(X''', ntake(s(N''''''), cons(X'''''', ntake(X1'''''''', X2'''''''')))))) -> TAKE(s(N'''), cons(X''', ntake(s(N''''''), cons(X'''''', ntake(X1'''''''', X2'''''''')))))
TAKE(s(N), cons(X, ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))) -> ACTIVATE(ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




The following dependency pairs can be strictly oriented:

ACTIVATE(ntake(s(N'''), cons(X''', ntake(s(N''''''), cons(X'''''', ntake(X1'''''''', X2'''''''')))))) -> TAKE(s(N'''), cons(X''', ntake(s(N''''''), cons(X'''''', ntake(X1'''''''', X2'''''''')))))
TAKE(s(N), cons(X, ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))) -> ACTIVATE(ntake(s(N''''), cons(X'''', ntake(X1'''''', X2''''''))))


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
TAKE(x1, x2) -> x2
cons(x1, x2) -> cons(x1, x2)
ACTIVATE(x1) -> x1
ntake(x1, x2) -> ntake(x1, x2)
s(x1) -> s(x1)


   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 3
FwdInst
             ...
               →DP Problem 7
Dependency Graph
       →DP Problem 2
Nar


Dependency Pair:


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Narrowing Transformation


Dependency Pair:

SEL(s(N), cons(X, XS)) -> SEL(N, activate(XS))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




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

SEL(s(N), cons(X, XS)) -> SEL(N, activate(XS))
three new Dependency Pairs are created:

SEL(s(N), cons(X, nfrom(X''))) -> SEL(N, from(X''))
SEL(s(N), cons(X, ntake(X1', X2'))) -> SEL(N, take(X1', X2'))
SEL(s(N), cons(X, XS')) -> SEL(N, XS')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Narrowing Transformation


Dependency Pairs:

SEL(s(N), cons(X, XS')) -> SEL(N, XS')
SEL(s(N), cons(X, ntake(X1', X2'))) -> SEL(N, take(X1', X2'))
SEL(s(N), cons(X, nfrom(X''))) -> SEL(N, from(X''))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




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

SEL(s(N), cons(X, nfrom(X''))) -> SEL(N, from(X''))
two new Dependency Pairs are created:

SEL(s(N), cons(X, nfrom(X'''))) -> SEL(N, cons(X''', nfrom(s(X'''))))
SEL(s(N), cons(X, nfrom(X'''))) -> SEL(N, nfrom(X'''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Nar
             ...
               →DP Problem 9
Narrowing Transformation


Dependency Pairs:

SEL(s(N), cons(X, nfrom(X'''))) -> SEL(N, cons(X''', nfrom(s(X'''))))
SEL(s(N), cons(X, ntake(X1', X2'))) -> SEL(N, take(X1', X2'))
SEL(s(N), cons(X, XS')) -> SEL(N, XS')


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




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

SEL(s(N), cons(X, ntake(X1', X2'))) -> SEL(N, take(X1', X2'))
three new Dependency Pairs are created:

SEL(s(N), cons(X, ntake(0, X2''))) -> SEL(N, nil)
SEL(s(N), cons(X, ntake(s(N''), cons(X'', XS')))) -> SEL(N, cons(X'', ntake(N'', activate(XS'))))
SEL(s(N), cons(X, ntake(X1'', X2''))) -> SEL(N, ntake(X1'', X2''))

The transformation is resulting in one new DP problem:



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


Dependency Pairs:

SEL(s(N), cons(X, ntake(s(N''), cons(X'', XS')))) -> SEL(N, cons(X'', ntake(N'', activate(XS'))))
SEL(s(N), cons(X, XS')) -> SEL(N, XS')
SEL(s(N), cons(X, nfrom(X'''))) -> SEL(N, cons(X''', nfrom(s(X'''))))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
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(s(N), cons(X, XS')) -> SEL(N, XS')
three new Dependency Pairs are created:

SEL(s(s(N'')), cons(X, cons(X'', XS'''))) -> SEL(s(N''), cons(X'', XS'''))
SEL(s(s(N'')), cons(X, cons(X'', nfrom(X''''')))) -> SEL(s(N''), cons(X'', nfrom(X''''')))
SEL(s(s(N'')), cons(X, cons(X'', ntake(s(N''''), cons(X'''', XS'''))))) -> SEL(s(N''), cons(X'', ntake(s(N''''), cons(X'''', XS'''))))

The transformation is resulting in three new DP problems:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Nar
             ...
               →DP Problem 11
Argument Filtering and Ordering


Dependency Pair:

SEL(s(N), cons(X, ntake(s(N''), cons(X'', XS')))) -> SEL(N, cons(X'', ntake(N'', activate(XS'))))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




The following dependency pair can be strictly oriented:

SEL(s(N), cons(X, ntake(s(N''), cons(X'', XS')))) -> SEL(N, cons(X'', ntake(N'', activate(XS'))))


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> x2
ntake(x1, x2) -> x1


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Nar
             ...
               →DP Problem 14
Dependency Graph


Dependency Pair:


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Nar
             ...
               →DP Problem 12
Argument Filtering and Ordering


Dependency Pair:

SEL(s(N), cons(X, nfrom(X'''))) -> SEL(N, cons(X''', nfrom(s(X'''))))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




The following dependency pair can be strictly oriented:

SEL(s(N), cons(X, nfrom(X'''))) -> SEL(N, cons(X''', nfrom(s(X'''))))


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> x2
nfrom(x1) -> nfrom


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Nar
             ...
               →DP Problem 13
Argument Filtering and Ordering


Dependency Pair:

SEL(s(s(N'')), cons(X, cons(X'', XS'''))) -> SEL(s(N''), cons(X'', XS'''))


Rules:


from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
head(cons(X, XS)) -> X
2nd(cons(X, XS)) -> head(activate(XS))
take(0, XS) -> nil
take(s(N), cons(X, XS)) -> cons(X, ntake(N, activate(XS)))
take(X1, X2) -> ntake(X1, X2)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(ntake(X1, X2)) -> take(X1, X2)
activate(X) -> X


Strategy:

innermost




The following dependency pair can be strictly oriented:

SEL(s(s(N'')), cons(X, cons(X'', XS'''))) -> SEL(s(N''), cons(X'', XS'''))


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> cons(x1, x2)

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