Termination proof of ../tpdb/TRS/CSR/Ex1

YES Termination proof of ../tpdb/TRS/CSR/Ex1_GL02a.trs
Termination of the following Term Rewriting System could be proven:

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

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

The replacement map contains the following entries:

eq: empty set
0: empty set
true: empty set
s: empty set
false: empty set
inf: {1}
cons: empty set
take: {1, 2}
nil: empty set
length: {1}

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

The replacement map contains the following entries:

eq: empty set
0: empty set
true: empty set
s: empty set
false: empty set
inf: {1}
cons: empty set
take: {1, 2}
nil: empty set
length: {1}

We applied the Lucas [26] to transform the context-sensitive TRS to an usual TRS.

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

eq → true
eq → eq
eq → false
inf(X) → cons
take(0, X) → nil
take(s, cons) → cons
length(nil) → 0
length(cons) → s

Q is empty.

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

eq → true
eq → eq
eq → false
inf(X) → cons
take(0, X) → nil
take(s, cons) → cons
length(nil) → 0
length(cons) → s

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

eq → true
eq → false
take(s, cons) → cons
length(nil) → 0
length(cons) → s

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(cons) = 2
POL(eq) = 2
POL(false) = 0
POL(inf(x₁)) = 2 + x₁
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 0
POL(s) = 1
POL(take(x₁, x₂)) = 2·x₁ + 2·x₂
POL(true) = 1

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

eq → eq
inf(X) → cons
take(0, X) → nil

Q is empty.

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

eq → eq
inf(X) → cons
take(0, X) → nil

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

inf(X) → cons
take(0, X) → nil

Used ordering:
Polynomial interpretation [25]:

POL(0) = 2
POL(cons) = 1
POL(eq) = 0
POL(inf(x₁)) = 2 + x₁
POL(nil) = 1
POL(take(x₁, x₂)) = 2 + 2·x₁ + x₂

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ AAECC Innermost

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

eq → eq

Q is empty.

We have applied [19,8] to switch to innermost. The TRS R 1 is none

The TRS R 2 is

eq → eq

The signature Sigma is {eq}

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ AAECC Innermost

                ↳ QTRS

                  ↳ DependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

eq → eq

The set Q consists of the following terms:

eq

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

EQ → EQ

The TRS R consists of the following rules:

eq → eq

The set Q consists of the following terms:

eq

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

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ AAECC Innermost

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ UsableRulesProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ → EQ

The TRS R consists of the following rules:

eq → eq

The set Q consists of the following terms:

eq

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.

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ AAECC Innermost

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ UsableRulesProof

                        ↳ QDP

                          ↳ QReductionProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ → EQ

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

eq

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.

eq

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ AAECC Innermost

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ UsableRulesProof

                        ↳ QDP

                          ↳ QReductionProof

                            ↳ QDP

                              ↳ NonTerminationProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ → EQ

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:

EQ → EQ

The TRS R consists of the following rules:none

s = EQ evaluates to t =EQ

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 EQ to EQ.

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.

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

TAKE(s(X), cons(Y, L)) → A(L)
A(0Inact) → 0¹
A(infInact(x1)) → INF(x1)
LENGTH(cons(X, L)) → A(L)
A(sInact(x1)) → S(x1)
A(takeInact(x1, x2)) → TAKE(x1, x2)
EQ(sInact(X), sInact(Y)) → EQ(a(X), a(Y))
INF(X) → S(X)
A(lengthInact(x1)) → LENGTH(x1)
TAKE(s(X), cons(Y, L)) → A(X)
LENGTH(nil) → 0¹
EQ(sInact(X), sInact(Y)) → A(Y)
LENGTH(cons(X, L)) → S(lengthInact(a(L)))
EQ(sInact(X), sInact(Y)) → A(X)
TAKE(s(X), cons(Y, L)) → A(Y)

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

