Termination proof of /tmp/tmpSjUnNc/LengthOfFiniteLists

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, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, and, U11¹, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, ISNAT, ISNATILIST, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U11¹(tt, L) → LENGTH(L)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(V) → ISNATLIST(V)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
LENGTH(cons(N, L)) → AND(isNatList(L), isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(L)

The collapsing dependency pairs are DP_c:

U11¹(tt, L) → L
AND(tt, X) → X

The hidden terms of R are:

zeros
isNatIList(V2)
isNatList(V2)

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

U11¹(tt, L) → U(L)
AND(tt, X) → U(X)
U(zeros) → ZEROS
U(isNatIList(V2)) → ISNATILIST(V2)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

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

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = x₁
POL(ISNATLIST(x₁)) = x₁
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = 1 + x₂
POL(and(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 1 + x₁
POL(nil) = 1
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0

the following usable rules

isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

ISNAT(length(V1)) → ISNATLIST(V1)

could be oriented strictly and thus removed.
The pairs

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatList(V2)) → ISNATLIST(V2)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                      ↳ QCSDPSubtermProof

                    ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

ISNAT(s(V1)) → ISNAT(V1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ISNAT(x1) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                      ↳ QCSDPSubtermProof

                        ↳ QCSDP

                          ↳ PIsEmptyProof

                    ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

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

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNATILIST(x₁)) = 1 + x₁
POL(ISNATLIST(x₁)) = x₁
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = x₂
POL(and(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0

the following usable rules

isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

ISNATILIST(V) → ISNATLIST(V)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

                        ↳ QCSDP

                          ↳ QCSDPInstantiationProcessor

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

Using the Context-Sensitive Instantiation Processor
the pair AND(tt, X) → U(X)
was transformed to the following new pairs:

AND(tt, isNatList(z1)) → U(isNatList(z1))
AND(tt, isNatIList(z1)) → U(isNatIList(z1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

                        ↳ QCSDP

                          ↳ QCSDPInstantiationProcessor

                            ↳ QCSDP

                              ↳ QCSDependencyGraphProof

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

U(isNatList(V2)) → ISNATLIST(V2)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, isNatIList(z1)) → U(isNatIList(z1))
AND(tt, isNatList(z1)) → U(isNatList(z1))
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs.
The rules ISNATILIST(cons(z0, z1)) → AND(isNat(z0), isNatIList(z1)) and AND(tt, isNatList(x0)) → U(isNatList(x0)) form no chain, because ECap^µ(AND(isNat(z0), isNatIList(z1))) = AND(x_1, isNatIList(z1)) does not unify with AND(tt, isNatList(x0)). The rules AND(tt, isNatList(z0)) → U(isNatList(z0)) and U(isNatIList(x0)) → ISNATILIST(x0) form no chain, because ECap^µ(U(isNatList(z0))) = U(isNatList(z0)) does not unify with U(isNatIList(x0)). The rules ISNATLIST(cons(z0, z1)) → AND(isNat(z0), isNatList(z1)) and AND(tt, isNatIList(x0)) → U(isNatIList(x0)) form no chain, because ECap^µ(AND(isNat(z0), isNatList(z1))) = AND(x_1, isNatList(z1)) does not unify with AND(tt, isNatIList(x0)). The rules AND(tt, isNatIList(z0)) → U(isNatIList(z0)) and U(isNatList(x0)) → ISNATLIST(x0) form no chain, because ECap^µ(U(isNatIList(z0))) = U(isNatIList(z0)) does not unify with U(isNatList(x0)).

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

                        ↳ QCSDP

                          ↳ QCSDPInstantiationProcessor

                            ↳ QCSDP

                              ↳ QCSDependencyGraphProof

                                ↳ AND

                                  ↳ QCSDP

                                    ↳ QCSDPForwardInstantiationProcessor

                                  ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, isNatList(z1)) → U(isNatList(z1))
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

Using the Context-Sensitive Forward Instantiation Processor
the pair U(isNatList(V2)) → ISNATLIST(V2)
was transformed to the following new pairs:

U(isNatList(cons(z0, z1))) → ISNATLIST(cons(z0, z1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

                        ↳ QCSDP

                          ↳ QCSDPInstantiationProcessor

                            ↳ QCSDP

                              ↳ QCSDependencyGraphProof

                                ↳ AND

                                  ↳ QCSDP

                                    ↳ QCSDPForwardInstantiationProcessor

                                      ↳ QCSDP

                                        ↳ QCSDPForwardInstantiationProcessor

                                  ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

U(isNatList(cons(z0, z1))) → ISNATLIST(cons(z0, z1))
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, isNatList(z1)) → U(isNatList(z1))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

Using the Context-Sensitive Forward Instantiation Processor
the pair AND(tt, isNatList(z1)) → U(isNatList(z1))
was transformed to the following new pairs:

AND(tt, isNatList(cons(z0, z1))) → U(isNatList(cons(z0, z1)))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

                        ↳ QCSDP

                          ↳ QCSDPInstantiationProcessor

                            ↳ QCSDP

                              ↳ QCSDependencyGraphProof

                                ↳ AND

                                  ↳ QCSDP

                                    ↳ QCSDPForwardInstantiationProcessor

                                      ↳ QCSDP

                                        ↳ QCSDPForwardInstantiationProcessor

                                          ↳ QCSDP

                                  ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

U(isNatList(cons(z0, z1))) → ISNATLIST(cons(z0, z1))
AND(tt, isNatList(cons(z0, z1))) → U(isNatList(cons(z0, z1)))
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPReductionPairProof

                        ↳ QCSDP

                          ↳ QCSDPInstantiationProcessor

                            ↳ QCSDP

                              ↳ QCSDependencyGraphProof

                                ↳ AND

                                  ↳ QCSDP

                                  ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, isNatIList(z1)) → U(isNatIList(z1))
U(isNatIList(V2)) → ISNATILIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
U11¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)

Q is empty.

We applied the Zantema transformation [34] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(lengthInact(V1)) → isNatList(a(V1))
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(nilInact) → tt
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(lengthInact(V1)) → isNatList(a(V1))
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(nilInact) → tt
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNatList(nilInact) → tt
length(nil) → 0

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListInact(x₁)) = x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListInact(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(lengthInact(x₁)) = 2·x₁
POL(nil) = 1
POL(nilInact) = 1
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(lengthInact(V1)) → isNatList(a(V1))
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(lengthInact(V1)) → isNatList(a(V1))
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNat(lengthInact(V1)) → isNatList(a(V1))

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(U11(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 2·x₁
POL(isNatIListInact(x₁)) = 2·x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = 2·x₁
POL(isNatListInact(x₁)) = 2·x₁
POL(length(x₁)) = 1 + 2·x₁
POL(lengthInact(x₁)) = 1 + 2·x₁
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNatIList(V) → isNatList(a(V))
isNatIList(zerosInact) → tt

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(U11(x₁, x₂)) = 2·x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + 2·x₁
POL(isNatIListInact(x₁)) = 1 + 2·x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListInact(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(lengthInact(x₁)) = 2·x₁
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

A(nilInact) → NIL
AND(tt, X) → A(X)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
U11¹(tt, L) → S(length(a(L)))
LENGTH(cons(N, L)) → U11¹(and(isNatList(a(L)), isNatInact(N)), a(L))
ISNATLIST(consInact(V1, V2)) → A(V2)
LENGTH(cons(N, L)) → ISNATLIST(a(L))
ISNATILIST(consInact(V1, V2)) → A(V1)
A(isNatIListInact(x1)) → ISNATILIST(x1)
A(isNatInact(x1)) → ISNAT(x1)
LENGTH(cons(N, L)) → AND(isNatList(a(L)), isNatInact(N))
A(sInact(x1)) → S(x1)
ISNATILIST(consInact(V1, V2)) → ISNAT(a(V1))
ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
A(consInact(x1, x2)) → CONS(x1, x2)
LENGTH(cons(N, L)) → A(L)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
ISNATILIST(consInact(V1, V2)) → A(V2)
A(0Inact) → 0¹
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
ISNATLIST(consInact(V1, V2)) → A(V1)
A(zerosInact) → ZEROS
U11¹(tt, L) → LENGTH(a(L))
ZEROS → CONS(0, zerosInact)
U11¹(tt, L) → A(L)
A(isNatListInact(x1)) → ISNATLIST(x1)
A(lengthInact(x1)) → LENGTH(x1)
ZEROS → 0¹

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

A(nilInact) → NIL
AND(tt, X) → A(X)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
U11¹(tt, L) → S(length(a(L)))
LENGTH(cons(N, L)) → U11¹(and(isNatList(a(L)), isNatInact(N)), a(L))
ISNATLIST(consInact(V1, V2)) → A(V2)
LENGTH(cons(N, L)) → ISNATLIST(a(L))
ISNATILIST(consInact(V1, V2)) → A(V1)
A(isNatIListInact(x1)) → ISNATILIST(x1)
A(isNatInact(x1)) → ISNAT(x1)
LENGTH(cons(N, L)) → AND(isNatList(a(L)), isNatInact(N))
A(sInact(x1)) → S(x1)
ISNATILIST(consInact(V1, V2)) → ISNAT(a(V1))
ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
A(consInact(x1, x2)) → CONS(x1, x2)
LENGTH(cons(N, L)) → A(L)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
ISNATILIST(consInact(V1, V2)) → A(V2)
A(0Inact) → 0¹
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
ISNATLIST(consInact(V1, V2)) → A(V1)
A(zerosInact) → ZEROS
U11¹(tt, L) → LENGTH(a(L))
ZEROS → CONS(0, zerosInact)
U11¹(tt, L) → A(L)
A(isNatListInact(x1)) → ISNATLIST(x1)
A(lengthInact(x1)) → LENGTH(x1)
ZEROS → 0¹

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 8 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
ISNATILIST(consInact(V1, V2)) → ISNAT(a(V1))
LENGTH(cons(N, L)) → A(L)
AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
ISNATILIST(consInact(V1, V2)) → A(V2)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
ISNATLIST(consInact(V1, V2)) → A(V1)
LENGTH(cons(N, L)) → U11¹(and(isNatList(a(L)), isNatInact(N)), a(L))
ISNATLIST(consInact(V1, V2)) → A(V2)
LENGTH(cons(N, L)) → ISNATLIST(a(L))
U11¹(tt, L) → LENGTH(a(L))
ISNATILIST(consInact(V1, V2)) → A(V1)
A(isNatIListInact(x1)) → ISNATILIST(x1)
U11¹(tt, L) → A(L)
A(isNatListInact(x1)) → ISNATLIST(x1)
A(isNatInact(x1)) → ISNAT(x1)
A(lengthInact(x1)) → LENGTH(x1)
LENGTH(cons(N, L)) → AND(isNatList(a(L)), isNatInact(N))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISNATILIST(consInact(V1, V2)) → ISNAT(a(V1))
ISNATILIST(consInact(V1, V2)) → A(V2)
ISNATILIST(consInact(V1, V2)) → A(V1)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₁ + x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 1 + 2·x₁
POL(ISNATLIST(x₁)) = x₁
POL(LENGTH(x₁)) = x₁
POL(U11(x₁, x₂)) = x₁ + x₂
POL(U11¹(x₁, x₂)) = x₁ + x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(consInact(x₁, x₂)) = x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + 2·x₁
POL(isNatIListInact(x₁)) = 1 + 2·x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListInact(x₁)) = x₁
POL(length(x₁)) = x₁
POL(lengthInact(x₁)) = x₁
POL(nil) = 1
POL(nilInact) = 1
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
LENGTH(cons(N, L)) → A(L)
AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
ISNATLIST(consInact(V1, V2)) → A(V1)
LENGTH(cons(N, L)) → U11¹(and(isNatList(a(L)), isNatInact(N)), a(L))
ISNATLIST(consInact(V1, V2)) → A(V2)
LENGTH(cons(N, L)) → ISNATLIST(a(L))
U11¹(tt, L) → LENGTH(a(L))
A(isNatIListInact(x1)) → ISNATILIST(x1)
U11¹(tt, L) → A(L)
A(isNatInact(x1)) → ISNAT(x1)
A(isNatListInact(x1)) → ISNATLIST(x1)
LENGTH(cons(N, L)) → AND(isNatList(a(L)), isNatInact(N))
A(lengthInact(x1)) → LENGTH(x1)

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

A(lengthInact(x1)) → LENGTH(x1)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = 2·x₁ + x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 2·x₁
POL(ISNATLIST(x₁)) = x₁
POL(LENGTH(x₁)) = 2·x₁
POL(U11(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U11¹(x₁, x₂)) = x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 2·x₁
POL(isNatIListInact(x₁)) = 2·x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = 2·x₁
POL(isNatListInact(x₁)) = 2·x₁
POL(length(x₁)) = 1 + 2·x₁
POL(lengthInact(x₁)) = 1 + 2·x₁
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
LENGTH(cons(N, L)) → A(L)
AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
ISNATLIST(consInact(V1, V2)) → A(V1)
LENGTH(cons(N, L)) → U11¹(and(isNatList(a(L)), isNatInact(N)), a(L))
ISNATLIST(consInact(V1, V2)) → A(V2)
LENGTH(cons(N, L)) → ISNATLIST(a(L))
U11¹(tt, L) → LENGTH(a(L))
A(isNatIListInact(x1)) → ISNATILIST(x1)
U11¹(tt, L) → A(L)
A(isNatListInact(x1)) → ISNATLIST(x1)
A(isNatInact(x1)) → ISNAT(x1)
LENGTH(cons(N, L)) → AND(isNatList(a(L)), isNatInact(N))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
ISNATLIST(consInact(V1, V2)) → A(V1)
ISNATLIST(consInact(V1, V2)) → A(V2)
AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
A(isNatInact(x1)) → ISNAT(x1)
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(consInact(V1, V2)) → ISNAT(a(V1))
ISNATLIST(consInact(V1, V2)) → A(V1)
ISNATLIST(consInact(V1, V2)) → A(V2)

The remaining pairs can at least be oriented weakly.

AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
A(isNatInact(x1)) → ISNAT(x1)
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 0
POL(ISNATLIST(x₁)) = 1 + x₁
POL(U11(x₁, x₂)) = 0
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(consInact(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 0
POL(isNatIListInact(x₁)) = 0
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = 1 + x₁
POL(isNatListInact(x₁)) = 1 + x₁
POL(length(x₁)) = 0
POL(lengthInact(x₁)) = 0
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

The following usable rules [17] were oriented:

isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
a(isNatListInact(x1)) → isNatList(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
and(tt, X) → a(X)
zeros → zerosInact
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(x) → x
cons(x1, x2) → consInact(x1, x2)
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
isNat(sInact(V1)) → isNat(a(V1))
isNat(0Inact) → tt
zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
a(nilInact) → nil
0 → 0Inact
a(lengthInact(x1)) → length(x1)
nil → nilInact
a(0Inact) → 0
isNat(x1) → isNatInact(x1)
a(sInact(x1)) → s(x1)
length(x1) → lengthInact(x1)
a(isNatInact(x1)) → isNat(x1)
isNatIList(x1) → isNatIListInact(x1)
a(zerosInact) → zeros
s(x1) → sInact(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNAT(sInact(V1)) → A(V1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
A(isNatListInact(x1)) → ISNATLIST(x1)
A(isNatInact(x1)) → ISNAT(x1)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNAT(sInact(V1)) → A(V1)

The remaining pairs can at least be oriented weakly.

AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
A(isNatListInact(x1)) → ISNATLIST(x1)
A(isNatInact(x1)) → ISNAT(x1)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = 1 + x₁
POL(ISNATILIST(x₁)) = 0
POL(ISNATLIST(x₁)) = 0
POL(U11(x₁, x₂)) = 0
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = 0
POL(consInact(x₁, x₂)) = 0
POL(isNat(x₁)) = 1 + x₁
POL(isNatIList(x₁)) = 0
POL(isNatIListInact(x₁)) = 0
POL(isNatInact(x₁)) = 1 + x₁
POL(isNatList(x₁)) = 0
POL(isNatListInact(x₁)) = 0
POL(length(x₁)) = 0
POL(lengthInact(x₁)) = 0
POL(nil) = 1
POL(nilInact) = 1
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 1
POL(zerosInact) = 1

The following usable rules [17] were oriented:

isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
a(isNatListInact(x1)) → isNatList(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
and(tt, X) → a(X)
zeros → zerosInact
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(x) → x
cons(x1, x2) → consInact(x1, x2)
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
isNat(sInact(V1)) → isNat(a(V1))
isNat(0Inact) → tt
zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
a(nilInact) → nil
0 → 0Inact
a(lengthInact(x1)) → length(x1)
nil → nilInact
a(0Inact) → 0
isNat(x1) → isNatInact(x1)
a(sInact(x1)) → s(x1)
length(x1) → lengthInact(x1)
a(isNatInact(x1)) → isNat(x1)
isNatIList(x1) → isNatIListInact(x1)
a(zerosInact) → zeros
s(x1) → sInact(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → A(X)
ISNAT(sInact(V1)) → ISNAT(a(V1))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
A(isNatInact(x1)) → ISNAT(x1)
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                    ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNAT(sInact(V1)) → ISNAT(a(V1))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNAT(sInact(V1)) → ISNAT(a(V1))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( sInact(x₁) ) =

/	1	\
\	0	/

/	1	0	\
\	0	0	/

x₁

M( lengthInact(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( nilInact ) =

/	0	\
\	0	/

M( isNatListInact(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	1	/

x₁

M( U11(x₁, x₂) ) =

/	0	\
\	0	/

/	0	1	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( and(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	1	0	/

x₁

/	1	0	\
\	0	1	/

x₂

M( 0 ) =

/	1	\
\	0	/

M( isNatIListInact(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	1	/

x₁

M( isNatInact(x₁) ) =

/	0	\
\	0	/

/	1	0	\
\	0	0	/

x₁

M( cons(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	1	0	/

x₁

/	0	0	\
\	0	1	/

x₂

M( tt ) =

/	1	\
\	1	/

M( a(x₁) ) =

/	0	\
\	1	/

/	1	0	\
\	0	1	/

x₁

M( isNatList(x₁) ) =

/	0	\
\	1	/

/	0	0	\
\	0	1	/

x₁

M( zeros ) =

/	0	\
\	1	/

M( isNatIList(x₁) ) =

/	0	\
\	1	/

/	0	0	\
\	0	1	/

x₁

M( zerosInact ) =

/	0	\
\	0	/

M( 0Inact ) =

/	1	\
\	0	/

M( s(x₁) ) =

/	1	\
\	0	/

/	1	0	\
\	0	0	/

x₁

M( consInact(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	1	0	/

x₁

/	0	0	\
\	0	1	/

x₂

M( length(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( isNat(x₁) ) =

/	0	\
\	1	/

/	1	0	\
\	0	0	/

x₁

M( nil ) =

/	0	\
\	0	/

Tuple symbols:

M( ISNAT(x₁) ) =

[

]

x₁

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

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
a(isNatListInact(x1)) → isNatList(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
and(tt, X) → a(X)
zeros → zerosInact
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(x) → x
cons(x1, x2) → consInact(x1, x2)
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
isNat(sInact(V1)) → isNat(a(V1))
isNat(0Inact) → tt
zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
a(nilInact) → nil
0 → 0Inact
a(lengthInact(x1)) → length(x1)
nil → nilInact
a(0Inact) → 0
isNat(x1) → isNatInact(x1)
a(sInact(x1)) → s(x1)
length(x1) → lengthInact(x1)
a(isNatInact(x1)) → isNat(x1)
isNatIList(x1) → isNatIListInact(x1)
a(zerosInact) → zeros
s(x1) → sInact(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ PisEmptyProof

                                                    ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
P is empty.
The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → A(X)
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNATLIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatListInact(a(V2))) at position [0] we obtained the following new rules:

ISNATLIST(consInact(y0, y1)) → AND(isNatInact(a(y0)), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(consInact(y0, y1)) → AND(isNatInact(a(y0)), isNatListInact(a(y1)))
AND(tt, X) → A(X)
ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → A(X)
ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNATILIST(consInact(V1, V2)) → AND(isNat(a(V1)), isNatIListInact(a(V2))) at position [0] we obtained the following new rules:

ISNATILIST(consInact(y0, y1)) → AND(isNatInact(a(y0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(y0, y1)) → AND(isNatInact(a(y0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
AND(tt, X) → A(X)
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATILIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatIListInact(a(y1)))
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
AND(tt, X) → A(X)
ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatIListInact(a(y1)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule AND(tt, X) → A(X) we obtained the following new rules:

AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
AND(tt, isNatListInact(y_4)) → A(isNatListInact(y_4))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
ISNATILIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatIListInact(a(y1)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
AND(tt, isNatListInact(y_4)) → A(isNatListInact(y_4))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ AND

                                                                              ↳ QDP

                                                                                ↳ RuleRemovalProof

                                                                              ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

ISNATILIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatIListInact(a(y1)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₁ + x₂
POL(ISNATILIST(x₁)) = x₁
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListInact(x₁)) = x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListInact(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(lengthInact(x₁)) = 2·x₁
POL(nil) = 2
POL(nilInact) = 2
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ AND

                                                                              ↳ QDP

                                                                                ↳ RuleRemovalProof

                                                                                  ↳ QDP

                                                                                    ↳ RuleRemovalProof

                                                                              ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

ISNATILIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatIListInact(a(y1)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = 2 + x₁
POL(AND(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(ISNATILIST(x₁)) = 2 + 2·x₁
POL(U11(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 2·x₁
POL(isNatIListInact(x₁)) = 2·x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListInact(x₁)) = x₁
POL(length(x₁)) = 1 + 2·x₁
POL(lengthInact(x₁)) = 1 + 2·x₁
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ AND

                                                                              ↳ QDP

                                                                                ↳ RuleRemovalProof

                                                                                  ↳ QDP

                                                                                    ↳ RuleRemovalProof

                                                                                      ↳ QDP

                                                                                        ↳ RuleRemovalProof

                                                                              ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

ISNATILIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatIListInact(a(y1)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = 2·x₁ + x₂
POL(ISNATILIST(x₁)) = 2 + 2·x₁
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = 2·x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(consInact(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 2 + 2·x₁
POL(isNatIListInact(x₁)) = 2 + 2·x₁
POL(isNatInact(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListInact(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(lengthInact(x₁)) = 2·x₁
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ AND

                                                                              ↳ QDP

                                                                                ↳ RuleRemovalProof

                                                                                  ↳ QDP

                                                                                    ↳ RuleRemovalProof

                                                                                      ↳ QDP

                                                                                        ↳ RuleRemovalProof

                                                                                          ↳ QDP

                                                                                            ↳ QDPOrderProof

                                                                              ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATILIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatIListInact(a(y1)))

The remaining pairs can at least be oriented weakly.

ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

Used ordering: Polynomial interpretation with max and min functions [25]:

POL(0) = 0
POL(0Inact) = 0
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₂
POL(ISNATILIST(x₁)) = x₁
POL(U11(x₁, x₂)) = 1
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(consInact(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 1
POL(isNatIList(x₁)) = x₁
POL(isNatIListInact(x₁)) = x₁
POL(isNatInact(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListInact(x₁)) = 0
POL(length(x₁)) = 1
POL(lengthInact(x₁)) = 1
POL(nil) = 0
POL(nilInact) = 0
POL(s(x₁)) = 0
POL(sInact(x₁)) = 0
POL(tt) = 0
POL(zeros) = 0
POL(zerosInact) = 0

The following usable rules [17] were oriented:

isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
a(isNatListInact(x1)) → isNatList(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
and(tt, X) → a(X)
zeros → zerosInact
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(x) → x
cons(x1, x2) → consInact(x1, x2)
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
isNat(sInact(V1)) → isNat(a(V1))
isNat(0Inact) → tt
zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
a(nilInact) → nil
0 → 0Inact
a(lengthInact(x1)) → length(x1)
nil → nilInact
a(0Inact) → 0
isNat(x1) → isNatInact(x1)
a(sInact(x1)) → s(x1)
length(x1) → lengthInact(x1)
a(isNatInact(x1)) → isNat(x1)
isNatIList(x1) → isNatIListInact(x1)
a(zerosInact) → zeros
s(x1) → sInact(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ AND

                                                                              ↳ QDP

                                                                                ↳ RuleRemovalProof

                                                                                  ↳ QDP

                                                                                    ↳ RuleRemovalProof

                                                                                      ↳ QDP

                                                                                        ↳ RuleRemovalProof

                                                                                          ↳ QDP

                                                                                            ↳ QDPOrderProof

                                                                                              ↳ QDP

                                                                              ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatIListInact(a(y1)))
ISNATILIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatIListInact(a(y1)))
AND(tt, isNatIListInact(y_4)) → A(isNatIListInact(y_4))
ISNATILIST(consInact(0Inact, y1)) → AND(isNat(0), isNatIListInact(a(y1)))
ISNATILIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatIListInact(a(y1)))
A(isNatIListInact(x1)) → ISNATILIST(x1)
ISNATILIST(consInact(x0, y1)) → AND(isNat(x0), isNatIListInact(a(y1)))
ISNATILIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatIListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ AND

                                                                              ↳ QDP

                                                                              ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(consInact(isNatIListInact(x0), y1)) → AND(isNat(isNatIList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(sInact(x0), y1)) → AND(isNat(s(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(lengthInact(x0), y1)) → AND(isNat(length(x0)), isNatListInact(a(y1)))
A(isNatListInact(x1)) → ISNATLIST(x1)
ISNATLIST(consInact(zerosInact, y1)) → AND(isNat(zeros), isNatListInact(a(y1)))
ISNATLIST(consInact(isNatInact(x0), y1)) → AND(isNat(isNat(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(0Inact, y1)) → AND(isNat(0), isNatListInact(a(y1)))
ISNATLIST(consInact(nilInact, y1)) → AND(isNat(nil), isNatListInact(a(y1)))
AND(tt, isNatListInact(y_4)) → A(isNatListInact(y_4))
ISNATLIST(consInact(isNatListInact(x0), y1)) → AND(isNat(isNatList(x0)), isNatListInact(a(y1)))
ISNATLIST(consInact(consInact(x0, x1), y1)) → AND(isNat(cons(x0, x1)), isNatListInact(a(y1)))
ISNATLIST(consInact(x0, y1)) → AND(isNat(x0), isNatListInact(a(y1)))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(and(isNatList(a(L)), isNatInact(N)), a(L))
U11¹(tt, L) → LENGTH(a(L))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
U11(tt, L) → s(length(a(L)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(sInact(V1)) → isNat(a(V1))
isNatIList(consInact(V1, V2)) → and(isNat(a(V1)), isNatIListInact(a(V2)))
isNatList(consInact(V1, V2)) → and(isNat(a(V1)), isNatListInact(a(V2)))
length(cons(N, L)) → U11(and(isNatList(a(L)), isNatInact(N)), a(L))
a(x) → x
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)
isNatList(x1) → isNatListInact(x1)
a(isNatListInact(x1)) → isNatList(x1)
zeros → zerosInact
a(zerosInact) → zeros
isNatIList(x1) → isNatIListInact(x1)
a(isNatIListInact(x1)) → isNatIList(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
0 → 0Inact
a(0Inact) → 0
nil → nilInact
a(nilInact) → nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + 2·x₁
POL(isNatIListActive(x₁)) = 1 + 2·x₁
POL(isNatList(x₁)) = 2·x₁
POL(isNatListActive(x₁)) = 2·x₁
POL(length(x₁)) = 2·x₁
POL(lengthActive(x₁)) = 2·x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNatListActive(nil) → tt
lengthActive(nil) → 0

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(lengthActive(x₁)) = 2·x₁
POL(mark(x₁)) = x₁
POL(nil) = 1
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNatActive(length(V1)) → isNatListActive(V1)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = 1 + 2·x₁
POL(lengthActive(x₁)) = 1 + 2·x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

zerosActive → zeros
mark(isNat(x1)) → isNatActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
mark(0) → 0
mark(tt) → tt
mark(nil) → nil
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))

Used ordering:
Polynomial interpretation [25]:

POL(0) = 1
POL(U11(x₁, x₂)) = x₁ + x₂
POL(U11Active(x₁, x₂)) = x₁ + x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + 2·x₁
POL(isNatIListActive(x₁)) = 2 + 2·x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = 1 + x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

mark(isNatIList(x1)) → isNatIListActive(x1)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = x₁ + 2·x₂
POL(and(x₁, x₂)) = 2·x₁ + 2·x₂
POL(andActive(x₁, x₂)) = 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = 2 + x₁
POL(isNatIListActive(x₁)) = 1 + x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(lengthActive(x₁)) = 2·x₁
POL(mark(x₁)) = x₁
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
isNatActive(x1) → isNat(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
isNatActive(x1) → isNat(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNatActive(x1) → isNat(x1)
isNatListActive(x1) → isNatList(x1)
andActive(tt, X) → mark(X)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = 2·x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + 2·x₂
POL(andActive(x₁, x₂)) = x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = 1 + 2·x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = 1 + x₁
POL(length(x₁)) = 2 + 2·x₁
POL(lengthActive(x₁)) = 2 + 2·x₁
POL(mark(x₁)) = x₁
POL(s(x₁)) = x₁
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + x₂
POL(U11Active(x₁, x₂)) = x₁ + x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = 1 + x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = 1 + x₁
POL(s(x₁)) = x₁
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U11Active(tt, L) → s(lengthActive(mark(L)))

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = 2·x₁ + 2·x₂
POL(and(x₁, x₂)) = 2·x₁ + 2·x₂
POL(andActive(x₁, x₂)) = 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(isNatActive(x₁)) = 1 + 2·x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = 2 + 2·x₁
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(s(x₁)) = x₁
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RRRPoloQTRSProof

                                    ↳ QTRS

                                      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U11Active(x1, x2) → U11(x1, x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
isNatActive(0) → tt
isNatActive(s(V1)) → isNatActive(V1)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 1
POL(U11(x₁, x₂)) = 1 + x₁ + x₂
POL(U11Active(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(and(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(andActive(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(isNatActive(x₁)) = x₁
POL(isNatList(x₁)) = 2·x₁
POL(isNatListActive(x₁)) = 2 + 2·x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = 2 + 2·x₁
POL(s(x₁)) = 1 + x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 2

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RRRPoloQTRSProof

                                    ↳ QTRS

                                      ↳ RRRPoloQTRSProof

                                        ↳ QTRS

                                          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

mark(zeros) → zerosActive
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = 1 + x₁ + x₂
POL(and(x₁, x₂)) = 1 + x₁ + x₂
POL(andActive(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(cons(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(isNatActive(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = 2·x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = 2 + 2·x₁
POL(zeros) = 2
POL(zerosActive) = 1

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RRRPoloQTRSProof

                                    ↳ QTRS

                                      ↳ RRRPoloQTRSProof

                                        ↳ QTRS

                                          ↳ RRRPoloQTRSProof

                                            ↳ QTRS

                                              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

lengthActive(x1) → length(x1)

Used ordering:
Polynomial interpretation [25]:

POL(and(x₁, x₂)) = 2 + x₁ + x₂
POL(andActive(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(length(x₁)) = 1 + 2·x₁
POL(lengthActive(x₁)) = 2 + 2·x₁
POL(mark(x₁)) = 2·x₁

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RRRPoloQTRSProof

                                    ↳ QTRS

                                      ↳ RRRPoloQTRSProof

                                        ↳ QTRS

                                          ↳ RRRPoloQTRSProof

                                            ↳ QTRS

                                              ↳ RRRPoloQTRSProof

                                                ↳ QTRS

                                                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))

Used ordering:
Polynomial interpretation [25]:

POL(and(x₁, x₂)) = 1 + x₁ + x₂
POL(andActive(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(length(x₁)) = 2 + 2·x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = 2 + x₁

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RRRPoloQTRSProof

                                    ↳ QTRS

                                      ↳ RRRPoloQTRSProof

                                        ↳ QTRS

                                          ↳ RRRPoloQTRSProof

                                            ↳ QTRS

                                              ↳ RRRPoloQTRSProof

                                                ↳ QTRS

                                                  ↳ RRRPoloQTRSProof

                                                    ↳ QTRS

                                                      ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.