MAYBE Termination proof of ../tpdb/TRS/CSR_Maude/length-lazy-list/LengthOfFiniteLists_nosorts.trs
Termination of the following Term Rewriting System could not be shown:

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

zeros → cons(0, zeros)
and(tt, X) → X
length(nil) → 0
length(cons(N, L)) → s(length(L))

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
and: {1}
tt: empty set
length: {1}
nil: empty set
s: {1}


↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zeros)
and(tt, X) → X
length(nil) → 0
length(cons(N, L)) → s(length(L))

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
and: {1}
tt: empty set
length: {1}
nil: empty set
s: {1}

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

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
and(tt, X) → a(X)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
and(tt, X) → a(X)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

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

and(tt, X) → a(X)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = x1   
POL(and(x1, x2)) = x1 + 2·x2   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(nil) = 0   
POL(s(x1)) = 2·x1   
POL(tt) = 1   
POL(zeros) = 0   
POL(zerosInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

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(nil) → 0
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(nil) = 2   
POL(s(x1)) = 2·x1   
POL(zeros) = 0   
POL(zerosInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

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

zeros → zerosInact
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = 2·x1   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(s(x1)) = x1   
POL(zeros) = 2   
POL(zerosInact) = 1   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
a(zerosInact) → zeros

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

a(x) → x
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = 1 + x1   
POL(cons(x1, x2)) = 1 + 2·x1 + x2   
POL(length(x1)) = x1   
POL(s(x1)) = x1   
POL(zeros) = 1   
POL(zerosInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

Q is empty.

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

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)


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(cons(N, L)) → A(L)
LENGTH(cons(N, L)) → LENGTH(a(L))
A(zerosInact) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → A(L)
LENGTH(cons(N, L)) → LENGTH(a(L))
A(zerosInact) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → LENGTH(a(L))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → LENGTH(a(L))

The TRS R consists of the following rules:

a(zerosInact) → zeros
zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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(cons(x0, x1))



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → LENGTH(a(L))

The TRS R consists of the following rules:

a(zerosInact) → zeros
zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
a(zerosInact)

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)

The TRS R consists of the following rules:

a(zerosInact) → zeros
zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
a(zerosInact)

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
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
a(zerosInact)

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.

a(zerosInact)



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros

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
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))

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

zeros

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

zeros



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ Instantiation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))

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

LENGTH(cons(0, zerosInact)) → LENGTH(cons(0, zerosInact))



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ Instantiation
                                                                    ↳ QDP
                                                                      ↳ NonTerminationProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(0, zerosInact)) → LENGTH(cons(0, zerosInact))

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:

LENGTH(cons(0, zerosInact)) → LENGTH(cons(0, zerosInact))

The TRS R consists of the following rules:none


s = LENGTH(cons(0, zerosInact)) evaluates to t =LENGTH(cons(0, zerosInact))

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



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LENGTH(cons(0, zerosInact)) to LENGTH(cons(0, zerosInact)).




