WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 375 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 69 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 34 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 26 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 25 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 22 ms] (20) CdtProblem (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 241 ms] (22) CdtProblem (23) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (24) BOUNDS(1, 1) (25) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CpxRelTRS (27) SlicingProof [LOWER BOUND(ID), 0 ms] (28) CpxRelTRS (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (30) typed CpxTrs (31) OrderProof [LOWER BOUND(ID), 0 ms] (32) typed CpxTrs (33) RewriteLemmaProof [LOWER BOUND(ID), 95.6 s] (34) BEST (35) proven lower bound (36) LowerBoundPropagationProof [FINISHED, 0 ms] (37) BOUNDS(n^1, INF) (38) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), y, ys, x, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0, S(y)) -> False !EQ(S(x), 0) -> False !EQ(0, 0) -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, y, ys, x, xs) -> False eqNatList[Ite](True, y, ys, x, xs) -> eqNatList(xs, ys) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), y, ys, x, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0, S(y)) -> False !EQ(S(x), 0) -> False !EQ(0, 0) -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, y, ys, x, xs) -> False eqNatList[Ite](True, y, ys, x, xs) -> eqNatList(xs, ys) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil))) domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))) eqNatList[Ite](False, z0, z1, z2, z3) -> False eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1) prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Cons(z0, z1), Nil) -> False prefix(Nil, z0) -> True domatch(Cons(z0, z1), Nil, z2) -> Nil domatch(Nil, Nil, z0) -> Cons(z0, Nil) domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3) eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1) eqNatList(Cons(z0, z1), Nil) -> False eqNatList(Nil, Cons(z0, z1)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False strmatch(z0, z1) -> domatch(z0, z1, Nil) Tuples: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) !EQ'(0, S(z0)) -> c5 !EQ'(S(z0), 0) -> c6 !EQ'(0, 0) -> c7 DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](False, z0, z1, z2, z3) -> c10 EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3)) PREFIX(Cons(z0, z1), Nil) -> c13 PREFIX(Nil, z0) -> c14 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 NOTEMPTY(Cons(z0, z1)) -> c22 NOTEMPTY(Nil) -> c23 STRMATCH(z0, z1) -> c24(DOMATCH(z0, z1, Nil)) S tuples: PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3)) PREFIX(Cons(z0, z1), Nil) -> c13 PREFIX(Nil, z0) -> c14 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 NOTEMPTY(Cons(z0, z1)) -> c22 NOTEMPTY(Nil) -> c23 STRMATCH(z0, z1) -> c24(DOMATCH(z0, z1, Nil)) K tuples:none Defined Rule Symbols: prefix_2, domatch_3, eqNatList_2, notEmpty_1, strmatch_2, and_2, !EQ_2, domatch[Ite]_4, eqNatList[Ite]_5 Defined Pair Symbols: AND_2, !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, PREFIX_2, DOMATCH_3, EQNATLIST_2, NOTEMPTY_1, STRMATCH_2 Compound Symbols: c, c1, c2, c3, c4_1, c5, c6, c7, c8_1, c9_1, c10, c11_1, c12_3, c13, c14, c15, c16, c17_2, c18_2, c19, c20, c21, c22, c23, c24_1 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: STRMATCH(z0, z1) -> c24(DOMATCH(z0, z1, Nil)) Removed 12 trailing nodes: !EQ'(0, 0) -> c7 !EQ'(0, S(z0)) -> c5 AND(False, True) -> c2 AND(True, False) -> c1 PREFIX(Cons(z0, z1), Nil) -> c13 !EQ'(S(z0), 0) -> c6 NOTEMPTY(Cons(z0, z1)) -> c22 AND(True, True) -> c3 NOTEMPTY(Nil) -> c23 PREFIX(Nil, z0) -> c14 EQNATLIST[ITE](False, z0, z1, z2, z3) -> c10 AND(False, False) -> c ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil))) domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))) eqNatList[Ite](False, z0, z1, z2, z3) -> False eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1) prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Cons(z0, z1), Nil) -> False prefix(Nil, z0) -> True domatch(Cons(z0, z1), Nil, z2) -> Nil domatch(Nil, Nil, z0) -> Cons(z0, Nil) domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3) eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1) eqNatList(Cons(z0, z1), Nil) -> False eqNatList(Nil, Cons(z0, z1)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False strmatch(z0, z1) -> domatch(z0, z1, Nil) Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 S tuples: PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 K tuples:none Defined Rule Symbols: prefix_2, domatch_3, eqNatList_2, notEmpty_1, strmatch_2, and_2, !EQ_2, domatch[Ite]_4, eqNatList[Ite]_5 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, PREFIX_2, DOMATCH_3, EQNATLIST_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c12_3, c15, c16, c17_2, c18_2, c19, c20, c21 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil))) domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))) eqNatList[Ite](False, z0, z1, z2, z3) -> False eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1) prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Cons(z0, z1), Nil) -> False prefix(Nil, z0) -> True domatch(Cons(z0, z1), Nil, z2) -> Nil domatch(Nil, Nil, z0) -> Cons(z0, Nil) domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3) eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1) eqNatList(Cons(z0, z1), Nil) -> False eqNatList(Nil, Cons(z0, z1)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False strmatch(z0, z1) -> domatch(z0, z1, Nil) Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples:none Defined Rule Symbols: prefix_2, domatch_3, eqNatList_2, notEmpty_1, strmatch_2, and_2, !EQ_2, domatch[Ite]_4, eqNatList[Ite]_5 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil))) domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))) eqNatList[Ite](False, z0, z1, z2, z3) -> False eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1) domatch(Cons(z0, z1), Nil, z2) -> Nil domatch(Nil, Nil, z0) -> Cons(z0, Nil) domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3) eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1) eqNatList(Cons(z0, z1), Nil) -> False eqNatList(Nil, Cons(z0, z1)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False strmatch(z0, z1) -> domatch(z0, z1, Nil) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples:none Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 We considered the (Usable) Rules:none And the Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(!EQ(x_1, x_2)) = [1] + x_2 POL(!EQ'(x_1, x_2)) = 0 POL(0) = [1] POL(Cons(x_1, x_2)) = 0 POL(DOMATCH(x_1, x_2, x_3)) = x_1 + x_3 POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 + x_3 + x_4 POL(EQNATLIST(x_1, x_2)) = [1] POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = [1] POL(False) = [1] POL(Nil) = 0 POL(PREFIX(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(True) = [1] POL(and(x_1, x_2)) = [1] + x_1 POL(c11(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c15) = 0 POL(c16) = 0 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19) = 0 POL(c20) = 0 POL(c21) = 0 POL(c4(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(prefix(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples: EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. DOMATCH(Cons(z0, z1), Nil, z2) -> c15 We considered the (Usable) Rules:none And the Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(!EQ(x_1, x_2)) = [1] POL(!EQ'(x_1, x_2)) = 0 POL(0) = [1] POL(Cons(x_1, x_2)) = [1] POL(DOMATCH(x_1, x_2, x_3)) = x_1 POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 POL(EQNATLIST(x_1, x_2)) = 0 POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0 POL(False) = [1] POL(Nil) = 0 POL(PREFIX(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(True) = 0 POL(and(x_1, x_2)) = [1] + x_1 POL(c11(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c15) = 0 POL(c16) = 0 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19) = 0 POL(c20) = 0 POL(c21) = 0 POL(c4(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(prefix(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples: EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. DOMATCH(Nil, Nil, z0) -> c16 We considered the (Usable) Rules:none And the Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(!EQ(x_1, x_2)) = [1] POL(!EQ'(x_1, x_2)) = 0 POL(0) = [1] POL(Cons(x_1, x_2)) = 0 POL(DOMATCH(x_1, x_2, x_3)) = x_1 + x_3 POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 + x_3 + x_4 POL(EQNATLIST(x_1, x_2)) = 0 POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0 POL(False) = [1] POL(Nil) = [1] POL(PREFIX(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(True) = 0 POL(and(x_1, x_2)) = [1] + x_1 POL(c11(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c15) = 0 POL(c16) = 0 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19) = 0 POL(c20) = 0 POL(c21) = 0 POL(c4(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(prefix(x_1, x_2)) = [1] + x_1 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples: EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) We considered the (Usable) Rules:none And the Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(!EQ(x_1, x_2)) = 0 POL(!EQ'(x_1, x_2)) = 0 POL(0) = [3] POL(Cons(x_1, x_2)) = [3] + x_2 POL(DOMATCH(x_1, x_2, x_3)) = 0 POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = 0 POL(EQNATLIST(x_1, x_2)) = [3]x_1 + x_2 POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = x_3 + [3]x_5 POL(False) = 0 POL(Nil) = 0 POL(PREFIX(x_1, x_2)) = 0 POL(S(x_1)) = [3] + x_1 POL(True) = 0 POL(and(x_1, x_2)) = 0 POL(c11(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c15) = 0 POL(c16) = 0 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19) = 0 POL(c20) = 0 POL(c21) = 0 POL(c4(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(prefix(x_1, x_2)) = [3]x_1 + [3]x_2 ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples: EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) We considered the (Usable) Rules:none And the Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(!EQ(x_1, x_2)) = [1] POL(!EQ'(x_1, x_2)) = 0 POL(0) = [1] POL(Cons(x_1, x_2)) = [1] + x_2 POL(DOMATCH(x_1, x_2, x_3)) = [1] + x_1 + x_2 POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 + x_3 POL(EQNATLIST(x_1, x_2)) = 0 POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0 POL(False) = [1] POL(Nil) = 0 POL(PREFIX(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(True) = 0 POL(and(x_1, x_2)) = [1] + x_1 POL(c11(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c15) = 0 POL(c16) = 0 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19) = 0 POL(c20) = 0 POL(c21) = 0 POL(c4(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(prefix(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples: PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) K tuples: EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) We considered the (Usable) Rules:none And the Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(!EQ(x_1, x_2)) = 0 POL(!EQ'(x_1, x_2)) = 0 POL(0) = 0 POL(Cons(x_1, x_2)) = [1] + x_2 POL(DOMATCH(x_1, x_2, x_3)) = x_1 + x_1*x_2 POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2*x_3 POL(EQNATLIST(x_1, x_2)) = 0 POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0 POL(False) = 0 POL(Nil) = 0 POL(PREFIX(x_1, x_2)) = x_1 POL(S(x_1)) = 0 POL(True) = 0 POL(and(x_1, x_2)) = [1] POL(c11(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c15) = 0 POL(c16) = 0 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19) = 0 POL(c20) = 0 POL(c21) = 0 POL(c4(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(prefix(x_1, x_2)) = 0 ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3)) prefix(Nil, z0) -> True prefix(Cons(z0, z1), Nil) -> False and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(z0), S(z1)) -> !EQ(z0, z1) !EQ(0, S(z0)) -> False !EQ(S(z0), 0) -> False !EQ(0, 0) -> True Tuples: !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1)) DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1)) DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) S tuples:none K tuples: EQNATLIST(Cons(z0, z1), Nil) -> c19 EQNATLIST(Nil, Cons(z0, z1)) -> c20 EQNATLIST(Nil, Nil) -> c21 DOMATCH(Cons(z0, z1), Nil, z2) -> c15 DOMATCH(Nil, Nil, z0) -> c16 EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2)) DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3)) Defined Rule Symbols: prefix_2, and_2, !EQ_2 Defined Pair Symbols: !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2 Compound Symbols: c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2 ---------------------------------------- (23) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (24) BOUNDS(1, 1) ---------------------------------------- (25) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (26) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), y, ys, x, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, y, ys, x, xs) -> False eqNatList[Ite](True, y, ys, x, xs) -> eqNatList(xs, ys) Rewrite Strategy: INNERMOST ---------------------------------------- (27) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: eqNatList[Ite]/1 eqNatList[Ite]/3 ---------------------------------------- (28) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, ys, xs) -> False eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys) Rewrite Strategy: INNERMOST ---------------------------------------- (29) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (30) Obligation: Innermost TRS: Rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, ys, xs) -> False eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys) Types: prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' and :: False:True -> False:True -> False:True !EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' Nil :: Cons:Nil:S:0' False :: False:True True :: False:True domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True notEmpty :: Cons:Nil:S:0' -> False:True strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' S :: Cons:Nil:S:0' -> Cons:Nil:S:0' 0' :: Cons:Nil:S:0' hole_False:True1_0 :: False:True hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0' gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0' ---------------------------------------- (31) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: prefix, !EQ, domatch, eqNatList They will be analysed ascendingly in the following order: !EQ < prefix prefix < domatch !EQ < eqNatList ---------------------------------------- (32) Obligation: Innermost TRS: Rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, ys, xs) -> False eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys) Types: prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' and :: False:True -> False:True -> False:True !EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' Nil :: Cons:Nil:S:0' False :: False:True True :: False:True domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True notEmpty :: Cons:Nil:S:0' -> False:True strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' S :: Cons:Nil:S:0' -> Cons:Nil:S:0' 0' :: Cons:Nil:S:0' hole_False:True1_0 :: False:True hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0' gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0' Generator Equations: gen_Cons:Nil:S:0'3_0(0) <=> Nil gen_Cons:Nil:S:0'3_0(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0'3_0(x)) The following defined symbols remain to be analysed: !EQ, prefix, domatch, eqNatList They will be analysed ascendingly in the following order: !EQ < prefix prefix < domatch !EQ < eqNatList ---------------------------------------- (33) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: prefix(gen_Cons:Nil:S:0'3_0(+(1, n20_0)), gen_Cons:Nil:S:0'3_0(+(1, n20_0))) -> *4_0, rt in Omega(n20_0) Induction Base: prefix(gen_Cons:Nil:S:0'3_0(+(1, 0)), gen_Cons:Nil:S:0'3_0(+(1, 0))) Induction Step: prefix(gen_Cons:Nil:S:0'3_0(+(1, +(n20_0, 1))), gen_Cons:Nil:S:0'3_0(+(1, +(n20_0, 1)))) ->_R^Omega(1) and(!EQ(Nil, Nil), prefix(gen_Cons:Nil:S:0'3_0(+(1, n20_0)), gen_Cons:Nil:S:0'3_0(+(1, n20_0)))) ->_IH and(!EQ(Nil, Nil), *4_0) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (34) Complex Obligation (BEST) ---------------------------------------- (35) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, ys, xs) -> False eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys) Types: prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' and :: False:True -> False:True -> False:True !EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' Nil :: Cons:Nil:S:0' False :: False:True True :: False:True domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True notEmpty :: Cons:Nil:S:0' -> False:True strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' S :: Cons:Nil:S:0' -> Cons:Nil:S:0' 0' :: Cons:Nil:S:0' hole_False:True1_0 :: False:True hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0' gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0' Generator Equations: gen_Cons:Nil:S:0'3_0(0) <=> Nil gen_Cons:Nil:S:0'3_0(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0'3_0(x)) The following defined symbols remain to be analysed: prefix, domatch, eqNatList They will be analysed ascendingly in the following order: prefix < domatch ---------------------------------------- (36) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (37) BOUNDS(n^1, INF) ---------------------------------------- (38) Obligation: Innermost TRS: Rules: prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs)) domatch(Cons(x, xs), Nil, n) -> Nil domatch(Nil, Nil, n) -> Cons(n, Nil) prefix(Cons(x, xs), Nil) -> False prefix(Nil, cs) -> True domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n) eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs) eqNatList(Cons(x, xs), Nil) -> False eqNatList(Nil, Cons(y, ys)) -> False eqNatList(Nil, Nil) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False strmatch(patstr, str) -> domatch(patstr, str, Nil) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))) eqNatList[Ite](False, ys, xs) -> False eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys) Types: prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' and :: False:True -> False:True -> False:True !EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' Nil :: Cons:Nil:S:0' False :: False:True True :: False:True domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True notEmpty :: Cons:Nil:S:0' -> False:True strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' S :: Cons:Nil:S:0' -> Cons:Nil:S:0' 0' :: Cons:Nil:S:0' hole_False:True1_0 :: False:True hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0' gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0' Lemmas: prefix(gen_Cons:Nil:S:0'3_0(+(1, n20_0)), gen_Cons:Nil:S:0'3_0(+(1, n20_0))) -> *4_0, rt in Omega(n20_0) Generator Equations: gen_Cons:Nil:S:0'3_0(0) <=> Nil gen_Cons:Nil:S:0'3_0(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0'3_0(x)) The following defined symbols remain to be analysed: domatch, eqNatList