WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 133 ms] (6) CdtProblem (7) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms] (10) CdtProblem (11) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 26 ms] (14) CdtProblem (15) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 27 ms] (18) CdtProblem (19) CdtKnowledgeProof [FINISHED, 0 ms] (20) BOUNDS(1, 1) (21) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CpxTRS (23) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (24) typed CpxTrs (25) OrderProof [LOWER BOUND(ID), 0 ms] (26) typed CpxTrs (27) RewriteLemmaProof [LOWER BOUND(ID), 271 ms] (28) BEST (29) proven lower bound (30) LowerBoundPropagationProof [FINISHED, 0 ms] (31) BOUNDS(n^1, INF) (32) typed CpxTrs (33) RewriteLemmaProof [LOWER BOUND(ID), 0 ms] (34) typed CpxTrs (35) RewriteLemmaProof [LOWER BOUND(ID), 87 ms] (36) typed CpxTrs (37) RewriteLemmaProof [LOWER BOUND(ID), 36 ms] (38) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPEND#1(nil, z0) -> c2 APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL#1(nil) -> c5 APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL2#1(nil) -> c8 APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL3#1(nil) -> c11 S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPEND#1(nil, z0) -> c2 APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL#1(nil) -> c5 APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL2#1(nil) -> c8 APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL3#1(nil) -> c11 K tuples:none Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c2, c3_1, c4_2, c5, c6_1, c7_3, c8, c9_1, c10_3, c11 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: APPENDALL#1(nil) -> c5 APPENDALL2#1(nil) -> c8 APPEND#1(nil, z0) -> c2 APPENDALL3#1(nil) -> c11 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) K tuples:none Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (5) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) We considered the (Usable) Rules:none And the Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(APPEND(x_1, x_2)) = 0 POL(APPEND#1(x_1, x_2)) = 0 POL(APPENDALL(x_1)) = 0 POL(APPENDALL#1(x_1)) = 0 POL(APPENDALL2(x_1)) = 0 POL(APPENDALL2#1(x_1)) = 0 POL(APPENDALL3(x_1)) = [1] + x_1 POL(APPENDALL3#1(x_1)) = x_1 POL(append(x_1, x_2)) = 0 POL(append#1(x_1, x_2)) = [1] + x_1 + x_2 POL(appendAll(x_1)) = x_1 POL(appendAll#1(x_1)) = [1] + x_1 POL(appendAll2(x_1)) = x_1 POL(appendAll2#1(x_1)) = [1] + x_1 POL(appendAll3(x_1)) = [1] + x_1 POL(appendAll3#1(x_1)) = [1] + x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c10(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c3(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c9(x_1)) = x_1 POL(nil) = [1] ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) We considered the (Usable) Rules:none And the Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(APPEND(x_1, x_2)) = 0 POL(APPEND#1(x_1, x_2)) = 0 POL(APPENDALL(x_1)) = 0 POL(APPENDALL#1(x_1)) = 0 POL(APPENDALL2(x_1)) = x_1 POL(APPENDALL2#1(x_1)) = x_1 POL(APPENDALL3(x_1)) = [1] + x_1 POL(APPENDALL3#1(x_1)) = [1] + x_1 POL(append(x_1, x_2)) = 0 POL(append#1(x_1, x_2)) = [1] + x_1 + x_2 POL(appendAll(x_1)) = x_1 POL(appendAll#1(x_1)) = [1] + x_1 POL(appendAll2(x_1)) = x_1 POL(appendAll2#1(x_1)) = [1] + x_1 POL(appendAll3(x_1)) = [1] + x_1 POL(appendAll3#1(x_1)) = [1] + x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c10(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c3(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c9(x_1)) = x_1 POL(nil) = [1] ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) We considered the (Usable) Rules:none And the Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(APPEND(x_1, x_2)) = 0 POL(APPEND#1(x_1, x_2)) = 0 POL(APPENDALL(x_1)) = x_1 POL(APPENDALL#1(x_1)) = x_1 POL(APPENDALL2(x_1)) = x_1 POL(APPENDALL2#1(x_1)) = x_1 POL(APPENDALL3(x_1)) = x_1 POL(APPENDALL3#1(x_1)) = x_1 POL(append(x_1, x_2)) = 0 POL(append#1(x_1, x_2)) = [1] + x_1 + x_2 POL(appendAll(x_1)) = x_1 POL(appendAll#1(x_1)) = [1] + x_1 POL(appendAll2(x_1)) = x_1 POL(appendAll2#1(x_1)) = [1] + x_1 POL(appendAll3(x_1)) = [1] + x_1 POL(appendAll3#1(x_1)) = [1] + x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c10(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c3(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c9(x_1)) = x_1 POL(nil) = [1] ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) We considered the (Usable) Rules: appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) append(z0, z1) -> append#1(z0, z1) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll#1(nil) -> nil append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) And the Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(::(x_1, x_2)) = [2] + x_1 + x_2 POL(APPEND(x_1, x_2)) = x_1 POL(APPEND#1(x_1, x_2)) = x_1 POL(APPENDALL(x_1)) = x_1 POL(APPENDALL#1(x_1)) = x_1 POL(APPENDALL2(x_1)) = [2]x_1 POL(APPENDALL2#1(x_1)) = [2]x_1 POL(APPENDALL3(x_1)) = [2] + [3]x_1 POL(APPENDALL3#1(x_1)) = [2] + [3]x_1 POL(append(x_1, x_2)) = x_1 + x_2 POL(append#1(x_1, x_2)) = x_1 + x_2 POL(appendAll(x_1)) = x_1 POL(appendAll#1(x_1)) = x_1 POL(appendAll2(x_1)) = x_1 POL(appendAll2#1(x_1)) = x_1 POL(appendAll3(x_1)) = [3] + [3]x_1 POL(appendAll3#1(x_1)) = [3] + [3]x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c10(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c3(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c9(x_1)) = x_1 POL(nil) = 0 ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 appendAll(z0) -> appendAll#1(z0) appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) appendAll#1(nil) -> nil appendAll2(z0) -> appendAll2#1(z0) appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) appendAll2#1(nil) -> nil appendAll3(z0) -> appendAll3#1(z0) appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) appendAll3#1(nil) -> nil Tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) S tuples: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) K tuples: APPENDALL3(z0) -> c9(APPENDALL3#1(z0)) APPENDALL3#1(::(z0, z1)) -> c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) APPENDALL(z0) -> c3(APPENDALL#1(z0)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) Defined Rule Symbols: append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1 Defined Pair Symbols: APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1 Compound Symbols: c_1, c1_1, c3_1, c4_2, c6_1, c7_3, c9_1, c10_3 ---------------------------------------- (19) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: APPEND(z0, z1) -> c(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) Now S is empty ---------------------------------------- (20) BOUNDS(1, 1) ---------------------------------------- (21) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (22) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (23) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (24) Obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil ---------------------------------------- (25) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1 They will be analysed ascendingly in the following order: append = append#1 append < appendAll#1 append < appendAll2#1 append < appendAll3#1 appendAll = appendAll#1 appendAll < appendAll2#1 appendAll2 = appendAll2#1 appendAll2 < appendAll3#1 appendAll3 = appendAll3#1 ---------------------------------------- (26) Obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil Generator Equations: gen_:::nil2_0(0) <=> nil gen_:::nil2_0(+(x, 1)) <=> ::(nil, gen_:::nil2_0(x)) The following defined symbols remain to be analysed: append#1, append, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1 They will be analysed ascendingly in the following order: append = append#1 append < appendAll#1 append < appendAll2#1 append < appendAll3#1 appendAll = appendAll#1 appendAll < appendAll2#1 appendAll2 = appendAll2#1 appendAll2 < appendAll3#1 appendAll3 = appendAll3#1 ---------------------------------------- (27) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) -> gen_:::nil2_0(+(n4_0, b)), rt in Omega(1 + n4_0) Induction Base: append#1(gen_:::nil2_0(0), gen_:::nil2_0(b)) ->_R^Omega(1) gen_:::nil2_0(b) Induction Step: append#1(gen_:::nil2_0(+(n4_0, 1)), gen_:::nil2_0(b)) ->_R^Omega(1) ::(nil, append(gen_:::nil2_0(n4_0), gen_:::nil2_0(b))) ->_R^Omega(1) ::(nil, append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b))) ->_IH ::(nil, gen_:::nil2_0(+(b, c5_0))) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (28) Complex Obligation (BEST) ---------------------------------------- (29) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil Generator Equations: gen_:::nil2_0(0) <=> nil gen_:::nil2_0(+(x, 1)) <=> ::(nil, gen_:::nil2_0(x)) The following defined symbols remain to be analysed: append#1, append, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1 They will be analysed ascendingly in the following order: append = append#1 append < appendAll#1 append < appendAll2#1 append < appendAll3#1 appendAll = appendAll#1 appendAll < appendAll2#1 appendAll2 = appendAll2#1 appendAll2 < appendAll3#1 appendAll3 = appendAll3#1 ---------------------------------------- (30) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (31) BOUNDS(n^1, INF) ---------------------------------------- (32) Obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil Lemmas: append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) -> gen_:::nil2_0(+(n4_0, b)), rt in Omega(1 + n4_0) Generator Equations: gen_:::nil2_0(0) <=> nil gen_:::nil2_0(+(x, 1)) <=> ::(nil, gen_:::nil2_0(x)) The following defined symbols remain to be analysed: append, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1 They will be analysed ascendingly in the following order: append = append#1 append < appendAll#1 append < appendAll2#1 append < appendAll3#1 appendAll = appendAll#1 appendAll < appendAll2#1 appendAll2 = appendAll2#1 appendAll2 < appendAll3#1 appendAll3 = appendAll3#1 ---------------------------------------- (33) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: appendAll#1(gen_:::nil2_0(n633_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n633_0) Induction Base: appendAll#1(gen_:::nil2_0(0)) ->_R^Omega(1) nil Induction Step: appendAll#1(gen_:::nil2_0(+(n633_0, 1))) ->_R^Omega(1) append(nil, appendAll(gen_:::nil2_0(n633_0))) ->_R^Omega(1) append(nil, appendAll#1(gen_:::nil2_0(n633_0))) ->_IH append(nil, gen_:::nil2_0(0)) ->_R^Omega(1) append#1(nil, gen_:::nil2_0(0)) ->_L^Omega(1) gen_:::nil2_0(+(0, 0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (34) Obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil Lemmas: append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) -> gen_:::nil2_0(+(n4_0, b)), rt in Omega(1 + n4_0) appendAll#1(gen_:::nil2_0(n633_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n633_0) Generator Equations: gen_:::nil2_0(0) <=> nil gen_:::nil2_0(+(x, 1)) <=> ::(nil, gen_:::nil2_0(x)) The following defined symbols remain to be analysed: appendAll, appendAll2, appendAll2#1, appendAll3, appendAll3#1 They will be analysed ascendingly in the following order: appendAll = appendAll#1 appendAll < appendAll2#1 appendAll2 = appendAll2#1 appendAll2 < appendAll3#1 appendAll3 = appendAll3#1 ---------------------------------------- (35) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: appendAll2#1(gen_:::nil2_0(n1017_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n1017_0) Induction Base: appendAll2#1(gen_:::nil2_0(0)) ->_R^Omega(1) nil Induction Step: appendAll2#1(gen_:::nil2_0(+(n1017_0, 1))) ->_R^Omega(1) append(appendAll(nil), appendAll2(gen_:::nil2_0(n1017_0))) ->_R^Omega(1) append(appendAll#1(nil), appendAll2(gen_:::nil2_0(n1017_0))) ->_L^Omega(1) append(gen_:::nil2_0(0), appendAll2(gen_:::nil2_0(n1017_0))) ->_R^Omega(1) append(gen_:::nil2_0(0), appendAll2#1(gen_:::nil2_0(n1017_0))) ->_IH append(gen_:::nil2_0(0), gen_:::nil2_0(0)) ->_R^Omega(1) append#1(gen_:::nil2_0(0), gen_:::nil2_0(0)) ->_L^Omega(1) gen_:::nil2_0(+(0, 0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (36) Obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil Lemmas: append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) -> gen_:::nil2_0(+(n4_0, b)), rt in Omega(1 + n4_0) appendAll#1(gen_:::nil2_0(n633_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n633_0) appendAll2#1(gen_:::nil2_0(n1017_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n1017_0) Generator Equations: gen_:::nil2_0(0) <=> nil gen_:::nil2_0(+(x, 1)) <=> ::(nil, gen_:::nil2_0(x)) The following defined symbols remain to be analysed: appendAll2, appendAll3, appendAll3#1 They will be analysed ascendingly in the following order: appendAll2 = appendAll2#1 appendAll2 < appendAll3#1 appendAll3 = appendAll3#1 ---------------------------------------- (37) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: appendAll3#1(gen_:::nil2_0(n1767_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n1767_0) Induction Base: appendAll3#1(gen_:::nil2_0(0)) ->_R^Omega(1) nil Induction Step: appendAll3#1(gen_:::nil2_0(+(n1767_0, 1))) ->_R^Omega(1) append(appendAll2(nil), appendAll3(gen_:::nil2_0(n1767_0))) ->_R^Omega(1) append(appendAll2#1(nil), appendAll3(gen_:::nil2_0(n1767_0))) ->_L^Omega(1) append(gen_:::nil2_0(0), appendAll3(gen_:::nil2_0(n1767_0))) ->_R^Omega(1) append(gen_:::nil2_0(0), appendAll3#1(gen_:::nil2_0(n1767_0))) ->_IH append(gen_:::nil2_0(0), gen_:::nil2_0(0)) ->_R^Omega(1) append#1(gen_:::nil2_0(0), gen_:::nil2_0(0)) ->_L^Omega(1) gen_:::nil2_0(+(0, 0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (38) Obligation: Innermost TRS: Rules: append(@l1, @l2) -> append#1(@l1, @l2) append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) append#1(nil, @l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls)) appendAll#1(nil) -> nil appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1, @ls)) -> append(appendAll(@l1), appendAll2(@ls)) appendAll2#1(nil) -> nil appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@l1, @ls)) -> append(appendAll2(@l1), appendAll3(@ls)) appendAll3#1(nil) -> nil Types: append :: :::nil -> :::nil -> :::nil append#1 :: :::nil -> :::nil -> :::nil :: :: :::nil -> :::nil -> :::nil nil :: :::nil appendAll :: :::nil -> :::nil appendAll#1 :: :::nil -> :::nil appendAll2 :: :::nil -> :::nil appendAll2#1 :: :::nil -> :::nil appendAll3 :: :::nil -> :::nil appendAll3#1 :: :::nil -> :::nil hole_:::nil1_0 :: :::nil gen_:::nil2_0 :: Nat -> :::nil Lemmas: append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) -> gen_:::nil2_0(+(n4_0, b)), rt in Omega(1 + n4_0) appendAll#1(gen_:::nil2_0(n633_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n633_0) appendAll2#1(gen_:::nil2_0(n1017_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n1017_0) appendAll3#1(gen_:::nil2_0(n1767_0)) -> gen_:::nil2_0(0), rt in Omega(1 + n1767_0) Generator Equations: gen_:::nil2_0(0) <=> nil gen_:::nil2_0(+(x, 1)) <=> ::(nil, gen_:::nil2_0(x)) The following defined symbols remain to be analysed: appendAll3 They will be analysed ascendingly in the following order: appendAll3 = appendAll3#1