We applied the Incomplete Giesl Middeldorp [11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(nil) → nil
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
andActive(tt, X) → mark(X)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(nil) → nil
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
andActive(tt, X) → mark(X)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

lengthActive(nil) → 0
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(and(x1, x2)) = 2·x1 + x2   
POL(andActive(x1, x2)) = 2·x1 + x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(lengthActive(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nil) = 1   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
POL(zerosActive) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(nil) → nil
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
andActive(tt, X) → mark(X)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(nil) → nil
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
andActive(tt, X) → mark(X)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

mark(nil) → nil
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(and(x1, x2)) = 2·x1 + 2·x2   
POL(andActive(x1, x2)) = 2·x1 + 2·x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(lengthActive(x1)) = 2·x1   
POL(mark(x1)) = 2·x1   
POL(nil) = 2   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
POL(zerosActive) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
andActive(tt, X) → mark(X)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
andActive(tt, X) → mark(X)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

andActive(tt, X) → mark(X)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(and(x1, x2)) = 2 + 2·x1 + x2   
POL(andActive(x1, x2)) = 2 + 2·x1 + x2   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(lengthActive(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
POL(zerosActive) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

zerosActive → zeros
mark(and(x1, x2)) → andActive(mark(x1), x2)
mark(tt) → tt
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(and(x1, x2)) = 1 + x1 + 2·x2   
POL(andActive(x1, x2)) = 1 + x1 + 2·x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = x1   
POL(lengthActive(x1)) = x1   
POL(mark(x1)) = 2·x1   
POL(s(x1)) = x1   
POL(tt) = 1   
POL(zeros) = 1   
POL(zerosActive) = 2   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
andActive(x1, x2) → and(x1, x2)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

andActive(x1, x2) → and(x1, x2)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(and(x1, x2)) = x1 + x2   
POL(andActive(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(length(x1)) = x1   
POL(lengthActive(x1)) = x1   
POL(mark(x1)) = x1   
POL(s(x1)) = x1   
POL(zeros) = 0   
POL(zerosActive) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

mark(length(x1)) → lengthActive(mark(x1))
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = 1 + 2·x1   
POL(lengthActive(x1)) = 1 + 2·x1   
POL(mark(x1)) = 2·x1   
POL(s(x1)) = x1   
POL(zeros) = 0   
POL(zerosActive) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

lengthActive(x1) → length(x1)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(length(x1)) = x1   
POL(lengthActive(x1)) = 1 + x1   
POL(mark(x1)) = x1   
POL(s(x1)) = x1   
POL(zeros) = 0   
POL(zerosActive) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

mark(0) → 0
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(lengthActive(x1)) = x1   
POL(mark(x1)) = 1 + x1   
POL(s(x1)) = x1   
POL(zeros) = 0   
POL(zerosActive) = 1   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

mark(zeros) → zerosActive
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

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

mark(cons(x1, x2)) → cons(mark(x1), x2)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(cons(x1, x2)) = 2 + x1 + 2·x2   
POL(lengthActive(x1)) = x1   
POL(mark(x1)) = 2 + 2·x1   
POL(s(x1)) = x1   
POL(zeros) = 0   
POL(zerosActive) = 2   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

Q is empty.

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))


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

MARK(s(x1)) → MARK(x1)
MARK(zeros) → ZEROSACTIVE
LENGTHACTIVE(cons(N, L)) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → MARK(L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(s(x1)) → MARK(x1)
MARK(zeros) → ZEROSACTIVE
LENGTHACTIVE(cons(N, L)) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → MARK(L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                      ↳ QDP
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(s(x1)) → MARK(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                      ↳ QDP
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(s(x1)) → MARK(x1)

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

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))

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

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ QDPSizeChangeProof
                                                      ↳ QDP
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(s(x1)) → MARK(x1)

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: 



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(N, L)) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)
lengthActive(cons(N, L)) → s(lengthActive(mark(L)))

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(N, L)) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive
lengthActive(cons(x0, x1))

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

lengthActive(cons(x0, x1))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(N, L)) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
mark(s(x1)) → s(mark(x1))
zerosActive → cons(0, zeros)

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive

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

Strictly oriented rules of the TRS R:

mark(s(x1)) → s(mark(x1))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0   
POL(LENGTHACTIVE(x1)) = 2·x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(mark(x1)) = 2·x1   
POL(s(x1)) = 1 + 2·x1   
POL(zeros) = 0   
POL(zerosActive) = 0   



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(N, L)) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → cons(0, zeros)

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(zerosActive)



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(zerosActive)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → cons(0, zeros)

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
                                                                          ↳ QDP
                                                                            ↳ QReductionProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(zerosActive)

The TRS R consists of the following rules:

zerosActive → cons(0, zeros)

The set Q consists of the following terms:

mark(zeros)
mark(s(x0))
zerosActive

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.

