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

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

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

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
length: empty set
nil: empty set
0: empty set
length1: empty set

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
length: empty set
nil: empty set
0: empty set
length1: empty set

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:

from(X) → cons(X)
length → 0
length → s(length1)
length1 → length

Q is empty.

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

from(X) → cons(X)
length → 0
length → s(length1)
length1 → length

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

from(X) → cons(X)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(cons(x₁)) = 2·x₁
POL(from(x₁)) = 1 + 2·x₁
POL(length) = 0
POL(length1) = 0
POL(s(x₁)) = 2·x₁

↳ 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:

length → 0
length → s(length1)
length1 → length

Q is empty.

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

length → 0
length → s(length1)
length1 → length

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

length → 0

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(length) = 1
POL(length1) = 1
POL(s(x₁)) = x₁

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

length → s(length1)
length1 → length

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

length → s(length1)
length1 → length

The set Q consists of the following terms:

length
length1

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

LENGTH → LENGTH1
LENGTH1 → LENGTH

The TRS R consists of the following rules:

length → s(length1)
length1 → length

The set Q consists of the following terms:

length
length1

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

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ UsableRulesProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

LENGTH → LENGTH1
LENGTH1 → LENGTH

The TRS R consists of the following rules:

length → s(length1)
length1 → length

The set Q consists of the following terms:

length
length1

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

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ UsableRulesProof

                        ↳ QDP

                          ↳ QReductionProof

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

LENGTH → LENGTH1
LENGTH1 → LENGTH

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

length
length1

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.

length
length1

↳ CSR

  ↳ Lucas-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ 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:

LENGTH → LENGTH1
LENGTH1 → LENGTH

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 narrowing to the left:

The TRS P consists of the following rules:

LENGTH → LENGTH1
LENGTH1 → LENGTH

The TRS R consists of the following rules:none

s = LENGTH1 evaluates to t =LENGTH1

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

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

LENGTH1 → LENGTH
with rule LENGTH1 → LENGTH at position [] and matcher [ ]

LENGTH → LENGTH1
with rule LENGTH → LENGTH1

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

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:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

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:

LENGTH(consInact(X, Y)) → A(Y)
A(fromInact(x1)) → FROM(x1)
LENGTH1(X) → LENGTH(a(X))
A(consInact(x1, x2)) → CONS(x1, x2)
LENGTH(consInact(X, Y)) → LENGTH1(a(Y))
LENGTH1(X) → A(X)
A(nilInact) → NIL
FROM(X) → CONS(X, fromInact(s(X)))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

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:

LENGTH(consInact(X, Y)) → A(Y)
A(fromInact(x1)) → FROM(x1)
LENGTH1(X) → LENGTH(a(X))
A(consInact(x1, x2)) → CONS(x1, x2)
LENGTH(consInact(X, Y)) → LENGTH1(a(Y))
LENGTH1(X) → A(X)
A(nilInact) → NIL
FROM(X) → CONS(X, fromInact(s(X)))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

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 6 less nodes.

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

LENGTH1(X) → LENGTH(a(X))
LENGTH(consInact(X, Y)) → LENGTH1(a(Y))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

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

