Various lemmas about domination

ink

theorem dominates_refl {α : Type} {m : Meas} (F : Factory α) : dominates F m m = true

ink

theorem dominates_trans {α : Type} {m₁ : Meas} {m₂ : Meas} {m₃ : Meas} {F : Factory α} (h : dominates F m₁ m₂ = true) (h' : dominates F m₂ m₃ = true) : dominates F m₁ m₃ = true

ink

inductive FourCases {α : Type} (F : Factory α) (m₁ : Meas) (m₂ : Meas) : Prop

• first_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, dominates F m₁ m₂ = true → FourCases F m₁ m₂
• second_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, ¬dominates F m₁ m₂ = true → dominates F m₂ m₁ = true → FourCases F m₁ m₂
• first_last: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, ¬dominates F m₁ m₂ = true → ¬dominates F m₂ m₁ = true → m₁.last > m₂.last → FourCases F m₁ m₂
• second_last: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, ¬dominates F m₁ m₂ = true → ¬dominates F m₂ m₁ = true → m₂.last > m₁.last → FourCases F m₁ m₂

ink

theorem four_cases {α : Type} (F : Factory α) (m₁ : Meas) (m₂ : Meas) : FourCases F m₁ m₂

In the merge operation, there are four possible cases based on domination of two measures. This lemma creates an exhaustive case analysis for these four cases.