mark(zeros)
mark(s(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
                                                                          ↳ QDP
                                                                            ↳ QReductionProof
                                                                              ↳ QDP
                                                                                ↳ Rewriting
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(zerosActive)

The TRS R consists of the following rules:

zerosActive → cons(0, zeros)

The set Q consists of the following terms:

zerosActive

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(cons(0, zeros))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
                                                                          ↳ QDP
                                                                            ↳ QReductionProof
                                                                              ↳ QDP
                                                                                ↳ Rewriting
                                                                                  ↳ QDP
                                                                                    ↳ UsableRulesProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(cons(0, zeros))

The TRS R consists of the following rules:

zerosActive → cons(0, zeros)

The set Q consists of the following terms:

zerosActive

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
                                                                          ↳ QDP
                                                                            ↳ QReductionProof
                                                                              ↳ QDP
                                                                                ↳ Rewriting
                                                                                  ↳ QDP
                                                                                    ↳ UsableRulesProof
                                                                                      ↳ QDP
                                                                                        ↳ QReductionProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(cons(0, zeros))

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

zerosActive

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.

zerosActive



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
                                                                          ↳ QDP
                                                                            ↳ QReductionProof
                                                                              ↳ QDP
                                                                                ↳ Rewriting
                                                                                  ↳ QDP
                                                                                    ↳ UsableRulesProof
                                                                                      ↳ QDP
                                                                                        ↳ QReductionProof
                                                                                          ↳ QDP
                                                                                            ↳ Instantiation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(y0, zeros)) → LENGTHACTIVE(cons(0, zeros))

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

LENGTHACTIVE(cons(0, zeros)) → LENGTHACTIVE(cons(0, zeros))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RRRPoloQTRSProof
                                    ↳ QTRS
                                      ↳ RRRPoloQTRSProof
                                        ↳ QTRS
                                          ↳ Overlay + Local Confluence
                                            ↳ QTRS
                                              ↳ DependencyPairsProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ AND
                                                      ↳ QDP
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ RuleRemovalProof
                                                                  ↳ QDP
                                                                    ↳ Narrowing
                                                                      ↳ QDP
                                                                        ↳ UsableRulesProof
                                                                          ↳ QDP
                                                                            ↳ QReductionProof
                                                                              ↳ QDP
                                                                                ↳ Rewriting
                                                                                  ↳ QDP
                                                                                    ↳ UsableRulesProof
                                                                                      ↳ QDP
                                                                                        ↳ QReductionProof
                                                                                          ↳ QDP
                                                                                            ↳ Instantiation
                                                                                              ↳ QDP
                                                                                                ↳ NonTerminationProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTHACTIVE(cons(0, zeros)) → LENGTHACTIVE(cons(0, zeros))

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

The TRS P consists of the following rules:

LENGTHACTIVE(cons(0, zeros)) → LENGTHACTIVE(cons(0, zeros))

The TRS R consists of the following rules:none


s = LENGTHACTIVE(cons(0, zeros)) evaluates to t =LENGTHACTIVE(cons(0, zeros))

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



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LENGTHACTIVE(cons(0, zeros)) to LENGTHACTIVE(cons(0, zeros)).




We applied the Improved Ferreira Ribeiro [5,11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
and(tt, X) → a(X)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
and(tt, X) → a(X)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

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

and(tt, X) → a(X)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = x1   
POL(and(x1, x2)) = x1 + 2·x2   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(nil) = 0   
POL(s(x1)) = 2·x1   
POL(tt) = 1   
POL(zeros) = 0   
POL(zerosInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
length(nil) → 0
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

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(nil) → 0
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(nil) = 2   
POL(s(x1)) = 2·x1   
POL(zeros) = 0   
POL(zerosInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
zeros → zerosInact
a(zerosInact) → zeros

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

zeros → zerosInact
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = 2·x1   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(s(x1)) = x1   
POL(zeros) = 2   
POL(zerosInact) = 1   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
a(zerosInact) → zeros

Q is empty.

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(x) → x
a(zerosInact) → zeros

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

a(x) → x
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(a(x1)) = 1 + x1   
POL(cons(x1, x2)) = 1 + 2·x1 + x2   
POL(length(x1)) = x1   
POL(s(x1)) = x1   
POL(zeros) = 1   
POL(zerosInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

Q is empty.

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
  ↳ Complete Giesl Middeldorp-Transformation

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

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)


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(cons(N, L)) → A(L)
LENGTH(cons(N, L)) → LENGTH(a(L))
A(zerosInact) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → A(L)
LENGTH(cons(N, L)) → LENGTH(a(L))
A(zerosInact) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → LENGTH(a(L))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)
length(cons(N, L)) → s(length(a(L)))
a(zerosInact) → zeros

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → LENGTH(a(L))

The TRS R consists of the following rules:

a(zerosInact) → zeros
zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
length(cons(x0, x1))
a(zerosInact)

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(cons(x0, x1))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(N, L)) → LENGTH(a(L))

The TRS R consists of the following rules:

a(zerosInact) → zeros
zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
a(zerosInact)

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)

The TRS R consists of the following rules:

a(zerosInact) → zeros
zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
a(zerosInact)

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros
a(zerosInact)

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.

a(zerosInact)



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(zeros)

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))

