Theorems about weak-fairness.

theorem TLA.wf_as_leads_to {σ : Type u} {a : action σ} : (𝒲ℱ a) =tla= (□Enabled a ↝ ⟨ a ⟩)

theorem TLA.wf_alt1 {σ : Type u} {a : action σ} : (𝒲ℱ a) =tla= (□◇(¬Enabled a ∨ □◇⟨ a ⟩))

theorem TLA.wf_alt1' {σ : Type u} {a : action σ} : (𝒲ℱ a) =tla= (□◇(¬Enabled a ∨ ⟨ a ⟩))

theorem TLA.wf1 {σ : Type u} (p q : pred σ) (next a : action σ) : ((p ∧ ⟨ next ⟩ ⇒ ◯p ∨ ◯q) ∧ (p ∧ ⟨ next ⟩ ∧ ⟨ a ⟩ ⇒ ◯q) ∧ (p ⇒ Enabled a ∨ q) ∧ □⟨ next ⟩ ∧ 𝒲ℱ a) |-tla- (p ↝ q)

A useful rule for proving ↝. Compared with its original presentation in the paper "The Temporal Logic of Actions", the following version contains some changes to make it hopefully more practical.

theorem TLA.wf1_original {σ : Type u} (p q : pred σ) (next a : action σ) : ((p ∧ ⟨ next ⟩ ⇒ ◯(p ∨ q)) ∧ (p ∧ ⟨ next ⟩ ∧ ⟨ a ⟩ ⇒ ◯q) ∧ (p ⇒ Enabled a)) |-tla- (□⟨ next ⟩ ∧ 𝒲ℱ a → p ↝ q)

A (relatively) original presentation of the wf1 rule.