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), 264 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)), 26 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: OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) The (relative) TRS S consists of the following rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(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: OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) The (relative) TRS S consists of the following rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(z0, z2)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(z0, z2)) OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) Tuples: OR'(true, z0) -> c7 OR'(z0, true) -> c8 OR'(false, false) -> c9 MEM'(z0, nil) -> c10 MEM'(z0, set(z1)) -> c11 MEM'(z0, union(z1, z2)) -> c12(OR'(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2)) OR''(true, z0) -> c13 OR''(z0, true) -> c14 OR''(false, false) -> c15 MEM''(z0, nil) -> c16 MEM''(z0, set(z1)) -> c17 MEM''(z0, union(z1, z2)) -> c18(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) S tuples: OR''(true, z0) -> c13 OR''(z0, true) -> c14 OR''(false, false) -> c15 MEM''(z0, nil) -> c16 MEM''(z0, set(z1)) -> c17 MEM''(z0, union(z1, z2)) -> c18(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) K tuples:none Defined Rule Symbols: OR_2, MEM_2, or_2, mem_2 Defined Pair Symbols: OR'_2, MEM'_2, OR''_2, MEM''_2 Compound Symbols: c7, c8, c9, c10, c11, c12_3, c13, c14, c15, c16, c17, c18_4, c19_4 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 10 trailing nodes: OR''(false, false) -> c15 MEM'(z0, nil) -> c10 MEM'(z0, set(z1)) -> c11 MEM''(z0, set(z1)) -> c17 OR''(true, z0) -> c13 OR''(z0, true) -> c14 OR'(false, false) -> c9 OR'(z0, true) -> c8 MEM''(z0, nil) -> c16 OR'(true, z0) -> c7 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(z0, z2)) OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) Tuples: MEM'(z0, union(z1, z2)) -> c12(OR'(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2)) MEM''(z0, union(z1, z2)) -> c18(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) S tuples: MEM''(z0, union(z1, z2)) -> c18(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(OR''(mem(z0, z1), mem(z0, z2)), MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) K tuples:none Defined Rule Symbols: OR_2, MEM_2, or_2, mem_2 Defined Pair Symbols: MEM'_2, MEM''_2 Compound Symbols: c12_3, c18_4, c19_4 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(z0, z2)) OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) Tuples: MEM'(z0, union(z1, z2)) -> c12(MEM'(z0, z1), MEM'(z0, z2)) MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) S tuples: MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) K tuples:none Defined Rule Symbols: OR_2, MEM_2, or_2, mem_2 Defined Pair Symbols: MEM'_2, MEM''_2 Compound Symbols: c12_2, c18_3, c19_3 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(z0, z2)) OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: MEM'(z0, union(z1, z2)) -> c12(MEM'(z0, z1), MEM'(z0, z2)) MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) S tuples: MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: MEM'_2, MEM''_2 Compound Symbols: c12_2, c18_3, c19_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. MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) We considered the (Usable) Rules:none And the Tuples: MEM'(z0, union(z1, z2)) -> c12(MEM'(z0, z1), MEM'(z0, z2)) MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(MEM'(x_1, x_2)) = 0 POL(MEM''(x_1, x_2)) = x_2 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c19(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(union(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: MEM'(z0, union(z1, z2)) -> c12(MEM'(z0, z1), MEM'(z0, z2)) MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) S tuples:none K tuples: MEM''(z0, union(z1, z2)) -> c18(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z1)) MEM''(z0, union(z1, z2)) -> c19(MEM'(z0, z1), MEM'(z0, z2), MEM''(z0, z2)) Defined Rule Symbols:none Defined Pair Symbols: MEM'_2, MEM''_2 Compound Symbols: c12_2, c18_3, c19_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: OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) The (relative) TRS S consists of the following rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(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 MEM(z0, union(z1, z2)) ->^+ c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [z2 / union(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: OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) The (relative) TRS S consists of the following rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(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: OR(true, z0) -> c OR(z0, true) -> c1 OR(false, false) -> c2 MEM(z0, nil) -> c3 MEM(z0, set(z1)) -> c4 MEM(z0, union(z1, z2)) -> c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1)) MEM(z0, union(z1, z2)) -> c6(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z2)) The (relative) TRS S consists of the following rules: or(true, z0) -> true or(z0, true) -> true or(false, false) -> false mem(z0, nil) -> false mem(z0, set(z1)) -> =(z0, z1) mem(z0, union(z1, z2)) -> or(mem(z0, z1), mem(z0, z2)) Rewrite Strategy: INNERMOST