The TRS R consists of the following rules:

zeros → cons(0, zerosInact)

The set Q consists of the following terms:

zeros

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))

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

zeros

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

zeros



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ Instantiation
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(y0, zerosInact)) → LENGTH(cons(0, zerosInact))

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

LENGTH(cons(0, zerosInact)) → LENGTH(cons(0, zerosInact))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ Overlay + Local Confluence
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ Narrowing
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ Instantiation
                                                                    ↳ QDP
                                                                      ↳ NonTerminationProof
  ↳ Complete Giesl Middeldorp-Transformation

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

LENGTH(cons(0, zerosInact)) → LENGTH(cons(0, zerosInact))

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:

LENGTH(cons(0, zerosInact)) → LENGTH(cons(0, zerosInact))

The TRS R consists of the following rules:none


s = LENGTH(cons(0, zerosInact)) evaluates to t =LENGTH(cons(0, zerosInact))

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



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LENGTH(cons(0, zerosInact)) to LENGTH(cons(0, zerosInact)).




We applied the Complete Giesl Middeldorp [11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof

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

active(zeros) → mark(cons(0, zeros))
active(and(tt, X)) → mark(X)
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))


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

active(zeros) → mark(cons(0, zeros))
active(and(tt, X)) → mark(X)
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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

active(length(nil)) → mark(0)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(and(x1, x2)) = x1 + 2·x2   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(length(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nil) = 2   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   
POL(s(x1)) = x1   
POL(top(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof

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

active(zeros) → mark(cons(0, zeros))
active(and(tt, X)) → mark(X)
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))


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

active(zeros) → mark(cons(0, zeros))
active(and(tt, X)) → mark(X)
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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

active(and(tt, X)) → mark(X)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 2·x1 + 2·x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = x1   
POL(mark(x1)) = x1   
POL(nil) = 0   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   
POL(s(x1)) = x1   
POL(top(x1)) = x1   
POL(tt) = 1   
POL(zeros) = 0   




↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof

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

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))


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