LENGTH1(consInact(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(nilInact) → LENGTH(nil)
LENGTH1(x0) → LENGTH(x0)
LENGTH1(fromInact(x0)) → LENGTH(from(x0))

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

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

LENGTH1(nilInact) → LENGTH(nil)
LENGTH(consInact(X, Y)) → LENGTH1(a(Y))
LENGTH1(consInact(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(fromInact(x0)) → LENGTH(from(x0))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule LENGTH1(nilInact) → LENGTH(nil) at position [0] we obtained the following new rules:

LENGTH1(nilInact) → LENGTH(nilInact)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

LENGTH1(nilInact) → LENGTH(nilInact)
LENGTH(consInact(X, Y)) → LENGTH1(a(Y))
LENGTH1(consInact(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(fromInact(x0)) → LENGTH(from(x0))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

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

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ NonTerminationProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

LENGTH(consInact(X, Y)) → LENGTH1(a(Y))
LENGTH1(consInact(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(fromInact(x0)) → LENGTH(from(x0))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

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 narrowing to the left:

The TRS P consists of the following rules:

LENGTH(consInact(X, Y)) → LENGTH1(a(Y))
LENGTH1(consInact(x0, x1)) → LENGTH(cons(x0, x1))
LENGTH1(x0) → LENGTH(x0)
LENGTH1(fromInact(x0)) → LENGTH(from(x0))

The TRS R consists of the following rules:

from(X) → cons(X, fromInact(s(X)))
length(nilInact) → 0
length(consInact(X, Y)) → s(length1(a(Y)))
length1(X) → length(a(X))
a(x) → x
from(x1) → fromInact(x1)
a(fromInact(x1)) → from(x1)
nil → nilInact
a(nilInact) → nil
cons(x1, x2) → consInact(x1, x2)
a(consInact(x1, x2)) → cons(x1, x2)

s = LENGTH1(a(fromInact(x1))) evaluates to t =LENGTH1(a(fromInact(s(x1))))

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

Matcher: [x1 / s(x1)]
Semiunifier: [ ]

Rewriting sequence

LENGTH1(a(fromInact(x1))) → LENGTH1(from(x1))
with rule a(fromInact(x1')) → from(x1') at position [0] and matcher [x1' / x1]

LENGTH1(from(x1)) → LENGTH1(cons(x1, fromInact(s(x1))))
with rule from(X) → cons(X, fromInact(s(X))) at position [0] and matcher [X / x1]

LENGTH1(cons(x1, fromInact(s(x1)))) → LENGTH1(consInact(x1, fromInact(s(x1))))
with rule cons(x1', x2) → consInact(x1', x2) at position [0] and matcher [x1' / x1, x2 / fromInact(s(x1))]

LENGTH1(consInact(x1, fromInact(s(x1)))) → LENGTH(consInact(x1, fromInact(s(x1))))
with rule LENGTH1(x0) → LENGTH(x0) at position [] and matcher [x0 / consInact(x1, fromInact(s(x1)))]

LENGTH(consInact(x1, fromInact(s(x1)))) → LENGTH1(a(fromInact(s(x1))))
with rule LENGTH(consInact(X, Y)) → LENGTH1(a(Y))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

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(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

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:

LENGTHACTIVE(cons(X, Y)) → LENGTH1ACTIVE(Y)
MARK(s(x1)) → MARK(x1)
MARK(length1(x1)) → LENGTH1ACTIVE(x1)
MARK(from(x1)) → FROMACTIVE(mark(x1))
LENGTH1ACTIVE(X) → LENGTHACTIVE(X)
MARK(length(x1)) → LENGTHACTIVE(x1)
MARK(from(x1)) → MARK(x1)
FROMACTIVE(X) → MARK(X)
MARK(cons(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

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:

LENGTHACTIVE(cons(X, Y)) → LENGTH1ACTIVE(Y)
MARK(s(x1)) → MARK(x1)
MARK(length1(x1)) → LENGTH1ACTIVE(x1)
MARK(from(x1)) → FROMACTIVE(mark(x1))
LENGTH1ACTIVE(X) → LENGTHACTIVE(X)
MARK(length(x1)) → LENGTHACTIVE(x1)
MARK(from(x1)) → MARK(x1)
FROMACTIVE(X) → MARK(X)
MARK(cons(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

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 2 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:

LENGTHACTIVE(cons(X, Y)) → LENGTH1ACTIVE(Y)
LENGTH1ACTIVE(X) → LENGTHACTIVE(X)

The TRS R consists of the following rules:

mark(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

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

  ↳ 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:

LENGTHACTIVE(cons(X, Y)) → LENGTH1ACTIVE(Y)
LENGTH1ACTIVE(X) → LENGTHACTIVE(X)

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:

LENGTH1ACTIVE(X) → LENGTHACTIVE(X)
The graph contains the following edges 1 >= 1
LENGTHACTIVE(cons(X, Y)) → LENGTH1ACTIVE(Y)
The graph contains the following edges 1 > 1

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

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

MARK(s(x1)) → MARK(x1)
MARK(from(x1)) → FROMACTIVE(mark(x1))
MARK(from(x1)) → MARK(x1)
FROMACTIVE(X) → MARK(X)
MARK(cons(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

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.

MARK(from(x1)) → FROMACTIVE(mark(x1))
MARK(from(x1)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

MARK(s(x1)) → MARK(x1)
FROMACTIVE(X) → MARK(X)
MARK(cons(x1, x2)) → MARK(x1)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(FROMACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁
POL(from(x₁)) = 1 + x₁
POL(fromActive(x₁)) = 1 + x₁
POL(length(x₁)) = 0
POL(length1(x₁)) = 0
POL(length1Active(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁

The following usable rules [17] were oriented:

lengthActive(cons(X, Y)) → s(length1Active(Y))
mark(from(x1)) → fromActive(mark(x1))
mark(s(x1)) → s(mark(x1))
lengthActive(x1) → length(x1)
lengthActive(nil) → 0
mark(length1(x1)) → length1Active(x1)
mark(nil) → nil
fromActive(X) → cons(mark(X), from(s(X)))
length1Active(x1) → length1(x1)
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
length1Active(X) → lengthActive(X)
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

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

MARK(s(x1)) → MARK(x1)
FROMACTIVE(X) → MARK(X)
MARK(cons(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

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

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ UsableRulesProof

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

MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(from(x1)) → fromActive(mark(x1))
fromActive(x1) → from(x1)
mark(length(x1)) → lengthActive(x1)
lengthActive(x1) → length(x1)
mark(length1(x1)) → length1Active(x1)
length1Active(x1) → length1(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(0) → 0
fromActive(X) → cons(mark(X), from(s(X)))
lengthActive(nil) → 0
lengthActive(cons(X, Y)) → s(length1Active(Y))
length1Active(X) → lengthActive(X)

↳ CSR

  ↳ Lucas-Transformation

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

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

MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)

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

MARK(s(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(cons(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1