TAKE(s(X), cons(Y, L)) → A(L)
A(0Inact) → 0¹
A(infInact(x1)) → INF(x1)
LENGTH(cons(X, L)) → A(L)
A(sInact(x1)) → S(x1)
A(takeInact(x1, x2)) → TAKE(x1, x2)
EQ(sInact(X), sInact(Y)) → EQ(a(X), a(Y))
INF(X) → S(X)
A(lengthInact(x1)) → LENGTH(x1)
TAKE(s(X), cons(Y, L)) → A(X)
LENGTH(nil) → 0¹
EQ(sInact(X), sInact(Y)) → A(Y)
LENGTH(cons(X, L)) → S(lengthInact(a(L)))
EQ(sInact(X), sInact(Y)) → A(X)
TAKE(s(X), cons(Y, L)) → A(Y)

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

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

TAKE(s(X), cons(Y, L)) → A(L)
LENGTH(cons(X, L)) → A(L)
A(lengthInact(x1)) → LENGTH(x1)
A(takeInact(x1, x2)) → TAKE(x1, x2)
TAKE(s(X), cons(Y, L)) → A(X)
TAKE(s(X), cons(Y, L)) → A(Y)

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

              ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

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

TAKE(s(X), cons(Y, L)) → A(L)
LENGTH(cons(X, L)) → A(L)
A(lengthInact(x1)) → LENGTH(x1)
A(takeInact(x1, x2)) → TAKE(x1, x2)
TAKE(s(X), cons(Y, L)) → A(X)
TAKE(s(X), cons(Y, L)) → A(Y)

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:

A(takeInact(x1, x2)) → TAKE(x1, x2)
The graph contains the following edges 1 > 1, 1 > 2
A(lengthInact(x1)) → LENGTH(x1)
The graph contains the following edges 1 > 1
LENGTH(cons(X, L)) → A(L)
The graph contains the following edges 1 > 1
TAKE(s(X), cons(Y, L)) → A(L)
The graph contains the following edges 2 > 1
TAKE(s(X), cons(Y, L)) → A(X)
The graph contains the following edges 1 > 1
TAKE(s(X), cons(Y, L)) → A(Y)
The graph contains the following edges 2 > 1

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(X), sInact(Y)) → EQ(a(X), a(Y))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(X), sInact(Y)) → EQ(a(X), a(Y)) at position [0] we obtained the following new rules:

EQ(sInact(infInact(x0)), sInact(y1)) → EQ(inf(x0), a(y1))
EQ(sInact(sInact(x0)), sInact(y1)) → EQ(s(x0), a(y1))
EQ(sInact(lengthInact(x0)), sInact(y1)) → EQ(length(x0), a(y1))
EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1))
EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1))
EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(infInact(x0)), sInact(y1)) → EQ(inf(x0), a(y1))
EQ(sInact(sInact(x0)), sInact(y1)) → EQ(s(x0), a(y1))
EQ(sInact(lengthInact(x0)), sInact(y1)) → EQ(length(x0), a(y1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(infInact(x0)), sInact(y1)) → EQ(inf(x0), a(y1)) at position [0] we obtained the following new rules:

EQ(sInact(infInact(x0)), sInact(y1)) → EQ(cons(x0, infInact(s(x0))), a(y1))
EQ(sInact(infInact(x0)), sInact(y1)) → EQ(infInact(x0), a(y1))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1))
EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(sInact(x0)), sInact(y1)) → EQ(s(x0), a(y1))
EQ(sInact(infInact(x0)), sInact(y1)) → EQ(cons(x0, infInact(s(x0))), a(y1))
EQ(sInact(lengthInact(x0)), sInact(y1)) → EQ(length(x0), a(y1))
EQ(sInact(infInact(x0)), sInact(y1)) → EQ(infInact(x0), a(y1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1))
EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(sInact(x0)), sInact(y1)) → EQ(s(x0), a(y1))
EQ(sInact(lengthInact(x0)), sInact(y1)) → EQ(length(x0), a(y1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(sInact(x0)), sInact(y1)) → EQ(s(x0), a(y1)) at position [1] we obtained the following new rules:

EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1))
EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(x0)), sInact(y1)) → EQ(length(x0), a(y1))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(lengthInact(x0)), sInact(y1)) → EQ(length(x0), a(y1)) at position [1] we obtained the following new rules:

EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(takeInact(x0, x1)), sInact(y1)) → EQ(take(x0, x1), a(y1)) at position [0] we obtained the following new rules:

EQ(sInact(takeInact(x0, x1)), sInact(y2)) → EQ(takeInact(x0, x1), a(y2))
EQ(sInact(takeInact(s(x0), cons(x1, x2))), sInact(y2)) → EQ(cons(a(x1), takeInact(a(x0), a(x2))), a(y2))
EQ(sInact(takeInact(0, x0)), sInact(y2)) → EQ(nil, a(y2))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(takeInact(s(x0), cons(x1, x2))), sInact(y2)) → EQ(cons(a(x1), takeInact(a(x0), a(x2))), a(y2))
EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(takeInact(x0, x1)), sInact(y2)) → EQ(takeInact(x0, x1), a(y2))
EQ(sInact(takeInact(0, x0)), sInact(y2)) → EQ(nil, a(y2))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(0Inact), sInact(y1)) → EQ(0, a(y1)) at position [0] we obtained the following new rules:

EQ(sInact(0Inact), sInact(y0)) → EQ(0Inact, a(y0))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(0Inact), sInact(y0)) → EQ(0Inact, a(y0))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))
EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(x0), sInact(y1)) → EQ(x0, a(y1)) at position [1] we obtained the following new rules:

EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), take(x0, x1)) at position [1] we obtained the following new rules:

EQ(sInact(sInact(y0)), sInact(takeInact(s(x0), cons(x1, x2)))) → EQ(s(y0), cons(a(x1), takeInact(a(x0), a(x2))))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), takeInact(x0, x1))
EQ(sInact(sInact(y0)), sInact(takeInact(0, x0))) → EQ(s(y0), nil)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(s(x0), cons(x1, x2)))) → EQ(s(y0), cons(a(x1), takeInact(a(x0), a(x2))))
EQ(sInact(sInact(y0)), sInact(takeInact(x0, x1))) → EQ(s(y0), takeInact(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(takeInact(0, x0))) → EQ(s(y0), nil)

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), inf(x0)) at position [1] we obtained the following new rules:

EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), cons(x0, infInact(s(x0))))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), infInact(x0))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), infInact(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(infInact(x0))) → EQ(s(y0), cons(x0, infInact(s(x0))))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0) at position [1] we obtained the following new rules:

EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0Inact)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(sInact(y0)), sInact(0Inact)) → EQ(s(y0), 0Inact)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), take(x0, x1)) at position [1] we obtained the following new rules:

EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), takeInact(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(takeInact(s(x0), cons(x1, x2)))) → EQ(length(y0), cons(a(x1), takeInact(a(x0), a(x2))))
EQ(sInact(lengthInact(y0)), sInact(takeInact(0, x0))) → EQ(length(y0), nil)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(lengthInact(y0)), sInact(takeInact(s(x0), cons(x1, x2)))) → EQ(length(y0), cons(a(x1), takeInact(a(x0), a(x2))))
EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(takeInact(0, x0))) → EQ(length(y0), nil)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(lengthInact(y0)), sInact(takeInact(x0, x1))) → EQ(length(y0), takeInact(x0, x1))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0) at position [1] we obtained the following new rules:

EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0Inact)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(0Inact)) → EQ(length(y0), 0Inact)

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), inf(x0)) at position [1] we obtained the following new rules:

EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), cons(x0, infInact(s(x0))))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), infInact(x0))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), infInact(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(infInact(x0))) → EQ(length(y0), cons(x0, infInact(s(x0))))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, inf(x0)) at position [1] we obtained the following new rules:

EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, infInact(x0))
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, cons(x0, infInact(s(x0))))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, infInact(x0))
EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(infInact(x0))) → EQ(y0, cons(x0, infInact(s(x0))))
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0)
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0) at position [1] we obtained the following new rules:

EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0Inact)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

                                                                                                                  ↳ QDP

                                                                                                                    ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(y0), sInact(0Inact)) → EQ(y0, 0Inact)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

                                                                                                                  ↳ QDP

                                                                                                                    ↳ DependencyGraphProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1))
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, take(x0, x1)) at position [1] we obtained the following new rules:

EQ(sInact(y0), sInact(takeInact(s(x0), cons(x1, x2)))) → EQ(y0, cons(a(x1), takeInact(a(x0), a(x2))))
EQ(sInact(y0), sInact(takeInact(0, x0))) → EQ(y0, nil)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, takeInact(x0, x1))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

                                                                                                                  ↳ QDP

                                                                                                                    ↳ DependencyGraphProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(takeInact(s(x0), cons(x1, x2)))) → EQ(y0, cons(a(x1), takeInact(a(x0), a(x2))))
EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(y0), sInact(takeInact(x0, x1))) → EQ(y0, takeInact(x0, x1))
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(y0), sInact(takeInact(0, x0))) → EQ(y0, nil)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

                                                                                                                  ↳ QDP

                                                                                                                    ↳ DependencyGraphProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ DependencyGraphProof

                                                                                                                              ↳ QDP

                                                                                                                                ↳ QDPOrderProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

The following pairs can be oriented strictly and are deleted.

EQ(sInact(y0), sInact(x0)) → EQ(y0, x0)
EQ(sInact(sInact(y0)), sInact(x0)) → EQ(s(y0), x0)
EQ(sInact(sInact(y0)), sInact(lengthInact(x0))) → EQ(s(y0), length(x0))
EQ(sInact(sInact(y0)), sInact(sInact(x0))) → EQ(s(y0), s(x0))
EQ(sInact(y0), sInact(sInact(x0))) → EQ(y0, s(x0))
EQ(sInact(y0), sInact(lengthInact(x0))) → EQ(y0, length(x0))

The remaining pairs can at least be oriented weakly.

EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(0Inact) = 1
POL(EQ(x₁, x₂)) = x₁
POL(a(x₁)) = 1
POL(cons(x₁, x₂)) = 0
POL(inf(x₁)) = 0
POL(infInact(x₁)) = 0
POL(length(x₁)) = 1
POL(lengthInact(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = 1 + x₁
POL(sInact(x₁)) = 1 + x₁
POL(take(x₁, x₂)) = 0
POL(takeInact(x₁, x₂)) = 0

The following usable rules [17] were oriented:

take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
a(takeInact(x1, x2)) → take(x1, x2)
take(0, X) → nil
length(x1) → lengthInact(x1)
0 → 0Inact
length(cons(X, L)) → s(lengthInact(a(L)))
s(x1) → sInact(x1)
length(nil) → 0
take(x1, x2) → takeInact(x1, x2)
a(lengthInact(x1)) → length(x1)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

                                                                                                                  ↳ QDP

                                                                                                                    ↳ DependencyGraphProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ DependencyGraphProof

                                                                                                                              ↳ QDP

                                                                                                                                ↳ QDPOrderProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ QDPOrderProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))
EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

The following pairs can be oriented strictly and are deleted.

EQ(sInact(lengthInact(y0)), sInact(x0)) → EQ(length(y0), x0)
EQ(sInact(lengthInact(y0)), sInact(sInact(x0))) → EQ(length(y0), s(x0))

The remaining pairs can at least be oriented weakly.

EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(0Inact) = 0
POL(EQ(x₁, x₂)) = x₂
POL(a(x₁)) = 1 + x₁
POL(cons(x₁, x₂)) = 0
POL(inf(x₁)) = 0
POL(infInact(x₁)) = 0
POL(length(x₁)) = 1
POL(lengthInact(x₁)) = 0
POL(nil) = 1
POL(s(x₁)) = 1 + x₁
POL(sInact(x₁)) = 1 + x₁
POL(take(x₁, x₂)) = 1
POL(takeInact(x₁, x₂)) = 1

