NO
proof of Transformed_CSR_04_LengthOfFiniteLists_nosorts_iGM.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


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

(0) QTRS
(1) QTRSRRRProof [EQUIVALENT, 62 ms]
(2) QTRS
(3) QTRSRRRProof [EQUIVALENT, 13 ms]
(4) QTRS
(5) QTRSRRRProof [EQUIVALENT, 0 ms]
(6) QTRS
(7) QTRSRRRProof [EQUIVALENT, 17 ms]
(8) QTRS
(9) DependencyPairsProof [EQUIVALENT, 23 ms]
(10) QDP
(11) DependencyGraphProof [EQUIVALENT, 0 ms]
(12) AND
    (13) QDP
        (14) UsableRulesProof [EQUIVALENT, 0 ms]
        (15) QDP
        (16) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (17) YES
    (18) QDP
        (19) UsableRulesProof [EQUIVALENT, 0 ms]
        (20) QDP
        (21) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (22) YES
    (23) QDP
        (24) UsableRulesProof [EQUIVALENT, 0 ms]
        (25) QDP
        (26) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (27) YES
    (28) QDP
        (29) UsableRulesProof [EQUIVALENT, 0 ms]
        (30) QDP
        (31) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (32) YES
    (33) QDP
        (34) UsableRulesProof [EQUIVALENT, 0 ms]
        (35) QDP
        (36) MRRProof [EQUIVALENT, 0 ms]
        (37) QDP
        (38) QDPOrderProof [EQUIVALENT, 71 ms]
        (39) QDP
        (40) DependencyGraphProof [EQUIVALENT, 0 ms]
        (41) QDP
        (42) QDPOrderProof [EQUIVALENT, 21 ms]
        (43) QDP
        (44) QDPOrderProof [EQUIVALENT, 0 ms]
        (45) QDP
        (46) QDPOrderProof [EQUIVALENT, 0 ms]
        (47) QDP
        (48) TransformationProof [EQUIVALENT, 0 ms]
        (49) QDP
        (50) TransformationProof [EQUIVALENT, 0 ms]
        (51) QDP
        (52) DependencyGraphProof [EQUIVALENT, 0 ms]
        (53) QDP
        (54) MRRProof [EQUIVALENT, 0 ms]
        (55) QDP
        (56) QDPOrderProof [EQUIVALENT, 49 ms]
        (57) QDP
        (58) QDPOrderProof [EQUIVALENT, 26 ms]
        (59) QDP
        (60) NonTerminationLoopProof [COMPLETE, 0 ms]
        (61) NO


----------------------------------------

(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)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(active(x_1)) = x_1
   POL(and(x_1, x_2)) = x_1 + 2*x_2
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(length(x_1)) = 2*x_1
   POL(mark(x_1)) = 2*x_1
   POL(nil) = 0
   POL(s(x_1)) = x_1
   POL(tt) = 2
   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)
   mark(tt) -> active(tt)




----------------------------------------

(2)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   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(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)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(active(x_1)) = x_1
   POL(and(x_1, x_2)) = 2 + 2*x_1 + 2*x_2
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(length(x_1)) = 2*x_1
   POL(mark(x_1)) = x_1
   POL(nil) = 2
   POL(s(x_1)) = 2*x_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(length(nil)) -> mark(0)




----------------------------------------

(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(and(X1, X2)) -> active(and(mark(X1), X2))
   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.

----------------------------------------

(5) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(active(x_1)) = x_1
   POL(and(x_1, x_2)) = x_1 + 2*x_2
   POL(cons(x_1, x_2)) = 2*x_1 + 2*x_2
   POL(length(x_1)) = x_1
   POL(mark(x_1)) = 2*x_1
   POL(nil) = 2
   POL(s(x_1)) = x_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(nil) -> active(nil)




----------------------------------------

(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(and(X1, X2)) -> active(and(mark(X1), X2))
   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) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(active(x_1)) = x_1
   POL(and(x_1, x_2)) = 1 + 2*x_1 + 2*x_2
   POL(cons(x_1, x_2)) = 2*x_1 + 2*x_2
   POL(length(x_1)) = 2*x_1
   POL(mark(x_1)) = 2*x_1
   POL(s(x_1)) = x_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(and(X1, X2)) -> active(and(mark(X1), X2))




----------------------------------------

(8)
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.

----------------------------------------

(9) DependencyPairsProof (EQUIVALENT)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
----------------------------------------

(10)
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.
----------------------------------------

(11) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 7 less nodes.
----------------------------------------

(12)
Complex Obligation (AND)

----------------------------------------

(13)
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.
----------------------------------------

(14) UsableRulesProof (EQUIVALENT)
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.
----------------------------------------

(15)
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.
----------------------------------------

(16) QDPSizeChangeProof (EQUIVALENT)
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


----------------------------------------

(17)
YES

----------------------------------------

(18)
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.
----------------------------------------

(19) UsableRulesProof (EQUIVALENT)
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.
----------------------------------------

(20)
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.
----------------------------------------

(21) QDPSizeChangeProof (EQUIVALENT)
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


----------------------------------------

(22)
YES

----------------------------------------

(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)

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

(24) UsableRulesProof (EQUIVALENT)
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.
----------------------------------------

(25)
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.
----------------------------------------

(26) QDPSizeChangeProof (EQUIVALENT)
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


----------------------------------------

(27)
YES

----------------------------------------

(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)

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

(29) UsableRulesProof (EQUIVALENT)
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.
----------------------------------------

(30)
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.
----------------------------------------

(31) QDPSizeChangeProof (EQUIVALENT)
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


----------------------------------------

(32)
YES

----------------------------------------

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

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

(34) UsableRulesProof (EQUIVALENT)
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.
----------------------------------------

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

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

(36) MRRProof (EQUIVALENT)
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(x_1)) = x_1
   POL(MARK(x_1)) = x_1
   POL(active(x_1)) = x_1
   POL(cons(x_1, x_2)) = x_1 + x_2
   POL(length(x_1)) = 2 + x_1
   POL(mark(x_1)) = x_1
   POL(s(x_1)) = x_1
   POL(zeros) = 0


