WORST_CASE(?,O(n^1)) proof of input_KaCUPZMQ9k.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)), 65 ms] (8) CdtProblem (9) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (10) 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: purge(nil) -> nil purge(.(x, y)) -> .(x, purge(remove(x, y))) remove(x, nil) -> nil remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(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: purge(nil) -> nil purge(.(z0, z1)) -> .(z0, purge(remove(z0, z1))) remove(z0, nil) -> nil remove(z0, .(z1, z2)) -> if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2))) Tuples: PURGE(nil) -> c PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, nil) -> c2 REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) S tuples: PURGE(nil) -> c PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, nil) -> c2 REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) K tuples:none Defined Rule Symbols: purge_1, remove_2 Defined Pair Symbols: PURGE_1, REMOVE_2 Compound Symbols: c, c1_2, c2, c3_1, c4_1 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: REMOVE(z0, nil) -> c2 PURGE(nil) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: purge(nil) -> nil purge(.(z0, z1)) -> .(z0, purge(remove(z0, z1))) remove(z0, nil) -> nil remove(z0, .(z1, z2)) -> if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2))) Tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) S tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) K tuples:none Defined Rule Symbols: purge_1, remove_2 Defined Pair Symbols: PURGE_1, REMOVE_2 Compound Symbols: c1_2, c3_1, c4_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: purge(nil) -> nil purge(.(z0, z1)) -> .(z0, purge(remove(z0, z1))) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, nil) -> nil remove(z0, .(z1, z2)) -> if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2))) Tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) S tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) K tuples:none Defined Rule Symbols: remove_2 Defined Pair Symbols: PURGE_1, REMOVE_2 Compound Symbols: c1_2, c3_1, c4_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. PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) We considered the (Usable) Rules: remove(z0, nil) -> nil remove(z0, .(z1, z2)) -> if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2))) And the Tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(.(x_1, x_2)) = [2] + x_1 + x_2 POL(=(x_1, x_2)) = 0 POL(PURGE(x_1)) = [2]x_1 POL(REMOVE(x_1, x_2)) = x_1 + x_2 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(if(x_1, x_2, x_3)) = x_1 POL(nil) = 0 POL(remove(x_1, x_2)) = 0 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, nil) -> nil remove(z0, .(z1, z2)) -> if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2))) Tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) S tuples:none K tuples: PURGE(.(z0, z1)) -> c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) REMOVE(z0, .(z1, z2)) -> c3(REMOVE(z0, z2)) REMOVE(z0, .(z1, z2)) -> c4(REMOVE(z0, z2)) Defined Rule Symbols: remove_2 Defined Pair Symbols: PURGE_1, REMOVE_2 Compound Symbols: c1_2, c3_1, c4_1 ---------------------------------------- (9) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (10) BOUNDS(1, 1)