WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^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) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 79 ms] (6) CdtProblem (7) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (8) BOUNDS(1, 1) (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxTRS (11) SlicingProof [LOWER BOUND(ID), 0 ms] (12) CpxTRS (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (14) typed CpxTrs (15) OrderProof [LOWER BOUND(ID), 0 ms] (16) typed CpxTrs (17) RewriteLemmaProof [LOWER BOUND(ID), 201 ms] (18) proven lower bound (19) LowerBoundPropagationProof [FINISHED, 0 ms] (20) BOUNDS(n^1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: f(0, y) -> 0 f(s(x), y) -> f(f(x, y), y) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) Tuples: F(0, z0) -> c F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) S tuples: F(0, z0) -> c F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c, c1_2 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, z0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) Tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) S tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) K tuples:none Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c1_2 ---------------------------------------- (5) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) We considered the (Usable) Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) And the Tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(F(x_1, x_2)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(f(x_1, x_2)) = 0 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f(0, z0) -> 0 f(s(z0), z1) -> f(f(z0, z1), z1) Tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) S tuples:none K tuples: F(s(z0), z1) -> c1(F(f(z0, z1), z1), F(z0, z1)) Defined Rule Symbols: f_2 Defined Pair Symbols: F_2 Compound Symbols: c1_2 ---------------------------------------- (7) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (8) BOUNDS(1, 1) ---------------------------------------- (9) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: f(0', y) -> 0' f(s(x), y) -> f(f(x, y), y) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (11) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: f/1 ---------------------------------------- (12) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: f(0') -> 0' f(s(x)) -> f(f(x)) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (13) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (14) Obligation: Innermost TRS: Rules: f(0') -> 0' f(s(x)) -> f(f(x)) Types: f :: 0':s -> 0':s 0' :: 0':s s :: 0':s -> 0':s hole_0':s1_0 :: 0':s gen_0':s2_0 :: Nat -> 0':s ---------------------------------------- (15) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: f ---------------------------------------- (16) Obligation: Innermost TRS: Rules: f(0') -> 0' f(s(x)) -> f(f(x)) Types: f :: 0':s -> 0':s 0' :: 0':s s :: 0':s -> 0':s hole_0':s1_0 :: 0':s gen_0':s2_0 :: Nat -> 0':s Generator Equations: gen_0':s2_0(0) <=> 0' gen_0':s2_0(+(x, 1)) <=> s(gen_0':s2_0(x)) The following defined symbols remain to be analysed: f ---------------------------------------- (17) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: f(gen_0':s2_0(n4_0)) -> gen_0':s2_0(0), rt in Omega(1 + n4_0) Induction Base: f(gen_0':s2_0(0)) ->_R^Omega(1) 0' Induction Step: f(gen_0':s2_0(+(n4_0, 1))) ->_R^Omega(1) f(f(gen_0':s2_0(n4_0))) ->_IH f(gen_0':s2_0(0)) ->_R^Omega(1) 0' We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (18) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: f(0') -> 0' f(s(x)) -> f(f(x)) Types: f :: 0':s -> 0':s 0' :: 0':s s :: 0':s -> 0':s hole_0':s1_0 :: 0':s gen_0':s2_0 :: Nat -> 0':s Generator Equations: gen_0':s2_0(0) <=> 0' gen_0':s2_0(+(x, 1)) <=> s(gen_0':s2_0(x)) The following defined symbols remain to be analysed: f ---------------------------------------- (19) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (20) BOUNDS(n^1, INF)