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
Polynomial 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 pair 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'''''''')))))


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(n__take(x1, x2))=  1 + x2  
  POL(cons(x1, x2))=  x2  
  POL(TAKE(x1, x2))=  x2  
  POL(s(x1))=  0  
  POL(ACTIVATE(x1))=  x1  

resulting in one new DP problem.



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


Dependency Pair:

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




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
Polynomial 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 implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(n__from(x1))=  0  
  POL(from(x1))=  0  
  POL(activate(x1))=  0  
  POL(0)=  0  
  POL(n__take(x1, x2))=  0  
  POL(cons(x1, x2))=  0  
  POL(SEL(x1, x2))=  x1  
  POL(take(x1, x2))=  0  
  POL(nil)=  0  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   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
Polynomial 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 implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(n__from(x1))=  0  
  POL(SEL(x1, x2))=  x1  
  POL(cons(x1, x2))=  0  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 8
Nar
             ...
               →DP Problem 13
Polynomial 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 implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(SEL(x1, x2))=  x1  
  POL(cons(x1, x2))=  0  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.


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