Term Rewriting System R:
[Z, X, Y, X1, X2]
fst(0, Z) -> nil
fst(s(X), cons(Y, Z)) -> cons(Y, nfst(activate(X), activate(Z)))
fst(X1, X2) -> nfst(X1, X2)
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
len(nil) -> 0
len(cons(X, Z)) -> s(nlen(activate(Z)))
len(X) -> nlen(X)
activate(nfst(X1, X2)) -> fst(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nlen(X)) -> len(X)
activate(X) -> X

Termination of R to be shown.

R
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

fst(0, Z) -> nil
len(nil) -> 0

where the Polynomial interpretation:
 POL(from(x1)) =  2·x1 POL(activate(x1)) =  2·x1 POL(len(x1)) =  2·x1 POL(n__fst(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  2·x1 + x2 POL(n__from(x1)) =  x1 POL(0) =  1 POL(cons(x1, x2)) =  x1 + x2 POL(nil) =  1 POL(fst(x1, x2)) =  2·x1 + 2·x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  x1 POL(n__add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

where the Polynomial interpretation:
 POL(n__from(x1)) =  x1 POL(from(x1)) =  2·x1 POL(activate(x1)) =  2·x1 POL(len(x1)) =  2·x1 POL(cons(x1, x2)) =  x1 + x2 POL(n__fst(x1, x2)) =  x1 + x2 POL(s(x1)) =  x1 POL(fst(x1, x2)) =  2·x1 + 2·x2 POL(n__len(x1)) =  x1 POL(n__add(x1, x2)) =  1 + x1 + x2 POL(add(x1, x2)) =  2 + 2·x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

activate(nlen(X)) -> len(X)

where the Polynomial interpretation:
 POL(n__from(x1)) =  x1 POL(from(x1)) =  2·x1 POL(activate(x1)) =  2·x1 POL(len(x1)) =  1 + 2·x1 POL(cons(x1, x2)) =  x1 + x2 POL(n__fst(x1, x2)) =  x1 + x2 POL(fst(x1, x2)) =  2·x1 + 2·x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  1 + x1 POL(n__add(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS4
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

where the Polynomial interpretation:
 POL(n__from(x1)) =  x1 POL(from(x1)) =  2·x1 POL(activate(x1)) =  2·x1 POL(cons(x1, x2)) =  x1 + x2 POL(len(x1)) =  2·x1 POL(n__fst(x1, x2)) =  x1 + x2 POL(fst(x1, x2)) =  2·x1 + 2·x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  x1 POL(n__add(x1, x2)) =  1 + x1 + x2 POL(add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS5
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

fst(X1, X2) -> nfst(X1, X2)
fst(s(X), cons(Y, Z)) -> cons(Y, nfst(activate(X), activate(Z)))

where the Polynomial interpretation:
 POL(from(x1)) =  2·x1 POL(n__from(x1)) =  x1 POL(activate(x1)) =  2·x1 POL(cons(x1, x2)) =  x1 + x2 POL(len(x1)) =  2·x1 POL(n__fst(x1, x2)) =  1 + x1 + x2 POL(fst(x1, x2)) =  2 + 2·x1 + 2·x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS6
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
activate(X) -> X
activate(nfst(X1, X2)) -> fst(X1, X2)
len(X) -> nlen(X)

where the Polynomial interpretation:
 POL(from(x1)) =  1 + 2·x1 POL(n__from(x1)) =  x1 POL(activate(x1)) =  1 + 2·x1 POL(len(x1)) =  1 + 2·x1 POL(cons(x1, x2)) =  x1 + x2 POL(n__fst(x1, x2)) =  x1 + x2 POL(fst(x1, x2)) =  x1 + x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS7
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

activate(nfrom(X)) -> from(X)

where the Polynomial interpretation:
 POL(n__from(x1)) =  1 + x1 POL(from(x1)) =  x1 POL(activate(x1)) =  x1 POL(len(x1)) =  x1 POL(cons(x1, x2)) =  x1 + x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS8
Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

len(cons(X, Z)) -> s(nlen(activate(Z)))

where the Polynomial interpretation:
 POL(activate(x1)) =  x1 POL(len(x1)) =  1 + x1 POL(cons(x1, x2)) =  x1 + x2 POL(s(x1)) =  x1 POL(n__len(x1)) =  x1
was used.

All Rules of R can be deleted.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS9
Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

R
RRRPolo
→TRS2
RRRPolo
→TRS3
RRRPolo
...
→TRS10
Dependency Pair Analysis

R contains no Dependency Pairs and therefore no SCCs.

Termination of R successfully shown.
Duration:
0:00 minutes