WORST_CASE(?,O(n^2)) proof of input_fKzxHMbrlg.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^2). (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)), 109 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 93 ms] (8) CdtProblem (9) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 50 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^2). The TRS R consists of the following rules: sort(nil) -> nil sort(cons(x, y)) -> insert(x, sort(y)) insert(x, nil) -> cons(x, nil) insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w)) choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w)) choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, 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: sort(nil) -> nil sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) Tuples: SORT(nil) -> c SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, nil) -> c2 INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), z3, 0) -> c4 CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) S tuples: SORT(nil) -> c SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, nil) -> c2 INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), z3, 0) -> c4 CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) K tuples:none Defined Rule Symbols: sort_1, insert_2, choose_4 Defined Pair Symbols: SORT_1, INSERT_2, CHOOSE_4 Compound Symbols: c, c1_2, c2, c3_1, c4, c5_1, c6_1 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing nodes: INSERT(z0, nil) -> c2 CHOOSE(z0, cons(z1, z2), z3, 0) -> c4 SORT(nil) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: sort(nil) -> nil sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) S tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) K tuples:none Defined Rule Symbols: sort_1, insert_2, choose_4 Defined Pair Symbols: SORT_1, INSERT_2, CHOOSE_4 Compound Symbols: c1_2, c3_1, c5_1, c6_1 ---------------------------------------- (5) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) We considered the (Usable) Rules:none And the Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(CHOOSE(x_1, x_2, x_3, x_4)) = x_1 POL(INSERT(x_1, x_2)) = x_1 POL(SORT(x_1)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(choose(x_1, x_2, x_3, x_4)) = [1] + x_1 + x_2 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(insert(x_1, x_2)) = [1] + x_1 + x_2 POL(nil) = [1] POL(s(x_1)) = [1] + x_1 POL(sort(x_1)) = [1] + x_1 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: sort(nil) -> nil sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) S tuples: INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) K tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) Defined Rule Symbols: sort_1, insert_2, choose_4 Defined Pair Symbols: SORT_1, INSERT_2, CHOOSE_4 Compound Symbols: c1_2, c3_1, c5_1, c6_1 ---------------------------------------- (7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) We considered the (Usable) Rules: choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) sort(nil) -> nil insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) And the Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(CHOOSE(x_1, x_2, x_3, x_4)) = [2]x_2 POL(INSERT(x_1, x_2)) = [2]x_2 POL(SORT(x_1)) = [2]x_1^2 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(choose(x_1, x_2, x_3, x_4)) = [1] + x_2 POL(cons(x_1, x_2)) = [1] + x_2 POL(insert(x_1, x_2)) = [1] + x_2 POL(nil) = 0 POL(s(x_1)) = 0 POL(sort(x_1)) = x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: sort(nil) -> nil sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) S tuples: INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) K tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) Defined Rule Symbols: sort_1, insert_2, choose_4 Defined Pair Symbols: SORT_1, INSERT_2, CHOOSE_4 Compound Symbols: c1_2, c3_1, c5_1, c6_1 ---------------------------------------- (9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: sort(nil) -> nil sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) S tuples: CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) K tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) Defined Rule Symbols: sort_1, insert_2, choose_4 Defined Pair Symbols: SORT_1, INSERT_2, CHOOSE_4 Compound Symbols: c1_2, c3_1, c5_1, c6_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) We considered the (Usable) Rules: choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) sort(nil) -> nil insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) And the Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(CHOOSE(x_1, x_2, x_3, x_4)) = [2]x_3 + x_1*x_2 POL(INSERT(x_1, x_2)) = [2]x_1 + x_1*x_2 POL(SORT(x_1)) = [2]x_1^2 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(choose(x_1, x_2, x_3, x_4)) = [2] + x_1 + x_2 POL(cons(x_1, x_2)) = [2] + x_1 + x_2 POL(insert(x_1, x_2)) = [2] + x_1 + x_2 POL(nil) = 0 POL(s(x_1)) = [2] + x_1 POL(sort(x_1)) = [2] + x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: sort(nil) -> nil sort(cons(z0, z1)) -> insert(z0, sort(z1)) insert(z0, nil) -> cons(z0, nil) insert(z0, cons(z1, z2)) -> choose(z0, cons(z1, z2), z0, z1) choose(z0, cons(z1, z2), z3, 0) -> cons(z0, cons(z1, z2)) choose(z0, cons(z1, z2), 0, s(z3)) -> cons(z1, insert(z0, z2)) choose(z0, cons(z1, z2), s(z3), s(z4)) -> choose(z0, cons(z1, z2), z3, z4) Tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) S tuples:none K tuples: SORT(cons(z0, z1)) -> c1(INSERT(z0, sort(z1)), SORT(z1)) CHOOSE(z0, cons(z1, z2), 0, s(z3)) -> c5(INSERT(z0, z2)) INSERT(z0, cons(z1, z2)) -> c3(CHOOSE(z0, cons(z1, z2), z0, z1)) CHOOSE(z0, cons(z1, z2), s(z3), s(z4)) -> c6(CHOOSE(z0, cons(z1, z2), z3, z4)) Defined Rule Symbols: sort_1, insert_2, choose_4 Defined Pair Symbols: SORT_1, INSERT_2, CHOOSE_4 Compound Symbols: c1_2, c3_1, c5_1, c6_1 ---------------------------------------- (13) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (14) BOUNDS(1, 1)