Termination w.r.t. Q proof of /tmp/tmpLN1D0i/Ex4_DLMMU04

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

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

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

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

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

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

ISNATILIST(IL) → ACTIVATE(IL)
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ISNATILIST(n__cons(N, IL)) → ACTIVATE(IL)
UTAKE1(tt) → NIL
ISNATLIST(n__take(N, IL)) → AND(isNat(activate(N)), isNatIList(activate(IL)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ISNATLIST(n__take(N, IL)) → ACTIVATE(IL)
ULENGTH(tt, L) → ACTIVATE(L)
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNATILIST(n__cons(N, IL)) → ACTIVATE(N)
ACTIVATE(n__0) → 0¹
ULENGTH(tt, L) → S(length(activate(L)))
ULENGTH(tt, L) → LENGTH(activate(L))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
LENGTH(cons(N, L)) → ISNAT(N)
ACTIVATE(n__zeros) → ZEROS
UTAKE2(tt, M, N, IL) → ACTIVATE(M)
ISNATLIST(n__cons(N, L)) → ACTIVATE(N)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__nil) → NIL
TAKE(0, IL) → ISNATILIST(IL)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ISNAT(n__s(N)) → ACTIVATE(N)
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
UTAKE2(tt, M, N, IL) → CONS(activate(N), n__take(activate(M), activate(IL)))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))
ISNATLIST(n__cons(N, L)) → AND(isNat(activate(N)), isNatList(activate(L)))
TAKE(s(M), cons(N, IL)) → AND(isNat(N), isNatIList(activate(IL)))
UTAKE2(tt, M, N, IL) → ACTIVATE(IL)
ISNATLIST(n__cons(N, L)) → ACTIVATE(L)
ISNATLIST(n__take(N, IL)) → ACTIVATE(N)
ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
UTAKE2(tt, M, N, IL) → ACTIVATE(N)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
TAKE(s(M), cons(N, IL)) → ISNAT(M)
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
TAKE(s(M), cons(N, IL)) → AND(isNat(M), and(isNat(N), isNatIList(activate(IL))))
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(activate(L))), activate(L))
TAKE(0, IL) → UTAKE1(isNatIList(IL))
LENGTH(cons(N, L)) → AND(isNat(N), isNatList(activate(L)))
LENGTH(cons(N, L)) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
ACTIVATE(n__length(X)) → LENGTH(activate(X))
ISNAT(n__s(N)) → ISNAT(activate(N))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
ISNATILIST(n__cons(N, IL)) → AND(isNat(activate(N)), isNatIList(activate(IL)))
ZEROS → CONS(0, n__zeros)
ZEROS → 0¹
ISNAT(n__length(L)) → ACTIVATE(L)
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ACTIVATE(n__length(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

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

ISNATILIST(IL) → ACTIVATE(IL)
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ISNATILIST(n__cons(N, IL)) → ACTIVATE(IL)
UTAKE1(tt) → NIL
ISNATLIST(n__take(N, IL)) → AND(isNat(activate(N)), isNatIList(activate(IL)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ISNATLIST(n__take(N, IL)) → ACTIVATE(IL)
ULENGTH(tt, L) → ACTIVATE(L)
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNATILIST(n__cons(N, IL)) → ACTIVATE(N)
ACTIVATE(n__0) → 0¹
ULENGTH(tt, L) → S(length(activate(L)))
ULENGTH(tt, L) → LENGTH(activate(L))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
LENGTH(cons(N, L)) → ISNAT(N)
ACTIVATE(n__zeros) → ZEROS
UTAKE2(tt, M, N, IL) → ACTIVATE(M)
ISNATLIST(n__cons(N, L)) → ACTIVATE(N)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__nil) → NIL
TAKE(0, IL) → ISNATILIST(IL)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ISNAT(n__s(N)) → ACTIVATE(N)
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
UTAKE2(tt, M, N, IL) → CONS(activate(N), n__take(activate(M), activate(IL)))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))
ISNATLIST(n__cons(N, L)) → AND(isNat(activate(N)), isNatList(activate(L)))
TAKE(s(M), cons(N, IL)) → AND(isNat(N), isNatIList(activate(IL)))
UTAKE2(tt, M, N, IL) → ACTIVATE(IL)
ISNATLIST(n__cons(N, L)) → ACTIVATE(L)
ISNATLIST(n__take(N, IL)) → ACTIVATE(N)
ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
UTAKE2(tt, M, N, IL) → ACTIVATE(N)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
TAKE(s(M), cons(N, IL)) → ISNAT(M)
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
TAKE(s(M), cons(N, IL)) → AND(isNat(M), and(isNat(N), isNatIList(activate(IL))))
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(activate(L))), activate(L))
TAKE(0, IL) → UTAKE1(isNatIList(IL))
LENGTH(cons(N, L)) → AND(isNat(N), isNatList(activate(L)))
LENGTH(cons(N, L)) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
ACTIVATE(n__length(X)) → LENGTH(activate(X))
ISNAT(n__s(N)) → ISNAT(activate(N))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
ISNATILIST(n__cons(N, IL)) → AND(isNat(activate(N)), isNatIList(activate(IL)))
ZEROS → CONS(0, n__zeros)
ZEROS → 0¹
ISNAT(n__length(L)) → ACTIVATE(L)
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ACTIVATE(n__length(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

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

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__length(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

          ↳ QDP

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

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__length(X)) → ACTIVATE(X)

R is empty.
The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

          ↳ QDP

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

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
The graph contains the following edges 1 > 1
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
The graph contains the following edges 1 > 1
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
The graph contains the following edges 1 > 1
ACTIVATE(n__s(X)) → ACTIVATE(X)
The graph contains the following edges 1 > 1
ACTIVATE(n__length(X)) → ACTIVATE(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNAT(n__s(N)) → ISNAT(activate(N))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNAT(n__s(N)) → ISNAT(activate(N))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isNatIList(x0)
isNat(n__s(x0))
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
isNat(n__length(x0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
ISNAT(n__s(N)) → ISNAT(activate(N))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

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:

ISNAT(n__length(L)) → ISNATLIST(activate(L))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 2·x₁
POL(ISNATLIST(x₁)) = x₁
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(length(x₁)) = 1 + x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__length(x₁)) = 1 + x₁
POL(n__nil) = 0
POL(n__s(x₁)) = x₁
POL(n__take(x₁, x₂)) = x₁ + 2·x₂
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + 2·x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNAT(n__s(N)) → ISNAT(activate(N))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ RuleRemovalProof

                            ↳ QDP

            ↳ UsableRulesProof

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

ISNAT(n__s(N)) → ISNAT(activate(N))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

ISNAT(n__s(N)) → ISNAT(activate(N))

Strictly oriented rules of the TRS R:

activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
nil → n__nil
s(X) → n__s(X)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNAT(x₁)) = x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(length(x₁)) = x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__length(x₁)) = x₁
POL(n__nil) = 1
POL(n__s(x₁)) = 1 + 2·x₁
POL(n__take(x₁, x₂)) = 2 + x₁ + x₂
POL(n__zeros) = 0
POL(nil) = 2
POL(s(x₁)) = 2 + 2·x₁
POL(take(x₁, x₂)) = 2 + x₁ + x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ PisEmptyProof

                            ↳ QDP

            ↳ UsableRulesProof

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

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

ISNATILIST(IL) → ISNATLIST(activate(IL))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = 2 + x₁
POL(ISNATLIST(x₁)) = 1 + x₁
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(length(x₁)) = x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__length(x₁)) = x₁
POL(n__nil) = 0
POL(n__s(x₁)) = 2·x₁
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x₁)) = 2·x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

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.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

