Main derivation
S01 · definition
Before
f(n)=3n^2+5n+2,\ g(n)=n^2,\ h(n)=n
After
f(n)>0,\ g(n)\ge 0,\ h(n)\ge 0\ \text{for all}\ n\ge 0Conditions: n\in\mathbb{N}
Rule: def_intro · Uses: G1, G2, G3
Leaf basis: def_intro + square_nonneg + order_basics
Name the three functions and confirm the nonnegativity the MKO requires: for n≥0, n²≥0, so 3n²≥0 and 5n≥0, and adding 2>0 gives f(n)>0; g(n)=n²≥0; h(n)=n≥0. The cost model and input size were declared with f (G2), and only functions under this declaration are compared.
S02 · equivalent
Before
f\in O(g)
After
\exists c>0\ \exists N\in\mathbb{N}\ \forall n\ge N,\ f(n)\le c\,g(n)Conditions: none
Rule: def_unfold · Uses: S01, mko_asymptotic_def
Leaf basis: def_unfold + mko_asymptotic_def
Unfold the definition of big O: find a witness pair (c,N) such that the whole tail from N on satisfies f(n)≤c·g(n). The quantifier order is 'there exist c and N such that for all n': c and N may not depend on n. The definition of Ω replaces ≤ by ≥, and Θ requires both.
S03 · theorem_application
Before
n\in\mathbb{N},\ n\ge 1After
1\le n\le n^2
Conditions: n\ge 1
Rule: L_n_le_nsq · Uses: G1
Leaf basis: order_basics + distributive
Apply Lemma L_n_le_nsq (proved in S03.1 and S03.2): for n≥1, 1≤n≤n². This lets the lower-order term 5n and the constant 2 be controlled by n².
S04 · implies
Before
n\le n^2,\ 1\le n^2\ (n\ge 1)
After
5n\le 5n^2,\ 2\le 2n^2\ (n\ge 1)
Conditions: n\ge 1; 5>0,\ 2>0
Rule: order_basics · Uses: S03
Leaf basis: order_basics
Multiply both sides of n≤n² by the positive number 5, and both sides of 1≤n² by the positive number 2; multiplying by a positive number preserves the direction of an inequality.
S05 · implies
Before
f(n)=3n^2+5n+2
After
f(n)\le 3n^2+5n^2+2n^2=10n^2\quad(n\ge 1)
Conditions: n\ge 1
Rule: order_basics · Uses: S04
Leaf basis: order_basics + distributive + add_assoc
Add the two inequalities of S04 to 3n²=3n² (inequalities in the same direction add), giving f(n)≤10n² for every n≥1. Equivalently, 10n²−f(n)=5n(n−1)+2(n²−1), and both terms are nonnegative for n≥1 (N1 checks this as a polynomial identity).
S06 · implies
Before
\forall n\ge 1,\ f(n)\le 10\,g(n)
After
f\in O(g)\ \text{with witness}\ (c,N)=(10,1)Conditions: 10>0
Rule: exists_intro · Uses: S05, S02
Leaf basis: exists_intro + forall_intro
S05 was proved for an arbitrary n≥1 with no extra assumption, so by generalization it holds on the whole tail n≥1. Take c=10>0 and N=1; by ∃-introduction and the equivalence of S02, f∈O(g).
S07 · implies
Before
n=0
After
f(0)=2>0=c\cdot g(0)\ \text{for every}\ c>0Conditions: none
Rule: numeric_evaluation · Uses: G2, G3
Leaf basis: numeric_evaluation + mul_zero
The role of the threshold: f(0)=2 while g(0)=0, so f(0)>c·g(0) for every c>0. Hence no O witness with threshold N=0 exists; N=1 excludes this finite prefix. This is what the MKO means by finite prefixes being absorbed into the witness.
S08 · implies
Before
f(n)-3g(n)=5n+2
After
f(n)\ge 3\,g(n)\ \forall n\ge 0\ \Rightarrow\ f\in\Omega(g)\ \text{with}\ (c,N)=(3,0)Conditions: n\ge 0
Rule: exists_intro · Uses: S01, mko_asymptotic_def
Leaf basis: exists_intro + order_basics + def_unfold
Unfold Ω: we need c>0 and N with f(n)≥c·g(n) for n≥N. Compute f(n)−3n²=5n+2, which is at least 2>0 for n≥0, so f(n)≥3g(n) for all n≥0. Taking c=3 and N=0 gives f∈Ω(g). The lower-bound witness can start at 0 because g(0)=0 is no obstacle.
S09 · implies
Before
f\in O(g),\ f\in\Omega(g)
After
f\in\Theta(g)=\Theta(n^2)
Conditions: none
Rule: and_intro_elim · Uses: S06, S08, mko_asymptotic_def
Leaf basis: and_intro_elim + mko_asymptotic_def
By the MKO definition, Θ requires both O and Ω. These were proved in S06 and S08, so f∈Θ(n²). The two witnesses need not coincide: the upper bound uses (10,1) and the lower bound uses (3,0).
S10 · implies
Before
4n^2-f(n)=n^2-5n-2=n(n-5)-2
After
n\ge 6\Rightarrow 4n^2-f(n)\ge 4>0;\quad n=5:\ f(5)=102>100=4\cdot 25
Conditions: n\ge 6
Rule: exists_intro · Uses: S02
Leaf basis: exists_intro + order_basics + distributive
Another witness: c=4, N=6. 4n²−f(n)=n²−5n−2=n(n−5)−2 (N4 checks the identity). Sub-step S10.1 proves it is at least 4 for n≥6. So (4,6) is also an O witness. But at n=5, f(5)=102>100: a smaller c needs a larger N. Witnesses are not unique, and finitely many exceptions are absorbed by N.
S11 · implies
Before
f(n)-3n^2=5n+2>0\ \forall n
After
\neg\exists N\ \forall n\ge N,\ f(n)\le 3\,g(n)
Conditions: none
Rule: quantifier_negation · Uses: S08
Leaf basis: quantifier_negation + order_basics
For every n, f(n)−3n²=5n+2≥2>0, so f(n)≤3g(n) never holds. However large N is, n=N is a counterexample, so c=3 cannot serve as the O constant. The definition asks for some c, not every c; constant factors are absorbed into the witness, but not arbitrarily small ones.
S12 · implies
Before
\text{assume}\ \exists c>0\ \exists N\ \forall n\ge N,\ f(n)\le c\,nAfter
\text{contradiction, so}\ f\notin O(h)Conditions: none
Rule: contradiction · Uses: S02, G3
Leaf basis: contradiction + archimedean + order_basics
By contradiction: suppose a witness (c,N) gives f(n)≤c·n for n≥N. S12.1 constructs an n with n≥N and n>c; S12.2 shows this n satisfies f(n)>c·n, contradicting the assumption. So no witness exists and f∉O(n).
S13 · implies
Before
f(n)\ge 5n\ge n\ (n\ge 0),\ f\notin O(h)
After
f\in\Omega(n),\ f\notin O(n),\ f\notin\Theta(n)
Conditions: none
Rule: and_intro_elim · Uses: S12, S01, mko_asymptotic_def
Leaf basis: and_intro_elim + exists_intro + order_basics
For n≥0, f(n)=3n²+5n+2≥5n≥n, so (c,N)=(1,0) is an Ω(n) witness and f∈Ω(n). But S12 showed f∉O(n). Θ(n) needs both, so f∉Θ(n). This shows that O, Ω and Θ are not interchangeable: the same f has n as a lower bound but not as an upper bound.
Substeps and lemmas
S03.1 · implies
Before
n\ge 1
After
n^2-n=n(n-1)\ge 0,\ \text{so}\ n\le n^2Conditions: n\ge 1
Rule: order_basics · Uses: order_basics, distributive
Leaf basis: order_basics + distributive + add_inverse
n≥1 gives n−1≥0 and n≥0. The product of two nonnegative numbers is nonnegative (multiply 0≤n−1 by n≥0), so n(n−1)≥0. By distributivity n(n−1)=n²−n, so n²−n≥0, and adding n to both sides gives n≤n².
S03.2 · implies
Before
1\le n,\ n\le n^2
After
1\le n\le n^2
Conditions: none
Rule: order_basics · Uses: S03.1, order_basics
Leaf basis: order_basics
Chain the hypothesis 1≤n with n≤n² from S03.1; transitivity gives 1≤n≤n², in particular 1≤n². S03.1 and S03.2 together prove L_n_le_nsq.
S10.1 · implies
Before
n\ge 6
After
n-5\ge 1,\ n(n-5)\ge n\ge 6,\ n(n-5)-2\ge 4
Conditions: n\ge 6
Rule: order_basics · Uses: order_basics
Leaf basis: order_basics
n≥6 gives n−5≥1. Multiplying n−5≥1 by the positive number n gives n(n−5)≥n≥6. Subtracting 2 gives n(n−5)−2≥4>0.
S12.1 · implies
Before
c>0,\ N\in\mathbb{N}After
n=\max(n_0,N,1)\ \text{with}\ n_0>c:\ n\ge N,\ n>c,\ n\ge 1Conditions: none
Rule: archimedean · Uses: archimedean
Leaf basis: archimedean + order_basics
By the Archimedean property there is a natural number n0>c. Let n=max(n0,N,1); then n≥N, n≥n0>c, and n≥1>0.
S12.2 · implies
Before
n>c,\ n\ge 1
After
f(n)\ge 3n^2\ge n^2=n\cdot n>c\cdot n
Conditions: none
Rule: order_basics · Uses: S12.1, S03, order_basics
Leaf basis: order_basics + square_nonneg
f(n)=3n²+5n+2≥3n²≥n² (since 5n+2≥0 and 2n²≥0). Multiplying c<n by the positive number n gives c·n<n·n=n². Chaining, f(n)>c·n. But n≥N, so the assumption gives f(n)≤c·n, a contradiction.