----------------------------------------

(37)
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(cons(X1, X2)) -> active(cons(mark(X1), X2))
   active(zeros) -> mark(cons(0, zeros))
   active(length(cons(N, L))) -> mark(s(length(L)))
   mark(zeros) -> active(zeros)
   mark(length(X)) -> active(length(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   mark(0) -> active(0)
   s(active(X)) -> s(X)
   s(mark(X)) -> s(X)
   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)
   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)
We use the reduction pair processor [LPAR04,JAR06].


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:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ACTIVE_1(x_1) ) = 1
POL( cons_2(x_1, x_2) ) = 2x_1
POL( length_1(x_1) ) = 0
POL( s_1(x_1) ) = x_1
POL( active_1(x_1) ) = x_1 + 1
POL( zeros ) = 1
POL( mark_1(x_1) ) = 2x_1
POL( 0 ) = 0
POL( MARK_1(x_1) ) = x_1 + 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

   length(mark(X)) -> length(X)
   length(active(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:

   MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2))
   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)) -> ACTIVE(s(mark(X)))
   MARK(s(X)) -> MARK(X)

The TRS R consists of the following rules:

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

   ACTIVE(length(cons(N, L))) -> MARK(s(length(L)))
   MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2))
   MARK(cons(X1, X2)) -> MARK(X1)
   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(cons(X1, X2)) -> active(cons(mark(X1), X2))
   active(zeros) -> mark(cons(0, zeros))
   active(length(cons(N, L))) -> mark(s(length(L)))
   mark(zeros) -> active(zeros)
   mark(length(X)) -> active(length(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   mark(0) -> active(0)
   s(active(X)) -> s(X)
   s(mark(X)) -> s(X)
   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)
   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)
We use the reduction pair processor [LPAR04,JAR06].


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:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ACTIVE_1(x_1) ) = x_1
POL( MARK_1(x_1) ) = x_1
POL( s_1(x_1) ) = x_1
POL( length_1(x_1) ) = 0
POL( mark_1(x_1) ) = x_1
POL( active_1(x_1) ) = x_1
POL( cons_2(x_1, x_2) ) = 2x_1 + 2
POL( zeros ) = 2
POL( 0 ) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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


----------------------------------------

(43)
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)) -> ACTIVE(cons(mark(X1), X2))
   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(cons(X1, X2)) -> active(cons(mark(X1), X2))
   active(zeros) -> mark(cons(0, zeros))
   active(length(cons(N, L))) -> mark(s(length(L)))
   mark(zeros) -> active(zeros)
   mark(length(X)) -> active(length(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   mark(0) -> active(0)
   s(active(X)) -> s(X)
   s(mark(X)) -> s(X)
   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)
   length(active(X)) -> length(X)
   length(mark(X)) -> length(X)

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

(44) QDPOrderProof (EQUIVALENT)
We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.

   MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2))
The remaining pairs can at least be oriented weakly.
Used ordering:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ACTIVE_1(x_1) ) = x_1
POL( MARK_1(x_1) ) = 2x_1
POL( s_1(x_1) ) = 2x_1
POL( length_1(x_1) ) = 0
POL( mark_1(x_1) ) = x_1
POL( active_1(x_1) ) = x_1
POL( cons_2(x_1, x_2) ) = 1
POL( zeros ) = 1
POL( 0 ) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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


----------------------------------------

