WORST_CASE(Omega(n^1),O(n^1)) proof of input_JBpugWJNBN.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxTRS (1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (2) CpxTRS (3) CpxTrsMatchBoundsTAProof [FINISHED, 13 ms] (4) BOUNDS(1, n^1) (5) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxRelTRS (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) typed CpxTrs (13) OrderProof [LOWER BOUND(ID), 2 ms] (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 1635 ms] (16) proven lower bound (17) LowerBoundPropagationProof [FINISHED, 0 ms] (18) BOUNDS(n^1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: +(0, y) -> y +(s(x), y) -> s(+(x, y)) +(s(x), y) -> +(x, s(y)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (2) 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: +(0, y) -> y +(s(x), y) -> s(+(x, y)) +(s(x), y) -> +(x, s(y)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsMatchBoundsTAProof (FINISHED) A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1. The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: final states : [1] transitions: 00() -> 0 s0(0) -> 0 +0(0, 0) -> 1 +1(0, 0) -> 2 s1(2) -> 1 s1(0) -> 3 +1(0, 3) -> 1 +1(0, 3) -> 2 s1(2) -> 2 s1(3) -> 3 0 -> 1 0 -> 2 3 -> 1 3 -> 2 ---------------------------------------- (4) BOUNDS(1, n^1) ---------------------------------------- (5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: +(0, z0) -> z0 +(s(z0), z1) -> s(+(z0, z1)) +(s(z0), z1) -> +(z0, s(z1)) Tuples: +'(0, z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) S tuples: +'(0, z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c, c1_1, c2_1 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: +'(0, z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) The (relative) TRS S consists of the following rules: +(0, z0) -> z0 +(s(z0), z1) -> s(+(z0, z1)) +(s(z0), z1) -> +(z0, s(z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (9) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: +'(0', z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) The (relative) TRS S consists of the following rules: +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) +'(s(z0), z1) -> +'(z0, s(z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (12) Obligation: Innermost TRS: Rules: +'(0', z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) +'(s(z0), z1) -> +'(z0, s(z1)) Types: +' :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 -> 0':c:s:c1:c2 0' :: 0':c:s:c1:c2 c :: 0':c:s:c1:c2 s :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 c1 :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 c2 :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 hole_0':c:s:c1:c21_3 :: 0':c:s:c1:c2 gen_0':c:s:c1:c22_3 :: Nat -> 0':c:s:c1:c2 ---------------------------------------- (13) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: +' ---------------------------------------- (14) Obligation: Innermost TRS: Rules: +'(0', z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) +'(s(z0), z1) -> +'(z0, s(z1)) Types: +' :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 -> 0':c:s:c1:c2 0' :: 0':c:s:c1:c2 c :: 0':c:s:c1:c2 s :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 c1 :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 c2 :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 hole_0':c:s:c1:c21_3 :: 0':c:s:c1:c2 gen_0':c:s:c1:c22_3 :: Nat -> 0':c:s:c1:c2 Generator Equations: gen_0':c:s:c1:c22_3(0) <=> 0' gen_0':c:s:c1:c22_3(+(x, 1)) <=> s(gen_0':c:s:c1:c22_3(x)) The following defined symbols remain to be analysed: +' ---------------------------------------- (15) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: +'(gen_0':c:s:c1:c22_3(+(1, n4_3)), gen_0':c:s:c1:c22_3(b)) -> *3_3, rt in Omega(n4_3) Induction Base: +'(gen_0':c:s:c1:c22_3(+(1, 0)), gen_0':c:s:c1:c22_3(b)) Induction Step: +'(gen_0':c:s:c1:c22_3(+(1, +(n4_3, 1))), gen_0':c:s:c1:c22_3(b)) ->_R^Omega(1) c1(+'(gen_0':c:s:c1:c22_3(+(1, n4_3)), gen_0':c:s:c1:c22_3(b))) ->_IH c1(*3_3) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (16) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: +'(0', z0) -> c +'(s(z0), z1) -> c1(+'(z0, z1)) +'(s(z0), z1) -> c2(+'(z0, s(z1))) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) +'(s(z0), z1) -> +'(z0, s(z1)) Types: +' :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 -> 0':c:s:c1:c2 0' :: 0':c:s:c1:c2 c :: 0':c:s:c1:c2 s :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 c1 :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 c2 :: 0':c:s:c1:c2 -> 0':c:s:c1:c2 hole_0':c:s:c1:c21_3 :: 0':c:s:c1:c2 gen_0':c:s:c1:c22_3 :: Nat -> 0':c:s:c1:c2 Generator Equations: gen_0':c:s:c1:c22_3(0) <=> 0' gen_0':c:s:c1:c22_3(+(x, 1)) <=> s(gen_0':c:s:c1:c22_3(x)) The following defined symbols remain to be analysed: +' ---------------------------------------- (17) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (18) BOUNDS(n^1, INF)