Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
isNat: empty set
s: {1}
length: {1}
nil: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length, U421, U521, LENGTH, U111, U211, U311} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U411, U511, U621, U611} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST, ISNATLIST, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U411(tt, V2) → U421(isNatIList(V2))
U411(tt, V2) → ISNATILIST(V2)
U511(tt, V2) → U521(isNatList(V2))
U511(tt, V2) → ISNATLIST(V2)
U611(tt, L, N) → U621(isNat(N), L)
U611(tt, L, N) → ISNAT(N)
U621(tt, L) → LENGTH(L)
ISNAT(length(V1)) → U111(isNatList(V1))
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → U211(isNat(V1))
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(V) → U311(isNatList(V))
ISNATILIST(V) → ISNATLIST(V)
ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U611(isNatList(L), L, N)
LENGTH(cons(N, L)) → ISNATLIST(L)

The collapsing dependency pairs are DPc:

U621(tt, L) → L


The hidden terms of R are:

zeros

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U621(tt, L) → U(L)
U(zeros) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 11 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U511} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U31(tt) → tt
U41(tt, x0) → U42(isNatIList(x0))
U42(tt) → tt
U61(tt, x0, x1) → U62(isNat(x1), x0)
U62(tt, x0) → s(length(x0))
isNatIList(x0) → U31(isNatList(x0))
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNat(x0), x1)
length(nil) → 0
length(cons(x0, x1)) → U61(isNatList(x1), x1, x0)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51, U511} we have µ(f) = {1}.
The symbols in {isNat, isNatList, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Matrix interpretation [3]:
Non-tuple symbols:
M( cons(x1, x2) ) =
/1\
\0/
+
/00\
\11/
·x1+
/00\
\11/
·x2

M( tt ) =
/1\
\0/

M( isNatList(x1) ) =
/1\
\0/
+
/00\
\00/
·x1

M( U52(x1) ) =
/1\
\0/
+
/00\
\00/
·x1

M( U11(x1) ) =
/1\
\0/
+
/00\
\00/
·x1

M( s(x1) ) =
/1\
\1/
+
/10\
\11/
·x1

M( isNat(x1) ) =
/0\
\0/
+
/10\
\01/
·x1

M( length(x1) ) =
/1\
\0/
+
/11\
\10/
·x1

M( 0 ) =
/1\
\0/

M( nil ) =
/0\
\0/

M( U51(x1, x2) ) =
/1\
\0/
+
/00\
\00/
·x1+
/00\
\00/
·x2

M( U21(x1) ) =
/0\
\0/
+
/10\
\00/
·x1

Tuple symbols:
M( ISNATLIST(x1) ) = 1+
[1,1]
·x1

M( U511(x1, x2) ) = 1+
[1,1]
·x1+
[1,1]
·x2

M( ISNAT(x1) ) = 1+
[1,1]
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51} we have µ(f) = {1}.
The symbols in {isNat, isNatList} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U621, U611} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

U611(tt, L, N) → U621(isNat(N), L)
U621(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U611(isNatList(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

Using the order
Polynomial Order [21,25] with Interpretation:

POL( U62(x1, x2) ) = 2x2 + 2


POL( LENGTH(x1) ) = 2x1


POL( U61(x1, ..., x3) ) = 2x1 + 2x2 + 1


POL( U621(x1, x2) ) = 2x2


POL( 0 ) = 2


POL( U51(x1, x2) ) = 2x2


POL( cons(x1, x2) ) = 2x2


POL( tt ) = 1


POL( U611(x1, ..., x3) ) = max{0, 2x1 + 2x2 - 1}


POL( isNatList(x1) ) = x1


POL( U52(x1) ) = 2x1


POL( zeros ) = max{0, -1}


POL( s(x1) ) = x1


POL( U11(x1) ) = max{0, 2x1 - 1}


POL( length(x1) ) = 2x1 + 1


POL( isNat(x1) ) = x1


POL( nil ) = 2


POL( U21(x1) ) = x1



the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt
U21(tt) → tt
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

U611(tt, L, N) → U621(isNat(N), L)

could be oriented strictly and thus removed.
The pairs

U621(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U611(isNatList(L), L, N)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U621, U611} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

U621(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U611(isNatList(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 2 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, s, length} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U62, U411} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(N), L)
U62(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U61(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U31(tt) → tt
U41(tt, x0) → U42(isNatIList(x0))
U42(tt) → tt
U61(tt, x0, x1) → U62(isNat(x1), x0)
U62(tt, x0) → s(length(x0))
isNatIList(x0) → U31(isNatList(x0))
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNat(x0), x1)
length(nil) → 0
length(cons(x0, x1)) → U61(isNatList(x1), x1, x0)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51, U411} we have µ(f) = {1}.
The symbols in {isNat, isNatList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(0) = 1   
POL(ISNATILIST(x1)) = x1   
POL(U11(x1)) = x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = x1 + x2   
POL(U51(x1, x2)) = 1   
POL(U52(x1)) = 1   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = 1 + x1   
POL(length(x1)) = 1 + x1   
POL(nil) = 1   
POL(s(x1)) = x1   
POL(tt) = 1   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52} are replacing on all positions.
For all symbols f in {cons, U51} we have µ(f) = {1}.
The symbols in {isNat, isNatList} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U11(tt) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.