WORST_CASE(?,O(n^1)) proof of input_v2CzHZxIBr.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(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) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 111 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 28 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 23 ms] (12) CdtProblem (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (14) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: msort(nil) -> nil msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y)))) min(x, nil) -> x min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z)) del(x, nil) -> nil del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: msort(nil) -> nil msort(.(z0, z1)) -> .(min(z0, z1), msort(del(min(z0, z1), .(z0, z1)))) min(z0, nil) -> z0 min(z0, .(z1, z2)) -> if(<=(z0, z1), min(z0, z2), min(z1, z2)) del(z0, nil) -> nil del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) Tuples: MSORT(nil) -> c MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, nil) -> c3 MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, nil) -> c6 DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) S tuples: MSORT(nil) -> c MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, nil) -> c3 MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, nil) -> c6 DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) K tuples:none Defined Rule Symbols: msort_1, min_2, del_2 Defined Pair Symbols: MSORT_1, MIN_2, DEL_2 Compound Symbols: c, c1_1, c2_3, c3, c4_1, c5_1, c6, c7_1 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing nodes: DEL(z0, nil) -> c6 MIN(z0, nil) -> c3 MSORT(nil) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: msort(nil) -> nil msort(.(z0, z1)) -> .(min(z0, z1), msort(del(min(z0, z1), .(z0, z1)))) min(z0, nil) -> z0 min(z0, .(z1, z2)) -> if(<=(z0, z1), min(z0, z2), min(z1, z2)) del(z0, nil) -> nil del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) S tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) K tuples:none Defined Rule Symbols: msort_1, min_2, del_2 Defined Pair Symbols: MSORT_1, MIN_2, DEL_2 Compound Symbols: c1_1, c2_3, c4_1, c5_1, c7_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: msort(nil) -> nil msort(.(z0, z1)) -> .(min(z0, z1), msort(del(min(z0, z1), .(z0, z1)))) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) del(z0, nil) -> nil min(z0, nil) -> z0 min(z0, .(z1, z2)) -> if(<=(z0, z1), min(z0, z2), min(z1, z2)) Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) S tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) K tuples:none Defined Rule Symbols: del_2, min_2 Defined Pair Symbols: MSORT_1, MIN_2, DEL_2 Compound Symbols: c1_1, c2_3, c4_1, c5_1, c7_1 ---------------------------------------- (7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) We considered the (Usable) Rules:none And the Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(.(x_1, x_2)) = [1] + x_1 + x_2 POL(<=(x_1, x_2)) = [1] + x_1 POL(=(x_1, x_2)) = 0 POL(DEL(x_1, x_2)) = 0 POL(MIN(x_1, x_2)) = 0 POL(MSORT(x_1)) = [1] POL(c1(x_1)) = x_1 POL(c2(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(del(x_1, x_2)) = [1] + x_1 + x_2 POL(if(x_1, x_2, x_3)) = x_1 + x_3 POL(min(x_1, x_2)) = [1] + x_1 + x_2 POL(nil) = [1] ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) del(z0, nil) -> nil min(z0, nil) -> z0 min(z0, .(z1, z2)) -> if(<=(z0, z1), min(z0, z2), min(z1, z2)) Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) S tuples: MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) K tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) Defined Rule Symbols: del_2, min_2 Defined Pair Symbols: MSORT_1, MIN_2, DEL_2 Compound Symbols: c1_1, c2_3, c4_1, c5_1, c7_1 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) We considered the (Usable) Rules: del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) And the Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(.(x_1, x_2)) = [1] + x_1 + x_2 POL(<=(x_1, x_2)) = [1] + x_1 + x_2 POL(=(x_1, x_2)) = 0 POL(DEL(x_1, x_2)) = 0 POL(MIN(x_1, x_2)) = x_1 + x_2 POL(MSORT(x_1)) = [1] + x_1 POL(c1(x_1)) = x_1 POL(c2(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(del(x_1, x_2)) = 0 POL(if(x_1, x_2, x_3)) = x_1 POL(min(x_1, x_2)) = [1] + x_1 + x_2 POL(nil) = 0 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) del(z0, nil) -> nil min(z0, nil) -> z0 min(z0, .(z1, z2)) -> if(<=(z0, z1), min(z0, z2), min(z1, z2)) Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) S tuples: DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) K tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) Defined Rule Symbols: del_2, min_2 Defined Pair Symbols: MSORT_1, MIN_2, DEL_2 Compound Symbols: c1_1, c2_3, c4_1, c5_1, c7_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) We considered the (Usable) Rules: del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) And the Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(.(x_1, x_2)) = [1] + x_1 + x_2 POL(<=(x_1, x_2)) = [1] + x_1 + x_2 POL(=(x_1, x_2)) = 0 POL(DEL(x_1, x_2)) = x_2 POL(MIN(x_1, x_2)) = 0 POL(MSORT(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c2(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(del(x_1, x_2)) = 0 POL(if(x_1, x_2, x_3)) = x_1 POL(min(x_1, x_2)) = [1] + x_1 + x_2 POL(nil) = 0 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: del(z0, .(z1, z2)) -> if(=(z0, z1), z2, .(z1, del(z0, z2))) del(z0, nil) -> nil min(z0, nil) -> z0 min(z0, .(z1, z2)) -> if(<=(z0, z1), min(z0, z2), min(z1, z2)) Tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) S tuples:none K tuples: MSORT(.(z0, z1)) -> c1(MIN(z0, z1)) MSORT(.(z0, z1)) -> c2(MSORT(del(min(z0, z1), .(z0, z1))), DEL(min(z0, z1), .(z0, z1)), MIN(z0, z1)) MIN(z0, .(z1, z2)) -> c4(MIN(z0, z2)) MIN(z0, .(z1, z2)) -> c5(MIN(z1, z2)) DEL(z0, .(z1, z2)) -> c7(DEL(z0, z2)) Defined Rule Symbols: del_2, min_2 Defined Pair Symbols: MSORT_1, MIN_2, DEL_2 Compound Symbols: c1_1, c2_3, c4_1, c5_1, c7_1 ---------------------------------------- (13) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (14) BOUNDS(1, 1)