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), 286 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 3 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 49 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 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: 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)) The (relative) TRS S consists of the following 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))) 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: 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)) The (relative) TRS S consists of the following 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))) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (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))) 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)) Tuples: PURGE'(nil) -> c5 PURGE'(.(z0, z1)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, nil) -> c7 REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(nil) -> c9 PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, nil) -> c11 REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) S tuples: PURGE''(nil) -> c9 PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, nil) -> c11 REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) K tuples:none Defined Rule Symbols: PURGE_1, REMOVE_2, purge_1, remove_2 Defined Pair Symbols: PURGE'_1, REMOVE'_2, PURGE''_1, REMOVE''_2 Compound Symbols: c5, c6_2, c7, c8_2, c9, c10_3, c11, c12_1, c13_1 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: PURGE''(nil) -> c9 REMOVE''(z0, nil) -> c11 REMOVE'(z0, nil) -> c7 PURGE'(nil) -> c5 ---------------------------------------- (6) 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))) 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)) Tuples: PURGE'(.(z0, z1)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) S tuples: PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) K tuples:none Defined Rule Symbols: PURGE_1, REMOVE_2, purge_1, remove_2 Defined Pair Symbols: PURGE'_1, REMOVE'_2, PURGE''_1, REMOVE''_2 Compound Symbols: c6_2, c8_2, c10_3, c12_1, c13_1 ---------------------------------------- (7) 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))) 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)) ---------------------------------------- (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)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) S tuples: PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) K tuples:none Defined Rule Symbols: remove_2 Defined Pair Symbols: PURGE'_1, REMOVE'_2, PURGE''_1, REMOVE''_2 Compound Symbols: c6_2, c8_2, c10_3, c12_1, c13_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. REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(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)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(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)) = 0 POL(PURGE'(x_1)) = x_1 POL(PURGE''(x_1)) = x_1 POL(REMOVE'(x_1, x_2)) = 0 POL(REMOVE''(x_1, x_2)) = x_2 POL(c10(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c6(x_1, x_2)) = x_1 + x_2 POL(c8(x_1, x_2)) = x_1 + x_2 POL(if(x_1, x_2, x_3)) = x_1 + x_2 POL(nil) = [1] POL(remove(x_1, x_2)) = [1] + x_1 ---------------------------------------- (10) 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)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) S tuples: PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) K tuples: REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) Defined Rule Symbols: remove_2 Defined Pair Symbols: PURGE'_1, REMOVE'_2, PURGE''_1, REMOVE''_2 Compound Symbols: c6_2, c8_2, c10_3, c12_1, c13_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. PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) 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)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(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)) = x_1 + x_2 POL(PURGE'(x_1)) = x_1 POL(PURGE''(x_1)) = x_1 POL(REMOVE'(x_1, x_2)) = 0 POL(REMOVE''(x_1, x_2)) = 0 POL(c10(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c6(x_1, x_2)) = x_1 + x_2 POL(c8(x_1, x_2)) = x_1 + x_2 POL(if(x_1, x_2, x_3)) = [1] + x_1 POL(nil) = [1] POL(remove(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (12) 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)) -> c6(PURGE'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, .(z1, z2)) -> c8(REMOVE'(z0, z2), REMOVE'(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) S tuples:none K tuples: REMOVE''(z0, .(z1, z2)) -> c12(REMOVE''(z0, z2)) REMOVE''(z0, .(z1, z2)) -> c13(REMOVE''(z0, z2)) PURGE''(.(z0, z1)) -> c10(PURGE''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) Defined Rule Symbols: remove_2 Defined Pair Symbols: PURGE'_1, REMOVE'_2, PURGE''_1, REMOVE''_2 Compound Symbols: c6_2, c8_2, c10_3, c12_1, c13_1 ---------------------------------------- (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: 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)) The (relative) TRS S consists of the following 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))) 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 REMOVE(z0, .(z1, z2)) ->^+ c4(REMOVE(z0, z2)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z2 / .(z1, z2)]. 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: 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)) The (relative) TRS S consists of the following 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))) 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: 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)) The (relative) TRS S consists of the following 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))) Rewrite Strategy: INNERMOST