NO proof of Transformed_CSR_04_OvConsOS_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, 69 ms] (2) QTRS (3) DependencyPairsProof [EQUIVALENT, 0 ms] (4) QDP (5) DependencyGraphProof [EQUIVALENT, 0 ms] (6) AND (7) QDP (8) UsableRulesProof [EQUIVALENT, 0 ms] (9) QDP (10) QDPSizeChangeProof [EQUIVALENT, 0 ms] (11) YES (12) QDP (13) UsableRulesProof [EQUIVALENT, 0 ms] (14) QDP (15) QDPSizeChangeProof [EQUIVALENT, 0 ms] (16) YES (17) QDP (18) UsableRulesProof [EQUIVALENT, 0 ms] (19) QDP (20) QDPSizeChangeProof [EQUIVALENT, 0 ms] (21) YES (22) QDP (23) UsableRulesProof [EQUIVALENT, 0 ms] (24) QDP (25) QDPSizeChangeProof [EQUIVALENT, 0 ms] (26) YES (27) QDP (28) UsableRulesProof [EQUIVALENT, 0 ms] (29) QDP (30) QDPSizeChangeProof [EQUIVALENT, 0 ms] (31) YES (32) QDP (33) MRRProof [EQUIVALENT, 24 ms] (34) QDP (35) MRRProof [EQUIVALENT, 0 ms] (36) QDP (37) QDPOrderProof [EQUIVALENT, 37 ms] (38) QDP (39) DependencyGraphProof [EQUIVALENT, 0 ms] (40) QDP (41) QDPOrderProof [EQUIVALENT, 5 ms] (42) QDP (43) QDPOrderProof [EQUIVALENT, 88 ms] (44) QDP (45) QDPOrderProof [EQUIVALENT, 35 ms] (46) QDP (47) QDPOrderProof [EQUIVALENT, 45 ms] (48) QDP (49) TransformationProof [EQUIVALENT, 0 ms] (50) QDP (51) TransformationProof [EQUIVALENT, 0 ms] (52) QDP (53) DependencyGraphProof [EQUIVALENT, 0 ms] (54) QDP (55) TransformationProof [EQUIVALENT, 0 ms] (56) QDP (57) DependencyGraphProof [EQUIVALENT, 0 ms] (58) QDP (59) TransformationProof [EQUIVALENT, 0 ms] (60) QDP (61) DependencyGraphProof [EQUIVALENT, 0 ms] (62) QDP (63) QDPOrderProof [EQUIVALENT, 64 ms] (64) QDP (65) QDPOrderProof [EQUIVALENT, 100 ms] (66) QDP (67) QDPOrderProof [EQUIVALENT, 140 ms] (68) QDP (69) QDPOrderProof [EQUIVALENT, 133 ms] (70) QDP (71) QDPOrderProof [EQUIVALENT, 202 ms] (72) QDP (73) NonTerminationLoopProof [COMPLETE, 74 ms] (74) 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))) active(take(0, IL)) -> mark(nil) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) 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)) = 2*x_1 + 2*x_2 POL(cons(x_1, x_2)) = x_1 + x_2 POL(length(x_1)) = 2 + x_1 POL(mark(x_1)) = x_1 POL(nil) = 1 POL(s(x_1)) = x_1 POL(take(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 POL(tt) = 2 POL(zeros) = 1 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) active(take(0, IL)) -> mark(nil) ---------------------------------------- (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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. ---------------------------------------- (3) DependencyPairsProof (EQUIVALENT) Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem. ---------------------------------------- (4) 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) ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) ACTIVE(take(s(M), cons(N, IL))) -> CONS(N, take(M, IL)) ACTIVE(take(s(M), cons(N, IL))) -> TAKE(M, IL) 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(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) MARK(and(X1, X2)) -> AND(mark(X1), X2) MARK(and(X1, X2)) -> MARK(X1) MARK(tt) -> ACTIVE(tt) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(length(X)) -> LENGTH(mark(X)) MARK(length(X)) -> MARK(X) MARK(nil) -> ACTIVE(nil) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> S(mark(X)) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) MARK(take(X1, X2)) -> TAKE(mark(X1), mark(X2)) MARK(take(X1, X2)) -> MARK(X1) MARK(take(X1, X2)) -> MARK(X2) 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) TAKE(mark(X1), X2) -> TAKE(X1, X2) TAKE(X1, mark(X2)) -> TAKE(X1, X2) TAKE(active(X1), X2) -> TAKE(X1, X2) TAKE(X1, active(X2)) -> TAKE(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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (5) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 13 less nodes. ---------------------------------------- (6) Complex Obligation (AND) ---------------------------------------- (7) Obligation: Q DP problem: The TRS P consists of the following rules: TAKE(X1, mark(X2)) -> TAKE(X1, X2) TAKE(mark(X1), X2) -> TAKE(X1, X2) TAKE(active(X1), X2) -> TAKE(X1, X2) TAKE(X1, active(X2)) -> TAKE(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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (8) 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. ---------------------------------------- (9) Obligation: Q DP problem: The TRS P consists of the following rules: TAKE(X1, mark(X2)) -> TAKE(X1, X2) TAKE(mark(X1), X2) -> TAKE(X1, X2) TAKE(active(X1), X2) -> TAKE(X1, X2) TAKE(X1, active(X2)) -> TAKE(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (10) 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: *TAKE(X1, mark(X2)) -> TAKE(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *TAKE(mark(X1), X2) -> TAKE(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *TAKE(active(X1), X2) -> TAKE(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *TAKE(X1, active(X2)) -> TAKE(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (11) YES ---------------------------------------- (12) 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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (13) 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. ---------------------------------------- (14) 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. ---------------------------------------- (15) 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 ---------------------------------------- (16) YES ---------------------------------------- (17) 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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (18) 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. ---------------------------------------- (19) 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. ---------------------------------------- (20) 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 ---------------------------------------- (21) YES ---------------------------------------- (22) 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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (23) 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. ---------------------------------------- (24) 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. ---------------------------------------- (25) 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 ---------------------------------------- (26) YES ---------------------------------------- (27) 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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (28) 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. ---------------------------------------- (29) 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. ---------------------------------------- (30) 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 ---------------------------------------- (31) YES ---------------------------------------- (32) 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(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) MARK(and(X1, X2)) -> MARK(X1) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(length(X)) -> MARK(X) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) MARK(take(X1, X2)) -> MARK(X1) MARK(take(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (33) 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(take(X1, X2)) -> MARK(X1) MARK(take(X1, X2)) -> MARK(X2) Used ordering: Polynomial interpretation [POLO]: POL(0) = 0 POL(ACTIVE(x_1)) = 1 + x_1 POL(MARK(x_1)) = 1 + x_1 POL(active(x_1)) = x_1 POL(and(x_1, x_2)) = 2*x_1 + 2*x_2 POL(cons(x_1, x_2)) = 2*x_1 + x_2 POL(length(x_1)) = 2*x_1 POL(mark(x_1)) = x_1 POL(nil) = 1 POL(s(x_1)) = x_1 POL(take(x_1, x_2)) = 1 + x_1 + x_2 POL(tt) = 1 POL(zeros) = 0 ---------------------------------------- (34) 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(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) MARK(and(X1, X2)) -> MARK(X1) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(length(X)) -> MARK(X) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (35) 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(and(X1, X2)) -> MARK(X1) MARK(length(X)) -> MARK(X) Used ordering: Polynomial interpretation [POLO]: POL(0) = 0 POL(ACTIVE(x_1)) = 2 + x_1 POL(MARK(x_1)) = 2 + x_1 POL(active(x_1)) = x_1 POL(and(x_1, x_2)) = 2 + 2*x_1 + x_2 POL(cons(x_1, x_2)) = 2*x_1 + x_2 POL(length(x_1)) = 1 + 2*x_1 POL(mark(x_1)) = x_1 POL(nil) = 1 POL(s(x_1)) = x_1 POL(take(x_1, x_2)) = 2 + 2*x_1 + x_2 POL(tt) = 2 POL(zeros) = 0 ---------------------------------------- (36) 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(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (37) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVE(zeros) -> MARK(cons(0, zeros)) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. MARK(x1) = x1 cons(x1, x2) = x1 ACTIVE(x1) = x1 mark(x1) = x1 length(x1) = length s(x1) = x1 zeros = zeros 0 = 0 and(x1, x2) = and take(x1, x2) = x2 active(x1) = x1 tt = tt nil = nil Knuth-Bendix order [KBO] with precedence:trivial and weight map: 0=2 length=1 and=2 tt=2 zeros=3 nil=2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) ---------------------------------------- (38) 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) MARK(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (39) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (40) 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)) ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) MARK(cons(X1, X2)) -> MARK(X1) MARK(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (41) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVE(take(s(M), cons(N, IL))) -> MARK(cons(N, take(M, IL))) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. ACTIVE(x1) = x1 length(x1) = length MARK(x1) = x1 s(x1) = x1 cons(x1, x2) = x1 mark(x1) = x1 take(x1, x2) = take(x2) and(x1, x2) = and active(x1) = x1 zeros = zeros 0 = 0 tt = tt nil = nil Knuth-Bendix order [KBO] with precedence:trivial and weight map: length=1 take_1=1 zeros=3 0=2 and=2 tt=2 nil=2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) 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) ---------------------------------------- (42) 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(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) MARK(length(X)) -> ACTIVE(length(mark(X))) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> MARK(X) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (43) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(and(X1, X2)) -> ACTIVE(and(mark(X1), X2)) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(take(X1, X2)) -> ACTIVE(take(mark(X1), mark(X2))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( ACTIVE_1(x_1) ) = max{0, 2x_1 - 2} POL( MARK_1(x_1) ) = 2 POL( s_1(x_1) ) = max{0, -2} POL( length_1(x_1) ) = 2 POL( active_1(x_1) ) = 2 POL( mark_1(x_1) ) = x_1 + 2 POL( and_2(x_1, x_2) ) = max{0, -2} POL( cons_2(x_1, x_2) ) = 2 POL( take_2(x_1, x_2) ) = 0 POL( zeros ) = 0 POL( 0 ) = 2 POL( tt ) = 2 POL( nil ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) 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) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) ---------------------------------------- (44) 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)) -> 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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (45) 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: Combined order from the following AFS and order. ACTIVE(x1) = x1 length(x1) = length MARK(x1) = x1 s(x1) = x1 cons(x1, x2) = cons(x1) mark(x1) = x1 active(x1) = x1 zeros = zeros 0 = 0 and(x1, x2) = and take(x1, x2) = x2 tt = tt nil = nil Knuth-Bendix order [KBO] with precedence:trivial and weight map: length=1 zeros=4 0=2 cons_1=1 and=2 tt=2 nil=2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) ---------------------------------------- (46) 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)) -> 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))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (47) 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) ) = max{0, x_1 - 2} POL( MARK_1(x_1) ) = x_1 POL( s_1(x_1) ) = x_1 POL( length_1(x_1) ) = 0 POL( active_1(x_1) ) = x_1 POL( mark_1(x_1) ) = x_1 POL( cons_2(x_1, x_2) ) = x_1 + 2 POL( zeros ) = 2 POL( 0 ) = 0 POL( and_2(x_1, x_2) ) = 2x_2 POL( take_2(x_1, x_2) ) = 2x_1 + x_2 POL( tt ) = 1 POL( nil ) = 0 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) ---------------------------------------- (48) 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: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (49) 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(zeros)) -> ACTIVE(length(active(zeros))),MARK(length(zeros)) -> ACTIVE(length(active(zeros)))) (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(0)) -> ACTIVE(length(active(0))),MARK(length(0)) -> ACTIVE(length(active(0)))) (MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))),MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1))))) (MARK(length(tt)) -> ACTIVE(length(active(tt))),MARK(length(tt)) -> ACTIVE(length(active(tt)))) (MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))),MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0)))))) (MARK(length(nil)) -> ACTIVE(length(active(nil))),MARK(length(nil)) -> ACTIVE(length(active(nil)))) (MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))),MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0)))))) (MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))),MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1)))))) ---------------------------------------- (50) 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(zeros)) -> ACTIVE(length(active(zeros))) MARK(length(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1)))) MARK(length(0)) -> ACTIVE(length(active(0))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(tt)) -> ACTIVE(length(active(tt))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(nil)) -> ACTIVE(length(active(nil))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (51) 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))) ---------------------------------------- (52) 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(zeros)) -> ACTIVE(length(active(zeros))) MARK(length(cons(x0, x1))) -> ACTIVE(length(active(cons(mark(x0), x1)))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(tt)) -> ACTIVE(length(active(tt))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(nil)) -> ACTIVE(length(active(nil))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) MARK(length(0)) -> ACTIVE(length(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(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (53) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (54) 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)))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(tt)) -> ACTIVE(length(active(tt))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(nil)) -> ACTIVE(length(active(nil))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (55) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule MARK(length(tt)) -> ACTIVE(length(active(tt))) at position [0] we obtained the following new rules [LPAR04]: (MARK(length(tt)) -> ACTIVE(length(tt)),MARK(length(tt)) -> ACTIVE(length(tt))) ---------------------------------------- (56) 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)))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(nil)) -> ACTIVE(length(active(nil))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) MARK(length(tt)) -> ACTIVE(length(tt)) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (57) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (58) 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)))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(nil)) -> ACTIVE(length(active(nil))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (59) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule MARK(length(nil)) -> ACTIVE(length(active(nil))) at position [0] we obtained the following new rules [LPAR04]: (MARK(length(nil)) -> ACTIVE(length(nil)),MARK(length(nil)) -> ACTIVE(length(nil))) ---------------------------------------- (60) 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)))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) MARK(length(nil)) -> ACTIVE(length(nil)) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (61) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (62) 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)))) MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), x1)))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (63) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(length(and(x0, x1))) -> ACTIVE(length(active(and(mark(x0), 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 + 1 POL( MARK_1(x_1) ) = 2x_1 + 1 POL( s_1(x_1) ) = x_1 POL( length_1(x_1) ) = 2x_1 POL( active_1(x_1) ) = x_1 POL( mark_1(x_1) ) = x_1 POL( cons_2(x_1, x_2) ) = 2x_2 POL( zeros ) = 0 POL( 0 ) = 2 POL( and_2(x_1, x_2) ) = 1 POL( take_2(x_1, x_2) ) = max{0, -2} POL( tt ) = 0 POL( nil ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) ---------------------------------------- (64) 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)))) MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (65) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(length(length(x0))) -> ACTIVE(length(active(length(mark(x0))))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( ACTIVE_1(x_1) ) = x_1 + 2 POL( MARK_1(x_1) ) = 2x_1 POL( s_1(x_1) ) = x_1 POL( length_1(x_1) ) = x_1 + 2 POL( active_1(x_1) ) = x_1 POL( mark_1(x_1) ) = x_1 POL( cons_2(x_1, x_2) ) = 2x_2 POL( zeros ) = 0 POL( 0 ) = 1 POL( and_2(x_1, x_2) ) = x_1 + 2x_2 POL( take_2(x_1, x_2) ) = 0 POL( tt ) = 2 POL( nil ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) 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) ---------------------------------------- (66) 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)))) MARK(length(s(x0))) -> ACTIVE(length(active(s(mark(x0))))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (67) 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: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[3A]] + [[1A]] * x_1 >>> <<< POL(s(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(length(x_1)) = [[2A]] + [[1A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[1A]] + [[-I]] * x_1 + [[1A]] * x_2 >>> <<< POL(zeros) = [[0A]] >>> <<< POL(active(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(take(x_1, x_2)) = [[0A]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[5A]] >>> <<< POL(and(x_1, x_2)) = [[2A]] + [[-I]] * x_1 + [[-I]] * x_2 >>> <<< POL(tt) = [[0A]] >>> <<< POL(nil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) 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) ---------------------------------------- (68) 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)))) MARK(length(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (69) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. 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(x_1)) = [[-I]] + [[2A]] * x_1 >>> <<< POL(s(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(length(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[1A]] + [[-I]] * x_1 + [[2A]] * x_2 >>> <<< POL(zeros) = [[0A]] >>> <<< POL(active(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(take(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[3A]] >>> <<< POL(and(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[5A]] * x_2 >>> <<< POL(tt) = [[3A]] >>> <<< POL(nil) = [[3A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) 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) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) 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) ---------------------------------------- (70) 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(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (71) 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)) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[4A]] + [[4A]] * x_1 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(length(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[3A]] + [[3A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[2A]] + [[-I]] * x_1 + [[1A]] * x_2 >>> <<< POL(zeros) = [[1A]] >>> <<< POL(active(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(take(x_1, x_2)) = [[1A]] + [[-I]] * x_1 + [[-I]] * x_2 >>> <<< POL(mark(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(0) = [[5A]] >>> <<< POL(and(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[1A]] * x_2 >>> <<< POL(tt) = [[5A]] >>> <<< POL(nil) = [[5A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: length(active(X)) -> length(X) length(mark(X)) -> length(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 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(and(X1, X2)) -> active(and(mark(X1), X2)) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) mark(length(X)) -> active(length(mark(X))) mark(s(X)) -> active(s(mark(X))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(0) -> active(0) mark(tt) -> active(tt) mark(nil) -> active(nil) take(X1, mark(X2)) -> take(X1, X2) take(mark(X1), X2) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) 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) 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) ---------------------------------------- (72) 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(take(x0, x1))) -> ACTIVE(length(active(take(mark(x0), mark(x1))))) The TRS R consists of the following rules: active(zeros) -> mark(cons(0, zeros)) active(length(cons(N, L))) -> mark(s(length(L))) active(take(s(M), cons(N, IL))) -> mark(cons(N, take(M, IL))) 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))) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) 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) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (73) 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. ---------------------------------------- (74) NO