The following usable rules [17] were oriented:

take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
a(takeInact(x1, x2)) → take(x1, x2)
take(0, X) → nil
length(x1) → lengthInact(x1)
0 → 0Inact
length(cons(X, L)) → s(lengthInact(a(L)))
s(x1) → sInact(x1)
length(nil) → 0
take(x1, x2) → takeInact(x1, x2)
a(lengthInact(x1)) → length(x1)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                                              ↳ QDP

                                                                                ↳ Narrowing

                                                                                  ↳ QDP

                                                                                    ↳ DependencyGraphProof

                                                                                      ↳ QDP

                                                                                        ↳ Narrowing

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                                                                                                ↳ Narrowing

                                                                                                  ↳ QDP

                                                                                                    ↳ DependencyGraphProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Narrowing

                                                                                                          ↳ QDP

                                                                                                            ↳ DependencyGraphProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Narrowing

                                                                                                                  ↳ QDP

                                                                                                                    ↳ DependencyGraphProof

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ DependencyGraphProof

                                                                                                                              ↳ QDP

                                                                                                                                ↳ QDPOrderProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ QDPOrderProof

                                                                                                                                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

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

EQ(sInact(lengthInact(y0)), sInact(lengthInact(x0))) → EQ(length(y0), length(x0))

The TRS R consists of the following rules:

