Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 QTRSRRRProof (⇔)
↳2 QTRS
↳3 QTRSRRRProof (⇔)
↳4 QTRS
↳5 QTRSRRRProof (⇔)
↳6 QTRS
↳7 DependencyPairsProof (⇔)
↳8 QDP
↳9 DependencyGraphProof (⇔)
↳10 AND
  ↳11 QDP
    ↳12 UsableRulesProof (⇔)
    ↳13 QDP
    ↳14 QDPSizeChangeProof (⇔)
    ↳15 TRUE
  ↳16 QDP
    ↳17 UsableRulesProof (⇔)
    ↳18 QDP
    ↳19 QDPSizeChangeProof (⇔)
    ↳20 TRUE
  ↳21 QDP
    ↳22 UsableRulesProof (⇔)
    ↳23 QDP
    ↳24 QDPSizeChangeProof (⇔)
    ↳25 TRUE
  ↳26 QDP
    ↳27 UsableRulesProof (⇔)
    ↳28 QDP
    ↳29 QDPSizeChangeProof (⇔)
    ↳30 TRUE
  ↳31 QDP
    ↳32 UsableRulesProof (⇔)
    ↳33 QDP
    ↳34 MRRProof (⇔)
    ↳35 QDP
    ↳36 QDPOrderProof (⇔)
    ↳37 QDP
    ↳38 QDPOrderProof (⇔)
    ↳39 QDP
    ↳40 DependencyGraphProof (⇔)
    ↳41 QDP
    ↳42 QDPOrderProof (⇔)
    ↳43 QDP
    ↳44 Narrowing (⇔)
    ↳45 QDP
    ↳46 Narrowing (⇔)
    ↳47 QDP
    ↳48 DependencyGraphProof (⇔)
    ↳49 QDP
    ↳50 MRRProof (⇔)
    ↳51 QDP
    ↳52 QDPOrderProof (⇔)
    ↳53 QDP
    ↳54 QDPOrderProof (⇔)
    ↳55 QDP
    ↳56 QDPOrderProof (⇔)
    ↳57 QDP
    ↳58 NonTerminationProof (⇔)
    ↳59 FALSE

(0) Obligation:

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)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(and(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = x1 + x2   
POL(length(x1)) = 1 + x1   
POL(mark(x1)) = x1   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 1   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

active(and(tt, X)) → mark(X)
active(length(nil)) → mark(0)


(2) Obligation:

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)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(nil) → active(nil)
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 2 + 2·x1 + x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = 2·x1   
POL(mark(x1)) = 2·x1   
POL(nil) = 2   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(nil) → active(nil)


(4) Obligation:

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)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(tt) → active(tt)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 2·x1 + x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(length(x1)) = x1   
POL(mark(x1)) = 2·x1   
POL(s(x1)) = x1   
POL(tt) = 1   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

mark(tt) → active(tt)


(6) Obligation:

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)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

Q is empty.

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(8) Obligation:

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