AND(ok(x1), ok(x2)) → AND(x1, x2)
TOP(mark(x)) → PROPER(x)
ACTIVE(zeros) → CONS(0, zeros)
PROPER(and(x1, x2)) → PROPER(x1)
LENGTH(ok(x1)) → LENGTH(x1)
PROPER(length(x1)) → PROPER(x1)
S(mark(x1)) → S(x1)
ACTIVE(length(cons(N, L))) → LENGTH(L)
PROPER(and(x1, x2)) → AND(proper(x1), proper(x2))
LENGTH(mark(x1)) → LENGTH(x1)
ACTIVE(and(x1, x2)) → ACTIVE(x1)
TOP(mark(x)) → TOP(proper(x))
PROPER(s(x1)) → S(proper(x1))
S(ok(x1)) → S(x1)
ACTIVE(s(x1)) → ACTIVE(x1)
CONS(mark(x1), x2) → CONS(x1, x2)
ACTIVE(cons(x1, x2)) → CONS(active(x1), x2)
ACTIVE(length(cons(N, L))) → S(length(L))
ACTIVE(length(x1)) → ACTIVE(x1)
ACTIVE(cons(x1, x2)) → ACTIVE(x1)
PROPER(cons(x1, x2)) → PROPER(x1)
ACTIVE(length(x1)) → LENGTH(active(x1))
PROPER(length(x1)) → LENGTH(proper(x1))
TOP(ok(x)) → ACTIVE(x)
ACTIVE(s(x1)) → S(active(x1))
PROPER(cons(x1, x2)) → CONS(proper(x1), proper(x2))
PROPER(s(x1)) → PROPER(x1)
TOP(ok(x)) → TOP(active(x))
PROPER(cons(x1, x2)) → PROPER(x2)
CONS(ok(x1), ok(x2)) → CONS(x1, x2)
PROPER(and(x1, x2)) → PROPER(x2)
ACTIVE(and(x1, x2)) → AND(active(x1), x2)
AND(mark(x1), x2) → AND(x1, x2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof

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

AND(ok(x1), ok(x2)) → AND(x1, x2)
TOP(mark(x)) → PROPER(x)
ACTIVE(zeros) → CONS(0, zeros)
PROPER(and(x1, x2)) → PROPER(x1)
LENGTH(ok(x1)) → LENGTH(x1)
PROPER(length(x1)) → PROPER(x1)
S(mark(x1)) → S(x1)
ACTIVE(length(cons(N, L))) → LENGTH(L)
PROPER(and(x1, x2)) → AND(proper(x1), proper(x2))
LENGTH(mark(x1)) → LENGTH(x1)
ACTIVE(and(x1, x2)) → ACTIVE(x1)
TOP(mark(x)) → TOP(proper(x))
PROPER(s(x1)) → S(proper(x1))
S(ok(x1)) → S(x1)
ACTIVE(s(x1)) → ACTIVE(x1)
CONS(mark(x1), x2) → CONS(x1, x2)
ACTIVE(cons(x1, x2)) → CONS(active(x1), x2)
ACTIVE(length(cons(N, L))) → S(length(L))
ACTIVE(length(x1)) → ACTIVE(x1)
ACTIVE(cons(x1, x2)) → ACTIVE(x1)
PROPER(cons(x1, x2)) → PROPER(x1)
ACTIVE(length(x1)) → LENGTH(active(x1))
PROPER(length(x1)) → LENGTH(proper(x1))
TOP(ok(x)) → ACTIVE(x)
ACTIVE(s(x1)) → S(active(x1))
PROPER(cons(x1, x2)) → CONS(proper(x1), proper(x2))
PROPER(s(x1)) → PROPER(x1)
TOP(ok(x)) → TOP(active(x))
PROPER(cons(x1, x2)) → PROPER(x2)
CONS(ok(x1), ok(x2)) → CONS(x1, x2)
PROPER(and(x1, x2)) → PROPER(x2)
ACTIVE(and(x1, x2)) → AND(active(x1), x2)
AND(mark(x1), x2) → AND(x1, x2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

S(ok(x1)) → S(x1)
S(mark(x1)) → S(x1)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

S(ok(x1)) → S(x1)
S(mark(x1)) → S(x1)

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

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

S(ok(x1)) → S(x1)
S(mark(x1)) → S(x1)

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: 



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

LENGTH(mark(x1)) → LENGTH(x1)
LENGTH(ok(x1)) → LENGTH(x1)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

LENGTH(mark(x1)) → LENGTH(x1)
LENGTH(ok(x1)) → LENGTH(x1)

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

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

LENGTH(ok(x1)) → LENGTH(x1)
LENGTH(mark(x1)) → LENGTH(x1)

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: 



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

AND(ok(x1), ok(x2)) → AND(x1, x2)
AND(mark(x1), x2) → AND(x1, x2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

AND(ok(x1), ok(x2)) → AND(x1, x2)
AND(mark(x1), x2) → AND(x1, x2)

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

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

AND(ok(x1), ok(x2)) → AND(x1, x2)
AND(mark(x1), x2) → AND(x1, x2)

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

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



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

CONS(mark(x1), x2) → CONS(x1, x2)
CONS(ok(x1), ok(x2)) → CONS(x1, x2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

CONS(mark(x1), x2) → CONS(x1, x2)
CONS(ok(x1), ok(x2)) → CONS(x1, x2)

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

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

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

CONS(mark(x1), x2) → CONS(x1, x2)
CONS(ok(x1), ok(x2)) → CONS(x1, x2)

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

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



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP

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

PROPER(and(x1, x2)) → PROPER(x1)
PROPER(s(x1)) → PROPER(x1)
PROPER(length(x1)) → PROPER(x1)
PROPER(cons(x1, x2)) → PROPER(x1)
PROPER(cons(x1, x2)) → PROPER(x2)
PROPER(and(x1, x2)) → PROPER(x2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP
                      ↳ QDP

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

PROPER(and(x1, x2)) → PROPER(x1)
PROPER(s(x1)) → PROPER(x1)
PROPER(length(x1)) → PROPER(x1)
PROPER(cons(x1, x2)) → PROPER(x1)
PROPER(cons(x1, x2)) → PROPER(x2)
PROPER(and(x1, x2)) → PROPER(x2)

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

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

active(zeros)
proper(zeros)
active(cons(x0, x1))
proper(cons(x0, x1))
proper(0)
active(and(x0, x1))
proper(and(x0, x1))
proper(tt)
active(length(x0))
proper(length(x0))
proper(nil)
active(s(x0))
proper(s(x0))
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP

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

PROPER(and(x1, x2)) → PROPER(x1)
PROPER(length(x1)) → PROPER(x1)
PROPER(s(x1)) → PROPER(x1)
PROPER(cons(x1, x2)) → PROPER(x1)
PROPER(cons(x1, x2)) → PROPER(x2)
PROPER(and(x1, x2)) → PROPER(x2)

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

cons(mark(x0), x1)
cons(ok(x0), ok(x1))
and(mark(x0), x1)
and(ok(x0), ok(x1))
length(mark(x0))
length(ok(x0))
s(mark(x0))
s(ok(x0))

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: 



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP

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

ACTIVE(length(x1)) → ACTIVE(x1)
ACTIVE(cons(x1, x2)) → ACTIVE(x1)
ACTIVE(and(x1, x2)) → ACTIVE(x1)
ACTIVE(s(x1)) → ACTIVE(x1)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP

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

ACTIVE(length(x1)) → ACTIVE(x1)
ACTIVE(cons(x1, x2)) → ACTIVE(x1)
ACTIVE(and(x1, x2)) → ACTIVE(x1)
ACTIVE(s(x1)) → ACTIVE(x1)

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

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

active(zeros)
proper(zeros)
active(cons(x0, x1))
proper(cons(x0, x1))
proper(0)
active(and(x0, x1))
proper(and(x0, x1))
proper(tt)
active(length(x0))
proper(length(x0))
proper(nil)
active(s(x0))
proper(s(x0))
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP

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

ACTIVE(length(x1)) → ACTIVE(x1)
ACTIVE(cons(x1, x2)) → ACTIVE(x1)
ACTIVE(and(x1, x2)) → ACTIVE(x1)
ACTIVE(s(x1)) → ACTIVE(x1)

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

cons(mark(x0), x1)
cons(ok(x0), ok(x1))
and(mark(x0), x1)
and(ok(x0), ok(x1))
length(mark(x0))
length(ok(x0))
s(mark(x0))
s(ok(x0))

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: 



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof

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

TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
proper(zeros) → ok(zeros)
active(cons(x1, x2)) → cons(active(x1), x2)
cons(mark(x1), x2) → mark(cons(x1, x2))
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(0) → ok(0)
active(and(x1, x2)) → and(active(x1), x2)
and(mark(x1), x2) → mark(and(x1, x2))
proper(and(x1, x2)) → and(proper(x1), proper(x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
proper(tt) → ok(tt)
active(length(x1)) → length(active(x1))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))
length(ok(x1)) → ok(length(x1))
proper(nil) → ok(nil)
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
s(ok(x1)) → ok(s(x1))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof

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

TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))
top(mark(x0))
top(ok(x0))

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.

top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Narrowing

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

TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(ok(x)) → TOP(active(x)) at position [0] we obtained the following new rules:

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(zeros)) → TOP(mark(cons(0, zeros)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
TOP(ok(length(x0))) → TOP(length(active(x0)))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing

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

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
TOP(mark(x)) → TOP(proper(x))
TOP(ok(zeros)) → TOP(mark(cons(0, zeros)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(ok(length(x0))) → TOP(length(active(x0)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(mark(x)) → TOP(proper(x)) at position [0] we obtained the following new rules:

TOP(mark(nil)) → TOP(ok(nil))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(zeros)) → TOP(ok(zeros))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(tt)) → TOP(ok(tt))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof

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

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(ok(zeros)) → TOP(mark(cons(0, zeros)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(zeros)) → TOP(ok(zeros))
TOP(ok(length(x0))) → TOP(length(active(x0)))
TOP(mark(tt)) → TOP(ok(tt))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(nil)) → TOP(ok(nil))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(mark(0)) → TOP(ok(0))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))

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

↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ QDPOrderProof

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

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(ok(zeros)) → TOP(mark(cons(0, zeros)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(ok(length(x0))) → TOP(length(active(x0)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))

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.


TOP(ok(zeros)) → TOP(mark(cons(0, zeros)))
The remaining pairs can at least be oriented weakly.

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(ok(length(x0))) → TOP(length(active(x0)))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = 0   
POL(and(x1, x2)) = 0   
POL(cons(x1, x2)) = 0   
POL(length(x1)) = 0   
POL(mark(x1)) = 0   
POL(nil) = 0   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   
POL(s(x1)) = 0   
POL(tt) = 0   
POL(zeros) = 1   

The following usable rules [17] were oriented:

length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
s(mark(x1)) → mark(s(x1))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
s(ok(x1)) → ok(s(x1))
cons(mark(x1), x2) → mark(cons(x1, x2))
length(mark(x1)) → mark(length(x1))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ QDPOrderProof
                                              ↳ QDP
                                                ↳ QDPOrderProof

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

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(ok(length(x0))) → TOP(length(active(x0)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))

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.


TOP(ok(length(cons(x0, x1)))) → TOP(mark(s(length(x1))))
The remaining pairs can at least be oriented weakly.

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(ok(length(x0))) → TOP(length(active(x0)))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = x1   
POL(and(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1   
POL(length(x1)) = 1 + x1   
POL(mark(x1)) = x1   
POL(nil) = 0   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   
POL(s(x1)) = 1   
POL(tt) = 0   
POL(zeros) = 1   

The following usable rules [17] were oriented:

active(length(x1)) → length(active(x1))
length(ok(x1)) → ok(length(x1))
proper(zeros) → ok(zeros)
proper(tt) → ok(tt)
active(and(x1, x2)) → and(active(x1), x2)
active(s(x1)) → s(active(x1))
and(mark(x1), x2) → mark(and(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
active(cons(x1, x2)) → cons(active(x1), x2)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
s(mark(x1)) → mark(s(x1))
proper(s(x1)) → s(proper(x1))
proper(0) → ok(0)
and(ok(x1), ok(x2)) → ok(and(x1, x2))
s(ok(x1)) → ok(s(x1))
active(length(cons(N, L))) → mark(s(length(L)))
proper(nil) → ok(nil)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
active(zeros) → mark(cons(0, zeros))
cons(mark(x1), x2) → mark(cons(x1, x2))
length(mark(x1)) → mark(length(x1))
proper(length(x1)) → length(proper(x1))



↳ CSR
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ QDPOrderProof
                                              ↳ QDP
                                                ↳ QDPOrderProof
                                                  ↳ QDP

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

TOP(ok(and(x0, x1))) → TOP(and(active(x0), x1))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(cons(x0, x1))) → TOP(cons(proper(x0), proper(x1)))
TOP(mark(and(x0, x1))) → TOP(and(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(cons(x0, x1))) → TOP(cons(active(x0), x1))
TOP(mark(length(x0))) → TOP(length(proper(x0)))
TOP(ok(length(x0))) → TOP(length(active(x0)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
active(cons(x1, x2)) → cons(active(x1), x2)
active(and(x1, x2)) → and(active(x1), x2)
active(length(x1)) → length(active(x1))
active(s(x1)) → s(active(x1))
s(mark(x1)) → mark(s(x1))
s(ok(x1)) → ok(s(x1))
length(mark(x1)) → mark(length(x1))
length(ok(x1)) → ok(length(x1))
and(mark(x1), x2) → mark(and(x1, x2))
and(ok(x1), ok(x2)) → ok(and(x1, x2))
cons(mark(x1), x2) → mark(cons(x1, x2))
cons(ok(x1), ok(x2)) → ok(cons(x1, x2))
proper(zeros) → ok(zeros)
proper(cons(x1, x2)) → cons(proper(x1), proper(x2))
proper(0) → ok(0)
proper(and(x1, x2)) → and(proper(x1), proper(x2))
proper(tt) → ok(tt)
proper(length(x1)) → length(proper(x1))
proper(nil) → ok(nil)
proper(s(x1)) → s(proper(x1))

The set Q consists of the following terms:

active(zeros)
proper(zeros)
active(cons(x0, x1))
cons(mark(x0), x1)
proper(cons(x0, x1))
cons(ok(x0), ok(x1))
proper(0)
active(and(x0, x1))
and(mark(x0), x1)
proper(and(x0, x1))
and(ok(x0), ok(x1))
proper(tt)
active(length(x0))
length(mark(x0))
proper(length(x0))
length(ok(x0))
proper(nil)
active(s(x0))
s(mark(x0))
proper(s(x0))
s(ok(x0))

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