ink

theorem ResolveConcatOne_pareto : ∀ {α : Type} {F : Factory α} {d : Doc} {m : Meas} {i : ℕ} {msr : List Meas} {h_non_empty : msr ≠ []}, ResolveConcatOne F d m i (MeasureSet.set msr h_non_empty) → pareto F msr

ink

theorem ResolveConcat_pareto : ∀ {α : Type} {F : Factory α} {ms : List Meas} {d : Doc} {i : ℕ} {msr : List Meas} {h_non_empty : msr ≠ []}, ResolveConcat F ms d i (MeasureSet.set msr h_non_empty) → pareto F msr

ink

theorem Resolve_pareto : ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : List Meas} {h_non_empty : ms ≠ []}, Resolve F d c i (MeasureSet.set ms h_non_empty) → pareto F ms