ink

theorem merge_first_dom : ∀ {α : Type} {F : Factory α} {m₂ : Meas} {ms₂ : List Meas} {m₁ : Meas} (ms₁ : List Meas), pareto F (m₂ :: ms₂) → dominates F m₁ m₂ = true → ∃ n, merge F (m₁ :: ms₁, m₂ :: ms₂) = m₁ :: merge F (ms₁, List.drop n ms₂) ∧ ∀ (m : Meas), m ∈ List.take n ms₂ → dominates F m₁ m = true

ink

theorem merge_second_dom : ∀ {α : Type} {F : Factory α} {m₁ : Meas} {ms₁ : List Meas} {m₂ : Meas} (ms₂ : List Meas), pareto F (m₁ :: ms₁) → dominates F m₂ m₁ = true → ¬dominates F m₁ m₂ = true → ∃ n, merge F (m₁ :: ms₁, m₂ :: ms₂) = m₂ :: merge F (List.drop n ms₁, ms₂) ∧ ∀ (m : Meas), m ∈ List.take n ms₁ → dominates F m₂ m = true

ink

theorem merge_head_either : ∀ {α : Type} {F : Factory α} {m₁ : Meas} {ms₁ : List Meas} {m₂ : Meas} {ms₂ : List Meas}, pareto F (m₁ :: ms₁) → pareto F (m₂ :: ms₂) → m₁ = List.head (merge F (m₁ :: ms₁, m₂ :: ms₂)) (_ : merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ []) ∨ m₂ = List.head (merge F (m₁ :: ms₁, m₂ :: ms₂)) (_ : merge F (m₁ :: ms₁, m₂ :: ms₂) ≠ [])

ink

theorem merge_preserves_pareto : ∀ {α : Type} {F : Factory α} {ms₁ ms₂ : List Meas}, pareto F ms₁ → pareto F ms₂ → pareto F (merge F (ms₁, ms₂))

ink

theorem merge_pareto_subset : ∀ {α : Type} {m : Meas} {F : Factory α} {ms₁ ms₂ : List Meas}, m ∈ merge F (ms₁, ms₂) → pareto F ms₁ → pareto F ms₂ → m ∈ ms₁ ∨ m ∈ ms₂

ink

theorem merge_dom₁ : ∀ {α : Type} {F : Factory α} {ms₁ ms₂ : List Meas} {m : Meas}, pareto F ms₁ → pareto F ms₂ → m ∈ ms₁ → ∃ m_better, m_better ∈ merge F (ms₁, ms₂) ∧ dominates F m_better m = true

ink

theorem merge_dom₂ : ∀ {α : Type} {F : Factory α} {ms₁ ms₂ : List Meas} {m : Meas}, pareto F ms₁ → pareto F ms₂ → m ∈ ms₂ → ∃ m_better, m_better ∈ merge F (ms₁, ms₂) ∧ dominates F m_better m = true