WORST_CASE(Omega(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, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) typed CpxTrs (5) OrderProof [LOWER BOUND(ID), 0 ms] (6) typed CpxTrs (7) RewriteLemmaProof [LOWER BOUND(ID), 1289 ms] (8) proven lower bound (9) LowerBoundPropagationProof [FINISHED, 0 ms] (10) BOUNDS(n^1, INF) ---------------------------------------- (0) 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: dfib(s(s(x)), y) -> dfib(s(x), dfib(x, y)) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (2) 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: dfib(s(s(x)), y) -> dfib(s(x), dfib(x, y)) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (3) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Innermost TRS: Rules: dfib(s(s(x)), y) -> dfib(s(x), dfib(x, y)) Types: dfib :: s -> dfib -> dfib s :: s -> s hole_dfib1_0 :: dfib hole_s2_0 :: s gen_s3_0 :: Nat -> s ---------------------------------------- (5) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: dfib ---------------------------------------- (6) Obligation: Innermost TRS: Rules: dfib(s(s(x)), y) -> dfib(s(x), dfib(x, y)) Types: dfib :: s -> dfib -> dfib s :: s -> s hole_dfib1_0 :: dfib hole_s2_0 :: s gen_s3_0 :: Nat -> s Generator Equations: gen_s3_0(0) <=> hole_s2_0 gen_s3_0(+(x, 1)) <=> s(gen_s3_0(x)) The following defined symbols remain to be analysed: dfib ---------------------------------------- (7) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: dfib(gen_s3_0(+(2, *(2, n5_0))), hole_dfib1_0) -> *4_0, rt in Omega(n5_0) Induction Base: dfib(gen_s3_0(+(2, *(2, 0))), hole_dfib1_0) Induction Step: dfib(gen_s3_0(+(2, *(2, +(n5_0, 1)))), hole_dfib1_0) ->_R^Omega(1) dfib(s(gen_s3_0(+(2, *(2, n5_0)))), dfib(gen_s3_0(+(2, *(2, n5_0))), hole_dfib1_0)) ->_IH dfib(s(gen_s3_0(+(2, *(2, n5_0)))), *4_0) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (8) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: dfib(s(s(x)), y) -> dfib(s(x), dfib(x, y)) Types: dfib :: s -> dfib -> dfib s :: s -> s hole_dfib1_0 :: dfib hole_s2_0 :: s gen_s3_0 :: Nat -> s Generator Equations: gen_s3_0(0) <=> hole_s2_0 gen_s3_0(+(x, 1)) <=> s(gen_s3_0(x)) The following defined symbols remain to be analysed: dfib ---------------------------------------- (9) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (10) BOUNDS(n^1, INF)