WORST_CASE(Omega(n^1),O(n^1)) proof of input_QUR49vbx8u.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) CpxTrsMatchBoundsProof [FINISHED, 0 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), 5 ms] (12) typed CpxTrs (13) OrderProof [LOWER BOUND(ID), 0 ms] (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 460 ms] (16) BEST (17) proven lower bound (18) LowerBoundPropagationProof [FINISHED, 0 ms] (19) BOUNDS(n^1, INF) (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 157 ms] (22) BOUNDS(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: a(b(x)) -> b(a(x)) a(c(x)) -> x 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: a(b(x)) -> b(a(x)) a(c(x)) -> x S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsMatchBoundsProof (FINISHED) A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1. The certificate found is represented by the following graph. "[3, 4, 5] {(3,4,[a_1|0, b_1|1, c_1|1]), (3,5,[b_1|1]), (4,4,[b_1|0, c_1|0]), (5,4,[a_1|1, b_1|1, c_1|1]), (5,5,[b_1|1])}" ---------------------------------------- (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: a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 Tuples: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 S tuples: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 K tuples:none Defined Rule Symbols: a_1 Defined Pair Symbols: A_1 Compound Symbols: c1_1, c2 ---------------------------------------- (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: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 The (relative) TRS S consists of the following rules: a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 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: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 The (relative) TRS S consists of the following rules: a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (12) Obligation: Innermost TRS: Rules: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 Types: A :: b:c -> c1:c2 b :: b:c -> b:c c1 :: c1:c2 -> c1:c2 c :: b:c -> b:c c2 :: c1:c2 a :: b:c -> b:c hole_c1:c21_3 :: c1:c2 hole_b:c2_3 :: b:c gen_c1:c23_3 :: Nat -> c1:c2 gen_b:c4_3 :: Nat -> b:c ---------------------------------------- (13) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: A, a ---------------------------------------- (14) Obligation: Innermost TRS: Rules: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 Types: A :: b:c -> c1:c2 b :: b:c -> b:c c1 :: c1:c2 -> c1:c2 c :: b:c -> b:c c2 :: c1:c2 a :: b:c -> b:c hole_c1:c21_3 :: c1:c2 hole_b:c2_3 :: b:c gen_c1:c23_3 :: Nat -> c1:c2 gen_b:c4_3 :: Nat -> b:c Generator Equations: gen_c1:c23_3(0) <=> c2 gen_c1:c23_3(+(x, 1)) <=> c1(gen_c1:c23_3(x)) gen_b:c4_3(0) <=> hole_b:c2_3 gen_b:c4_3(+(x, 1)) <=> b(gen_b:c4_3(x)) The following defined symbols remain to be analysed: A, a ---------------------------------------- (15) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: A(gen_b:c4_3(+(1, n6_3))) -> *5_3, rt in Omega(n6_3) Induction Base: A(gen_b:c4_3(+(1, 0))) Induction Step: A(gen_b:c4_3(+(1, +(n6_3, 1)))) ->_R^Omega(1) c1(A(gen_b:c4_3(+(1, n6_3)))) ->_IH c1(*5_3) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (16) Complex Obligation (BEST) ---------------------------------------- (17) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 Types: A :: b:c -> c1:c2 b :: b:c -> b:c c1 :: c1:c2 -> c1:c2 c :: b:c -> b:c c2 :: c1:c2 a :: b:c -> b:c hole_c1:c21_3 :: c1:c2 hole_b:c2_3 :: b:c gen_c1:c23_3 :: Nat -> c1:c2 gen_b:c4_3 :: Nat -> b:c Generator Equations: gen_c1:c23_3(0) <=> c2 gen_c1:c23_3(+(x, 1)) <=> c1(gen_c1:c23_3(x)) gen_b:c4_3(0) <=> hole_b:c2_3 gen_b:c4_3(+(x, 1)) <=> b(gen_b:c4_3(x)) The following defined symbols remain to be analysed: A, a ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (20) Obligation: Innermost TRS: Rules: A(b(z0)) -> c1(A(z0)) A(c(z0)) -> c2 a(b(z0)) -> b(a(z0)) a(c(z0)) -> z0 Types: A :: b:c -> c1:c2 b :: b:c -> b:c c1 :: c1:c2 -> c1:c2 c :: b:c -> b:c c2 :: c1:c2 a :: b:c -> b:c hole_c1:c21_3 :: c1:c2 hole_b:c2_3 :: b:c gen_c1:c23_3 :: Nat -> c1:c2 gen_b:c4_3 :: Nat -> b:c Lemmas: A(gen_b:c4_3(+(1, n6_3))) -> *5_3, rt in Omega(n6_3) Generator Equations: gen_c1:c23_3(0) <=> c2 gen_c1:c23_3(+(x, 1)) <=> c1(gen_c1:c23_3(x)) gen_b:c4_3(0) <=> hole_b:c2_3 gen_b:c4_3(+(x, 1)) <=> b(gen_b:c4_3(x)) The following defined symbols remain to be analysed: a ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: a(gen_b:c4_3(+(1, n303_3))) -> *5_3, rt in Omega(0) Induction Base: a(gen_b:c4_3(+(1, 0))) Induction Step: a(gen_b:c4_3(+(1, +(n303_3, 1)))) ->_R^Omega(0) b(a(gen_b:c4_3(+(1, n303_3)))) ->_IH b(*5_3) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (22) BOUNDS(1, INF)