postAtTick

formal source

 208variable [DecidableEq E]
 209
 210/-- Event at a given tick (index into the order), if any. -/
 211def postAtTick (σ : Schedule E) (n : ℕ) : Option E :=
 212  (σ.order.get? n)
 213
 214end Schedule
 215
 216/-- Existence of a one‑per‑tick schedule (finite history version). -/
 217theorem exists_sequential_schedule
 218    (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
 219    (wf : WellFounded prec) (H : Finset E) :
 220    ∃ σ : Schedule E,
 221      σ.order.Pairwise (· ≠ ·) ∧
 222      σ.order.toFinset = H ∧
 223      (∀ {e₁ e₂}, e₁ ∈ H → e₂ ∈ H → prec e₁ e₂ →
 224        σ.order.indexOf e₁ < σ.order.indexOf e₂) := by
 225  classical
 226  refine ⟨⟨topoSort (E:=E) prec wf H, ?_⟩, ?_, ?_, ?_⟩
 227  · exact (topoSort_perm (E:=E) prec wf H).1
 228  · exact (topoSort_perm (E:=E) prec wf H).2
 229  · intro e₁ e₂ h₁ h₂ h12; exact topoSort_respects (E:=E) prec wf H h₁ h₂ h12
 230
 231/-- Generic preservation: if conservation holds initially and is preserved
 232    by single postings, then conservation holds along any sequential schedule
 233    for a finite history. -/
 234theorem sequential_preserves_conservation
 235    {S : Type _} (Conservation : S → Prop) (post : S → E → S)
 236    (prec : Precedence E)
 237    [DecidableRel prec] [DecidableEq E]
 238    (H : Finset E) (σ : Schedule E)
 239    (hcover : σ.order.toFinset = H)
 240    (s0 : S)
 241    (h0 : Conservation s0)