Validity theorems

ink

theorem Resolve_valid : ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : List Meas} {h : ms ≠ []} {D : List Doc} {m : Meas}, Resolve F d c i (MeasureSet.set ms h) → Widen d D → m ∈ ms → ∃ d_choiceless, d_choiceless ∈ D ∧ MeasRender F d_choiceless c i m

The validity theorem for non-tainted result (the first part of Theorem 5.8)

ink

theorem ResolveConcat_valid : ∀ {α : Type} {F : Factory α} {ms : List Meas} {d₂ : Doc} {i : ℕ} {ms_r : List Meas} {h_non_empty_r : ms_r ≠ []} {d₁ : Doc} {L₁ L₂ : List Doc} {c : ℕ} {orig_ms : List Meas} {h_non_empty : orig_ms ≠ []} (m : Meas), ResolveConcat F ms d₂ i (MeasureSet.set ms_r h_non_empty_r) → Widen d₁ L₁ → Widen d₂ L₂ → Resolve F d₁ c i (MeasureSet.set orig_ms h_non_empty) → (∀ (x : Meas), x ∈ ms → x ∈ orig_ms) → m ∈ ms_r → ∃ d_choiceless, d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂) L₁) ∧ MeasRender F d_choiceless c i m

ink

theorem Resolve_tainted_valid : ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {m : Meas} {D : List Doc}, Resolve F d c i (MeasureSet.tainted m) → Widen d D → ∃ d_choiceless, d_choiceless ∈ D ∧ MeasRender F d_choiceless c i m

The validity theorem for tainted result (the second part of Theorem 5.8)

ink

theorem ResolveConcat_tainted_valid : ∀ {α : Type} {F : Factory α} {ms : List Meas} {d₂ : Doc} {i : ℕ} {m : Meas} {d₁ : Doc} {L₁ L₂ : List Doc} {c : ℕ} {orig_ms : List Meas} {h_non_empty : orig_ms ≠ []}, ResolveConcat F ms d₂ i (MeasureSet.tainted m) → Widen d₁ L₁ → Widen d₂ L₂ → Resolve F d₁ c i (MeasureSet.set orig_ms h_non_empty) → (∀ (x : Meas), x ∈ ms → x ∈ orig_ms) → ∃ d_choiceless, d_choiceless ∈ List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂) L₁) ∧ MeasRender F d_choiceless c i m