ACTIVE(zeros) → MARK(cons(0, zeros))
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → S(length(L))
ACTIVE(length(cons(N, L))) → LENGTH(L)
MARK(zeros) → ACTIVE(zeros)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(0) → ACTIVE(0)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → LENGTH(mark(X))
MARK(length(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(X1, mark(X2)) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
LENGTH(mark(X)) → LENGTH(X)
LENGTH(active(X)) → LENGTH(X)
S(mark(X)) → S(X)
S(active(X)) → S(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 7 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

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

S(active(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

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

(12) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

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

S(active(X)) → S(X)
S(mark(X)) → S(X)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • S(active(X)) → S(X)
    The graph contains the following edges 1 > 1

  • S(mark(X)) → S(X)
    The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

LENGTH(active(X)) → LENGTH(X)
LENGTH(mark(X)) → LENGTH(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

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

(17) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(18) Obligation:

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

LENGTH(active(X)) → LENGTH(X)
LENGTH(mark(X)) → LENGTH(X)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • LENGTH(active(X)) → LENGTH(X)
    The graph contains the following edges 1 > 1

  • LENGTH(mark(X)) → LENGTH(X)
    The graph contains the following edges 1 > 1

(20) TRUE

(21) Obligation:

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

AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(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)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

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

(22) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

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

AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)

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

(24) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • AND(X1, mark(X2)) → AND(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • AND(mark(X1), X2) → AND(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • AND(active(X1), X2) → AND(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • AND(X1, active(X2)) → AND(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(25) TRUE

(26) Obligation:

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

CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(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)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

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

(27) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(28) Obligation:

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

CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)

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

(29) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • CONS(X1, mark(X2)) → CONS(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • CONS(mark(X1), X2) → CONS(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CONS(active(X1), X2) → CONS(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CONS(X1, active(X2)) → CONS(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(30) TRUE

(31) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(length(X)) → active(length(mark(X)))
mark(s(X)) → active(s(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
length(mark(X)) → length(X)
length(active(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

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

(32) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(33) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(34) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MARK(length(X)) → MARK(X)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVE(x1)) = x1   
POL(MARK(x1)) = x1   
POL(active(x1)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(length(x1)) = 1 + x1   
POL(mark(x1)) = x1   
POL(s(x1)) = x1   
POL(zeros) = 0   

(35) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(36) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(MARK(x1)) =
/1\
\0/
 +
/00\
\00/
·x1

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(ACTIVE(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(mark(x1)) =
/0\
\1/
 +
/00\
\01/
·x1

POL(length(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(s(x1)) =
/1\
\0/
 +
/01\
\00/
·x1

POL(zeros) =
/0\
\1/

POL(0) =
/0\
\0/

POL(active(x1)) =
/0\
\1/
 +
/00\
\01/
·x1

The following usable rules [FROCOS05] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
mark(s(X)) → active(s(mark(X)))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
mark(0) → active(0)
s(mark(X)) → s(X)
s(active(X)) → s(X)

(37) Obligation:

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

ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(zeros) → ACTIVE(zeros)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(ACTIVE(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(length(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(cons(x1, x2)) =
/0\
\0/
 +
/01\
\10/
·x1 +
/00\
\00/
·x2

POL(MARK(x1)) =
/0\
\0/
 +
/11\
\11/
·x1

POL(s(x1)) =
/0\
\0/
 +
/11\
\11/
·x1

POL(zeros) =
/1\
\1/

POL(0) =
/0\
\0/

POL(mark(x1)) =
/0\
\0/
 +
/11\
\00/
·x1

POL(active(x1)) =
/1\
\0/
 +
/11\
\00/
·x1

The following usable rules [FROCOS05] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

(39) Obligation:

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

ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(40) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(41) Obligation:

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

MARK(cons(X1, X2)) → MARK(X1)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(MARK(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(cons(x1, x2)) =
/0\
\1/
 +
/00\
\01/
·x1 +
/11\
\00/
·x2

POL(length(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(ACTIVE(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(mark(x1)) =
/1\
\0/
 +
/11\
\00/
·x1

POL(s(x1)) =
/0\
\0/
 +
/00\
\11/
·x1

POL(active(x1)) =
/0\
\1/
 +
/01\
\10/
·x1

POL(zeros) =
/1\
\1/

POL(0) =
/0\
\1/

The following usable rules [FROCOS05] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)

(43) Obligation:

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

MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(44) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(length(X)) → ACTIVE(length(mark(X))) at position [0] we obtained the following new rules [LPAR04]:

MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(active(0)))

(45) Obligation:

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

ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(active(0)))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(46) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(length(0)) → ACTIVE(length(active(0))) at position [0] we obtained the following new rules [LPAR04]:

MARK(length(0)) → ACTIVE(length(0))

(47) Obligation:

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

ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(0))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(48) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(49) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(50) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVE(x1)) = 1 + x1   
POL(MARK(x1)) = 2·x1   
POL(active(x1)) = x1   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(length(x1)) = 1 + x1   
POL(mark(x1)) = x1   
POL(s(x1)) = x1   
POL(zeros) = 0   

(51) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(MARK(x1)) =
/1\
\0/
 +
/10\
\00/
·x1

POL(s(x1)) =
/0\
\1/
 +
/10\
\00/
·x1

POL(length(x1)) =
/0\
\1/
 +
/11\
\10/
·x1

POL(ACTIVE(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\00/
·x2

POL(active(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(mark(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(zeros) =
/0\
\0/

POL(0) =
/0\
\0/

The following usable rules [FROCOS05] were oriented:

mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
mark(s(X)) → active(s(mark(X)))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
length(active(X)) → length(X)
length(mark(X)) → length(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
mark(0) → active(0)
s(mark(X)) → s(X)
s(active(X)) → s(X)

(53) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(length(x0)) → ACTIVE(length(x0))
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(length(x0)) → ACTIVE(length(x0))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = -I + 1A·x1

POL(s(x1)) = -I + 0A·x1

POL(length(x1)) = -I + 0A·x1

POL(ACTIVE(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 0A + -I·x1 + 1A·x2

POL(zeros) = 0A

POL(active(x1)) = 1A + 0A·x1

POL(mark(x1)) = 1A + 0A·x1

POL(0) = 0A

The following usable rules [FROCOS05] were oriented:

mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
mark(s(X)) → active(s(mark(X)))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
length(active(X)) → length(X)
length(mark(X)) → length(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
mark(0) → active(0)
s(mark(X)) → s(X)
s(active(X)) → s(X)

(55) Obligation:

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

MARK(s(X)) → MARK(X)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(56) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = -I + 1A·x1

POL(s(x1)) = -I + 0A·x1

POL(ACTIVE(x1)) = -I + 0A·x1

POL(length(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 1A + -I·x1 + 1A·x2

POL(zeros) = 0A

POL(active(x1)) = 1A + 0A·x1

POL(mark(x1)) = 1A + 0A·x1

POL(0) = 0A

The following usable rules [FROCOS05] were oriented:

mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
mark(s(X)) → active(s(mark(X)))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
length(active(X)) → length(X)
length(mark(X)) → length(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
mark(0) → active(0)
s(mark(X)) → s(X)
s(active(X)) → s(X)

(57) Obligation:

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

MARK(s(X)) → MARK(X)
ACTIVE(length(cons(N, L))) → MARK(s(length(L)))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))

The TRS R consists of the following rules:

mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
active(zeros) → mark(cons(0, zeros))
active(length(cons(N, L))) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)

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

(58) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = MARK(length(zeros)) evaluates to t =MARK(length(zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

MARK(length(zeros)) → ACTIVE(length(active(zeros)))
with rule MARK(length(zeros)) → ACTIVE(length(active(zeros))) at position [] and matcher [ ]

ACTIVE(length(active(zeros))) → ACTIVE(length(mark(cons(0, zeros))))
with rule active(zeros) → mark(cons(0, zeros)) at position [0,0] and matcher [ ]

ACTIVE(length(mark(cons(0, zeros)))) → ACTIVE(length(cons(0, zeros)))
with rule length(mark(X)) → length(X) at position [0] and matcher [X / cons(0, zeros)]

ACTIVE(length(cons(0, zeros))) → MARK(s(length(zeros)))
with rule ACTIVE(length(cons(N, L))) → MARK(s(length(L))) at position [] and matcher [N / 0, L / zeros]

MARK(s(length(zeros))) → MARK(length(zeros))
with rule MARK(s(X)) → MARK(X)

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


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



(59) FALSE