nil → n__nil
length(X) → n__length(X)
s(X) → n__s(X)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = 2·x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(length(x₁)) = 2 + x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__length(x₁)) = 1 + x₁
POL(n__nil) = 1
POL(n__s(x₁)) = 1 + x₁
POL(n__take(x₁, x₂)) = 2·x₁ + x₂
POL(n__zeros) = 0
POL(nil) = 2
POL(s(x₁)) = 2 + x₁
POL(take(x₁, x₂)) = 2·x₁ + x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__nil) → nil

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = 2·x₁
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(length(x₁)) = 2·x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = x₁ + 2·x₂
POL(n__length(x₁)) = 2·x₁
POL(n__nil) = 1
POL(n__s(x₁)) = 2 + x₁
POL(n__take(x₁, x₂)) = x₁ + 2·x₂
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x₁)) = 1 + x₁
POL(take(x₁, x₂)) = x₁ + 2·x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

nil
s(x0)
length(x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
take(x0, x1)
0
cons(x0, x1)

activate(n__take(X1, X2)) → take(activate(X1), activate(X2))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__take(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(n__zeros) = 0
POL(take(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
take(x0, x1)
0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
take(x0, x1)
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

take(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

zeros → n__zeros

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = 2·x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__zeros) = 1
POL(zeros) = 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

activate(n__0) → 0
activate(X) → X

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = 2·x₁
POL(activate(x₁)) = 2 + x₁
POL(cons(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(n__zeros) = 0
POL(zeros) = 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

activate(n__cons(X1, X2)) → cons(activate(X1), X2)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATILIST(x₁)) = x₁
POL(activate(x₁)) = 1 + 2·x₁
POL(cons(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(n__zeros) = 0
POL(zeros) = 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL)) at position [0] we obtained the following new rules:

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(zeros)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(zeros)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(zeros)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

activate(x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(zeros)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(zeros) at position [0] we obtained the following new rules:

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(cons(0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

zeros
0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

zeros

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(cons(0, n__zeros)) at position [0] we obtained the following new rules:

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0

The set Q consists of the following terms:

0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0

The set Q consists of the following terms:

0

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(0, n__zeros)) at position [0,0] we obtained the following new rules:

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

0 → n__0

The set Q consists of the following terms:

0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ QReductionProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

R is empty.
The set Q consists of the following terms:

0

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ QReductionProof

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule ISNATILIST(n__cons(y0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros)) we obtained the following new rules:

ISNATILIST(n__cons(n__0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ QReductionProof

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ NonTerminationProof

                                      ↳ QDP

            ↳ UsableRulesProof

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

ISNATILIST(n__cons(n__0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

ISNATILIST(n__cons(n__0, n__zeros)) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:none

s = ISNATILIST(n__cons(n__0, n__zeros)) evaluates to t =ISNATILIST(n__cons(n__0, n__zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISNATILIST(n__cons(n__0, n__zeros)) to ISNATILIST(n__cons(n__0, n__zeros)).

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

nil → n__nil
length(X) → n__length(X)
s(X) → n__s(X)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATLIST(x₁)) = 2·x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(length(x₁)) = 2 + x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__length(x₁)) = 1 + x₁
POL(n__nil) = 1
POL(n__s(x₁)) = 1 + x₁
POL(n__take(x₁, x₂)) = 2·x₁ + x₂
POL(n__zeros) = 0
POL(nil) = 2
POL(s(x₁)) = 2 + x₁
POL(take(x₁, x₂)) = 2·x₁ + x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__nil) → nil

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATLIST(x₁)) = 2·x₁
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(length(x₁)) = 2·x₁
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = x₁ + 2·x₂
POL(n__length(x₁)) = 2·x₁
POL(n__nil) = 1
POL(n__s(x₁)) = 2 + x₁
POL(n__take(x₁, x₂)) = x₁ + 2·x₂
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x₁)) = 1 + x₁
POL(take(x₁, x₂)) = x₁ + 2·x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

nil
s(x0)
length(x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
take(x0, x1)
0
cons(x0, x1)

activate(n__take(X1, X2)) → take(activate(X1), activate(X2))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATLIST(x₁)) = x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__take(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(n__zeros) = 0
POL(take(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(zeros) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
take(x0, x1)
0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
take(x0, x1)
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

take(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

zeros → n__zeros

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATLIST(x₁)) = 2·x₁
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__zeros) = 1
POL(zeros) = 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

activate(n__0) → 0
activate(X) → X

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATLIST(x₁)) = 2·x₁
POL(activate(x₁)) = 2 + x₁
POL(cons(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(n__zeros) = 0
POL(zeros) = 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

activate(n__cons(X1, X2)) → cons(activate(X1), X2)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(ISNATLIST(x₁)) = x₁
POL(activate(x₁)) = 1 + 2·x₁
POL(cons(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(n__0) = 0
POL(n__cons(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(n__zeros) = 0
POL(zeros) = 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L)) at position [0] we obtained the following new rules:

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(zeros)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(zeros)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
0 → n__0

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(zeros)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

activate(x0)
zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

activate(x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(zeros)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(zeros) at position [0] we obtained the following new rules:

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(cons(0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

zeros
0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

zeros
0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

zeros

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(cons(0, n__zeros)) at position [0] we obtained the following new rules:

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0
cons(X1, X2) → n__cons(X1, X2)

The set Q consists of the following terms:

0
cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0

The set Q consists of the following terms:

0
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

cons(x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(0, n__zeros))

The TRS R consists of the following rules:

0 → n__0

The set Q consists of the following terms:

0

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(0, n__zeros)) at position [0,0] we obtained the following new rules:

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

0 → n__0

The set Q consists of the following terms:

0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ QReductionProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros))

R is empty.
The set Q consists of the following terms:

0

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ QReductionProof

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule ISNATLIST(n__cons(y0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros)) we obtained the following new rules:

ISNATLIST(n__cons(n__0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ RuleRemovalProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ AND

                                      ↳ QDP

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ UsableRulesReductionPairsProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ RuleRemovalProof

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ RuleRemovalProof

                                                                  ↳ QDP

                                                                    ↳ RuleRemovalProof

                                                                      ↳ QDP

                                                                        ↳ RuleRemovalProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ UsableRulesProof

                                                                                  ↳ QDP

                                                                                    ↳ QReductionProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ UsableRulesProof

                                                                                              ↳ QDP

                                                                                                ↳ QReductionProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ UsableRulesProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ QReductionProof

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Instantiation

                                                                                                                              ↳ QDP

                                                                                                                                ↳ NonTerminationProof

            ↳ UsableRulesProof

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

ISNATLIST(n__cons(n__0, n__zeros)) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:none

s = ISNATLIST(n__cons(n__0, n__zeros)) evaluates to t =ISNATLIST(n__cons(n__0, n__zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISNATLIST(n__cons(n__0, n__zeros)) to ISNATLIST(n__cons(n__0, n__zeros)).

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

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

ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNAT(n__s(N)) → ISNAT(activate(N))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

isNatIList(x0)
activate(x0)
isNat(n__s(x0))
nil
zeros
s(x0)
take(x0, x1)
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
length(x0)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
0
isNat(n__length(x0))
cons(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isNatIList(x0)
isNat(n__s(x0))
uLength(tt, x0)
isNatList(n__nil)
isNatList(n__cons(x0, x1))
uTake1(tt)
uTake2(tt, x0, x1, x2)
isNatList(n__take(x0, x1))
isNat(n__0)
and(tt, x0)
isNat(n__length(x0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

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

ISNATILIST(n__cons(N, IL)) → ISNAT(activate(N))
ISNAT(n__length(L)) → ISNATLIST(activate(L))
ISNATILIST(IL) → ISNATLIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__take(N, IL)) → ISNAT(activate(N))
ISNAT(n__s(N)) → ISNAT(activate(N))
ISNATLIST(n__take(N, IL)) → ISNATILIST(activate(IL))
ISNATILIST(n__cons(N, IL)) → ISNATILIST(activate(IL))
ISNATLIST(n__cons(N, L)) → ISNAT(activate(N))

The TRS R consists of the following rules:

activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X
take(X1, X2) → n__take(X1, X2)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)

The set Q consists of the following terms:

activate(x0)
nil
zeros
s(x0)
take(x0, x1)
length(x0)
0
cons(x0, x1)

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