Totality of resolving theorems

ink

theorem Resolve_total {α : Type} (F : Factory α) (d : Doc) (c : ℕ) (i : ℕ) : ∃ ms, Resolve F d c i ms

The totality of resolving (Page 19, Section 5.6)

ink

theorem ResolveConcatOne_total {α : Type} (F : Factory α) (d : Doc) (m : Meas) (i : ℕ) : ∃ msr, ResolveConcatOne F d m i msr

ink

theorem ResolveConcat_total {α : Type} (F : Factory α) (ms : List Meas) (d : Doc) (i : ℕ) (h_non_empty : ms ≠ []) : ∃ msr, ResolveConcat F ms d i msr