(45)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   ACTIVE(length(cons(N, L))) -> MARK(s(length(L)))
   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(cons(X1, X2)) -> active(cons(mark(X1), X2))
   active(zeros) -> mark(cons(0, zeros))
   active(length(cons(N, L))) -> mark(s(length(L)))
   mark(zeros) -> active(zeros)
   mark(length(X)) -> active(length(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   mark(0) -> active(0)
   s(active(X)) -> s(X)
   s(mark(X)) -> s(X)
   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)
   length(active(X)) -> length(X)
   length(mark(X)) -> length(X)

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

(46) QDPOrderProof (EQUIVALENT)
We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.

   MARK(s(X)) -> ACTIVE(s(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ACTIVE_1(x_1) ) = x_1 + 1
POL( MARK_1(x_1) ) = 2
POL( s_1(x_1) ) = max{0, -2}
POL( length_1(x_1) ) = 1
POL( mark_1(x_1) ) = x_1 + 2
POL( active_1(x_1) ) = 2x_1 + 2
POL( zeros ) = 2
POL( cons_2(x_1, x_2) ) = 2x_1 + x_2 + 2
POL( 0 ) = 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

   length(mark(X)) -> length(X)
   length(active(X)) -> length(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)


----------------------------------------

(47)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

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

(48) TransformationProof (EQUIVALENT)
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(x0)) -> ACTIVE(length(x0)))
   (MARK(length(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1)))),MARK(length(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1)))))
   (MARK(length(zeros)) -> ACTIVE(length(active(zeros))),MARK(length(zeros)) -> ACTIVE(length(active(zeros))))
   (MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))),MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))))
   (MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))),MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))))
   (MARK(length(0)) -> ACTIVE(length(active(0))),MARK(length(0)) -> ACTIVE(length(active(0))))


----------------------------------------

(49)
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(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1))))
   MARK(length(zeros)) -> ACTIVE(length(active(zeros)))
   MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0)))))
   MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0)))))
   MARK(length(0)) -> ACTIVE(length(active(0)))

The TRS R consists of the following rules:

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

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

(50) TransformationProof (EQUIVALENT)
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)),MARK(length(0)) -> ACTIVE(length(0)))


----------------------------------------

(51)
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(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1))))
   MARK(length(zeros)) -> ACTIVE(length(active(zeros)))
   MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0)))))
   MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0)))))
   MARK(length(0)) -> ACTIVE(length(0))

The TRS R consists of the following rules:

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

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

(52) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
----------------------------------------

(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(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1))))
   MARK(length(zeros)) -> ACTIVE(length(active(zeros)))
   MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0)))))
   MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0)))))

The TRS R consists of the following rules:

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

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

(54) MRRProof (EQUIVALENT)
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(x_1)) = 2 + x_1
   POL(MARK(x_1)) = 1 + 2*x_1
   POL(active(x_1)) = x_1
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(length(x_1)) = 1 + x_1
   POL(mark(x_1)) = x_1
   POL(s(x_1)) = x_1
   POL(zeros) = 0


----------------------------------------

(55)
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(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1))))
   MARK(length(zeros)) -> ACTIVE(length(active(zeros)))
   MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0)))))

The TRS R consists of the following rules:

   mark(cons(X1, X2)) -> active(cons(mark(X1), X2))
   active(zeros) -> mark(cons(0, zeros))
   active(length(cons(N, L))) -> mark(s(length(L)))
   mark(zeros) -> active(zeros)
   mark(length(X)) -> active(length(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   mark(0) -> active(0)
   s(active(X)) -> s(X)
   s(mark(X)) -> s(X)
   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)
   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)
We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.

   MARK(length(x0)) -> ACTIVE(length(x0))
   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(x_1)) =  	[[3A]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 POL(s(x_1)) =  	[[2A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(length(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(ACTIVE(x_1)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(active(x_1)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(mark(x_1)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(zeros) =  	[[2A]]
>>>

   <<<
 POL(0) =  	[[3A]]
>>>


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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


----------------------------------------

(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)))
   MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0)))))

The TRS R consists of the following rules:

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

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

(58) QDPOrderProof (EQUIVALENT)
We use the reduction pair processor [LPAR04,JAR06].


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:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ACTIVE_1(x_1) ) = max{0, x_1 - 2}
POL( MARK_1(x_1) ) = 2
POL( s_1(x_1) ) = max{0, -2}
POL( length_1(x_1) ) = 2x_1 + 2
POL( mark_1(x_1) ) = x_1
POL( active_1(x_1) ) = x_1
POL( zeros ) = 1
POL( cons_2(x_1, x_2) ) = 1
POL( 0 ) = 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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


----------------------------------------

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

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

(60) NonTerminationLoopProof (COMPLETE)
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:
* Matcher: [ ]
* Semiunifier: [ ]

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




----------------------------------------

(61)
NO