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 CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 303 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 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)), 42 ms] (12) CdtProblem (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (14) BOUNDS(1, 1) (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (16) TRS for Loop Detection (17) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (18) BEST (19) proven lower bound (20) LowerBoundPropagationProof [FINISHED, 0 ms] (21) BOUNDS(n^1, INF) (22) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 The (relative) TRS S consists of the following rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 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^1). The TRS R consists of the following rules: MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 The (relative) TRS S consists of the following rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 Tuples: MERGE'(nil, z0) -> c8 MERGE'(z0, nil) -> c9 MERGE'(.(z0, z1), .(z2, z3)) -> c10(IF'(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3)) ++''(nil, z0) -> c11 ++''(.(z0, z1), z2) -> c12(++''(z1, z2)) IF'(true, z0, z1) -> c13 IF'(false, z0, z1) -> c14 MERGE''(nil, z0) -> c15 MERGE''(z0, nil) -> c16 MERGE''(.(z0, z1), .(z2, z3)) -> c17(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) ++'''(nil, z0) -> c19 ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) IF''(true, z0, z1) -> c21 IF''(false, z0, z1) -> c22 S tuples: MERGE''(nil, z0) -> c15 MERGE''(z0, nil) -> c16 MERGE''(.(z0, z1), .(z2, z3)) -> c17(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) ++'''(nil, z0) -> c19 ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) IF''(true, z0, z1) -> c21 IF''(false, z0, z1) -> c22 K tuples:none Defined Rule Symbols: MERGE_2, ++'_2, IF_3, merge_2, ++_2, if_3 Defined Pair Symbols: MERGE'_2, ++''_2, IF'_3, MERGE''_2, ++'''_2, IF''_3 Compound Symbols: c8, c9, c10_3, c11, c12_1, c13, c14, c15, c16, c17_4, c18_4, c19, c20_1, c21, c22 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 10 trailing nodes: ++'''(nil, z0) -> c19 IF'(true, z0, z1) -> c13 IF'(false, z0, z1) -> c14 MERGE''(z0, nil) -> c16 ++''(nil, z0) -> c11 MERGE'(z0, nil) -> c9 IF''(false, z0, z1) -> c22 IF''(true, z0, z1) -> c21 MERGE''(nil, z0) -> c15 MERGE'(nil, z0) -> c8 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 Tuples: MERGE'(.(z0, z1), .(z2, z3)) -> c10(IF'(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3)) ++''(.(z0, z1), z2) -> c12(++''(z1, z2)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) S tuples: MERGE''(.(z0, z1), .(z2, z3)) -> c17(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(IF''(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) K tuples:none Defined Rule Symbols: MERGE_2, ++'_2, IF_3, merge_2, ++_2, if_3 Defined Pair Symbols: MERGE'_2, ++''_2, MERGE''_2, ++'''_2 Compound Symbols: c10_3, c12_1, c17_4, c18_4, c20_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 Tuples: ++''(.(z0, z1), z2) -> c12(++''(z1, z2)) ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE'(.(z0, z1), .(z2, z3)) -> c10(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) S tuples: ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) K tuples:none Defined Rule Symbols: MERGE_2, ++'_2, IF_3, merge_2, ++_2, if_3 Defined Pair Symbols: ++''_2, ++'''_2, MERGE'_2, MERGE''_2 Compound Symbols: c12_1, c20_1, c10_2, c17_3, c18_3 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: ++''(.(z0, z1), z2) -> c12(++''(z1, z2)) ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE'(.(z0, z1), .(z2, z3)) -> c10(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) S tuples: ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: ++''_2, ++'''_2, MERGE'_2, MERGE''_2 Compound Symbols: c12_1, c20_1, c10_2, c17_3, c18_3 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) We considered the (Usable) Rules:none And the Tuples: ++''(.(z0, z1), z2) -> c12(++''(z1, z2)) ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE'(.(z0, z1), .(z2, z3)) -> c10(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(++''(x_1, x_2)) = x_1 POL(++'''(x_1, x_2)) = x_1 POL(.(x_1, x_2)) = [1] + x_2 POL(MERGE'(x_1, x_2)) = 0 POL(MERGE''(x_1, x_2)) = x_1 + x_2 POL(c10(x_1, x_2)) = x_1 + x_2 POL(c12(x_1)) = x_1 POL(c17(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c18(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c20(x_1)) = x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: ++''(.(z0, z1), z2) -> c12(++''(z1, z2)) ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE'(.(z0, z1), .(z2, z3)) -> c10(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) S tuples:none K tuples: ++'''(.(z0, z1), z2) -> c20(++'''(z1, z2)) MERGE''(.(z0, z1), .(z2, z3)) -> c17(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(z1, .(z2, z3))) MERGE''(.(z0, z1), .(z2, z3)) -> c18(MERGE'(z1, .(z2, z3)), MERGE'(.(z0, z1), z3), MERGE''(.(z0, z1), z3)) Defined Rule Symbols:none Defined Pair Symbols: ++''_2, ++'''_2, MERGE'_2, MERGE''_2 Compound Symbols: c12_1, c20_1, c10_2, c17_3, c18_3 ---------------------------------------- (13) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (14) BOUNDS(1, 1) ---------------------------------------- (15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (16) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 The (relative) TRS S consists of the following rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (17) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence ++'(.(z0, z1), z2) ->^+ c5(++'(z1, z2)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / .(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (18) Complex Obligation (BEST) ---------------------------------------- (19) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 The (relative) TRS S consists of the following rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (20) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (21) BOUNDS(n^1, INF) ---------------------------------------- (22) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: MERGE(nil, z0) -> c MERGE(z0, nil) -> c1 MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3))) MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3)) ++'(nil, z0) -> c4 ++'(.(z0, z1), z2) -> c5(++'(z1, z2)) IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 The (relative) TRS S consists of the following rules: merge(nil, z0) -> z0 merge(z0, nil) -> z0 merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) ++(nil, z0) -> z0 ++(.(z0, z1), z2) -> .(z0, ++(z1, z2)) if(true, z0, z1) -> z0 if(false, z0, z1) -> z0 Rewrite Strategy: INNERMOST