eq(0Inact, 0Inact) → true
eq(sInact(X), sInact(Y)) → eq(a(X), a(Y))
eq(X, Y) → false
inf(X) → cons(X, infInact(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(a(Y), takeInact(a(X), a(L)))
length(nil) → 0
length(cons(X, L)) → s(lengthInact(a(L)))
a(x) → x
length(x1) → lengthInact(x1)
a(lengthInact(x1)) → length(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
take(x1, x2) → takeInact(x1, x2)
a(takeInact(x1, x2)) → take(x1, x2)
inf(x1) → infInact(x1)
a(infInact(x1)) → inf(x1)

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

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

mark(eq(x1, x2)) → eqActive(x1, x2)
eqActive(x1, x2) → eq(x1, x2)
mark(inf(x1)) → infActive(mark(x1))
infActive(x1) → inf(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(0) → 0
mark(true) → true
mark(s(x1)) → s(x1)
mark(false) → false
mark(cons(x1, x2)) → cons(x1, x2)
mark(nil) → nil
eqActive(0, 0) → true
eqActive(s(X), s(Y)) → eqActive(X, Y)
eqActive(X, Y) → false
infActive(X) → cons(X, inf(s(X)))
takeActive(0, X) → nil
takeActive(s(X), cons(Y, L)) → cons(Y, take(X, L))
lengthActive(nil) → 0
lengthActive(cons(X, L)) → s(length(L))

Q is empty.

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

MARK(take(x1, x2)) → MARK(x2)
MARK(inf(x1)) → MARK(x1)
EQACTIVE(s(X), s(Y)) → EQACTIVE(X, Y)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(take(x1, x2)) → MARK(x1)
MARK(eq(x1, x2)) → EQACTIVE(x1, x2)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(length(x1)) → MARK(x1)
MARK(inf(x1)) → INFACTIVE(mark(x1))

The TRS R consists of the following rules:

mark(eq(x1, x2)) → eqActive(x1, x2)
eqActive(x1, x2) → eq(x1, x2)
mark(inf(x1)) → infActive(mark(x1))
infActive(x1) → inf(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(0) → 0
mark(true) → true
mark(s(x1)) → s(x1)
mark(false) → false
mark(cons(x1, x2)) → cons(x1, x2)
mark(nil) → nil
eqActive(0, 0) → true
eqActive(s(X), s(Y)) → eqActive(X, Y)
eqActive(X, Y) → false
infActive(X) → cons(X, inf(s(X)))
takeActive(0, X) → nil
takeActive(s(X), cons(Y, L)) → cons(Y, take(X, L))
lengthActive(nil) → 0
lengthActive(cons(X, L)) → s(length(L))

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

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

MARK(take(x1, x2)) → MARK(x2)
MARK(inf(x1)) → MARK(x1)
EQACTIVE(s(X), s(Y)) → EQACTIVE(X, Y)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(take(x1, x2)) → MARK(x1)
MARK(eq(x1, x2)) → EQACTIVE(x1, x2)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(length(x1)) → MARK(x1)
MARK(inf(x1)) → INFACTIVE(mark(x1))

The TRS R consists of the following rules:

mark(eq(x1, x2)) → eqActive(x1, x2)
eqActive(x1, x2) → eq(x1, x2)
mark(inf(x1)) → infActive(mark(x1))
infActive(x1) → inf(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(0) → 0
mark(true) → true
mark(s(x1)) → s(x1)
mark(false) → false
mark(cons(x1, x2)) → cons(x1, x2)
mark(nil) → nil
eqActive(0, 0) → true
eqActive(s(X), s(Y)) → eqActive(X, Y)
eqActive(X, Y) → false
infActive(X) → cons(X, inf(s(X)))
takeActive(0, X) → nil
takeActive(s(X), cons(Y, L)) → cons(Y, take(X, L))
lengthActive(nil) → 0
lengthActive(cons(X, L)) → s(length(L))

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

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

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

EQACTIVE(s(X), s(Y)) → EQACTIVE(X, Y)

The TRS R consists of the following rules:

mark(eq(x1, x2)) → eqActive(x1, x2)
eqActive(x1, x2) → eq(x1, x2)
mark(inf(x1)) → infActive(mark(x1))
infActive(x1) → inf(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(0) → 0
mark(true) → true
mark(s(x1)) → s(x1)
mark(false) → false
mark(cons(x1, x2)) → cons(x1, x2)
mark(nil) → nil
eqActive(0, 0) → true
eqActive(s(X), s(Y)) → eqActive(X, Y)
eqActive(X, Y) → false
infActive(X) → cons(X, inf(s(X)))
takeActive(0, X) → nil
takeActive(s(X), cons(Y, L)) → cons(Y, take(X, L))
lengthActive(nil) → 0
lengthActive(cons(X, L)) → s(length(L))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

              ↳ QDP

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

EQACTIVE(s(X), s(Y)) → EQACTIVE(X, Y)

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

EQACTIVE(s(X), s(Y)) → EQACTIVE(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

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

MARK(take(x1, x2)) → MARK(x2)
MARK(inf(x1)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
MARK(length(x1)) → MARK(x1)

The TRS R consists of the following rules:

mark(eq(x1, x2)) → eqActive(x1, x2)
eqActive(x1, x2) → eq(x1, x2)
mark(inf(x1)) → infActive(mark(x1))
infActive(x1) → inf(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(0) → 0
mark(true) → true
mark(s(x1)) → s(x1)
mark(false) → false
mark(cons(x1, x2)) → cons(x1, x2)
mark(nil) → nil
eqActive(0, 0) → true
eqActive(s(X), s(Y)) → eqActive(X, Y)
eqActive(X, Y) → false
infActive(X) → cons(X, inf(s(X)))
takeActive(0, X) → nil
takeActive(s(X), cons(Y, L)) → cons(Y, take(X, L))
lengthActive(nil) → 0
lengthActive(cons(X, L)) → s(length(L))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

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

MARK(take(x1, x2)) → MARK(x2)
MARK(inf(x1)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
MARK(length(x1)) → MARK(x1)

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

MARK(take(x1, x2)) → MARK(x2)
The graph contains the following edges 1 > 1
MARK(inf(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(take(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(length(x1)) → MARK(x1)
The graph contains the following edges 1 > 1