Lemmas for the informal proof of time complexity of $Π_e$

ink

theorem Resolve_bound : ∀ {α : Type} {ms : List Meas} {F : Factory α} {d : Doc} {c i : ℕ} {h_not_empty : ms ≠ []}, Resolve F d c i (MeasureSet.set ms h_not_empty) → List.length ms ≤ F.W + 1

A measure set from resolving will have size at most $W_\mathcal{F} + 1$ (Lemma 5.9)

ink

theorem Resolve_exceeding_tainted : ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : MeasureSet}, Resolve F d c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

If resolving happens at a printing context that exceeds $W_\mathcal{F}$, the result will always be tainted (Lemma 5.10)