Basic theorems about TLA.

theorem TLA.dual_lemma {σ : Type u} (p q : pred σ) : (¬p) =tla= (¬q) → p = q

theorem TLA.pred_eq_iff_iff {σ : Type u} (p q : pred σ) : p = q ↔ (p) |-tla- (q) ∧ (q) |-tla- (p)

theorem TLA.impl_intro {σ : Type u} (p q : pred σ) : |-tla- (p → q) = (p) |-tla- (q)

theorem TLA.impl_decouple {σ : Type u} (p q : pred σ) : |-tla- (p → q) → |-tla- (p) → |-tla- (q)

theorem TLA.and_pred_implies_split {σ : Type u} (Γ p q : pred σ) : (Γ) |-tla- (p ∧ q) = ((Γ) |-tla- (p) ∧ (Γ) |-tla- (q))

theorem TLA.valid_eq_true_implies {σ : Type u} (p : pred σ) : |-tla- (p) = (⊤) |-tla- (p)

theorem TLA.and_valid_split {σ : Type u} (p q : pred σ) : |-tla- (p ∧ q) = (|-tla- (p) ∧ |-tla- (q))

theorem TLA.impl_intro_add_r {σ : Type u} (p q r : pred σ) : (r) |-tla- (p → q) = (r ∧ p) |-tla- (q)

theorem TLA.impl_drop_hyp {σ : Type u} (p q : pred σ) : |-tla- (q) → (p) |-tla- (q)

theorem TLA.impl_drop_hyp_one_r {σ : Type u} (p q r : pred σ) : (p) |-tla- (q) → (p ∧ r) |-tla- (q)

theorem TLA.and_true {σ : Type u} (p : pred σ) : (p ∧ ⊤) =tla= (p)

theorem TLA.true_and {σ : Type u} (p : pred σ) : (⊤ ∧ p) =tla= (p)

theorem TLA.or_false {σ : Type u} (p : pred σ) : (p ∨ ⊥) =tla= (p)

theorem TLA.false_or {σ : Type u} (p : pred σ) : (⊥ ∨ p) =tla= (p)

theorem TLA.imp_true {σ : Type u} (p : pred σ) : (p → ⊤) =tla= (⊤)

theorem TLA.always_true {σ : Type u} : (□⊤) =tla= (⊤)

theorem TLA.eventually_true {σ : Type u} : (◇⊤) =tla= (⊤)

theorem TLA.later_true {σ : Type u} : (◯⊤) =tla= (⊤)

theorem TLA.always_intro {σ : Type u} (p : pred σ) : |-tla- (p) = |-tla- (□p)

theorem TLA.later_always_comm {σ : Type u} (p : pred σ) : (◯□p) =tla= (□◯p)

theorem TLA.always_unroll {σ : Type u} (p : pred σ) : (□p) =tla= (p ∧ ◯□p)

theorem TLA.always_induction {σ : Type u} (p : pred σ) : (□p) =tla= (p ∧ □(p → ◯p))

theorem TLA.always_weaken {σ : Type u} (p : pred σ) : (□p) |-tla- (p)

theorem TLA.always_weaken_to_eventually {σ : Type u} (p : pred σ) : (□p) |-tla- (◇p)

theorem TLA.later_weaken_to_eventually {σ : Type u} (p : pred σ) : (◯p) |-tla- (◇p)

theorem TLA.now_weaken_to_eventually {σ : Type u} (p : pred σ) : (p) |-tla- (◇p)

theorem TLA.not_always {σ : Type u} (p : pred σ) : (¬□p) =tla= (◇¬p)

theorem TLA.not_eventually {σ : Type u} (p : pred σ) : (¬◇p) =tla= (□¬p)

theorem TLA.eventually_to_always {σ : Type u} (p : pred σ) : (◇p) =tla= (¬□¬p)

theorem TLA.always_to_eventually {σ : Type u} (p : pred σ) : (□p) =tla= (¬◇¬p)

theorem TLA.always_idem {σ : Type u} (p : pred σ) : (□□p) =tla= (□p)

theorem TLA.eventually_idem {σ : Type u} (p : pred σ) : (◇◇p) =tla= (◇p)

theorem TLA.always_eventually_always {σ : Type u} (p : pred σ) : (□◇□p) =tla= (◇□p)

theorem TLA.eventually_always_eventually {σ : Type u} (p : pred σ) : (◇□◇p) =tla= (□◇p)

theorem TLA.always_eventually_idem {σ : Type u} (p : pred σ) : (□◇□◇p) =tla= (□◇p)

theorem TLA.eventually_always_idem {σ : Type u} (p : pred σ) : (◇□◇□p) =tla= (◇□p)

theorem TLA.contraposition_for_pred_implies {σ : Type u} (p q : pred σ) : (p) |-tla- (q) = (¬q) |-tla- (¬p)

theorem TLA.proof_by_contra {σ : Type u} (p q : pred σ) : (p) |-tla- (q) = (¬q ∧ p) |-tla- (⊥)

theorem TLA.modus_ponens {σ : Type u} (p q : pred σ) : (p ∧ (p → q)) |-tla- (q)

theorem TLA.modus_ponens_with_premise {σ : Type u} (p q : pred σ) : (p ∧ (p → q)) |-tla- (p ∧ q)

theorem TLA.always_pred_implies {σ : Type u} (p q : pred σ) : (□p) |-tla- (q) = (□p) |-tla- (□q)

theorem TLA.always_and_eventually {σ : Type u} (p q : pred σ) : (◇p ∧ □q) |-tla- (◇(p ∧ q))

theorem TLA.always_and_eventually' {σ : Type u} (p q : pred σ) : (◇p ∧ □q) |-tla- (◇(p ∧ □q))

theorem TLA.later_monotone {σ : Type u} (p q : pred σ) : (p) |-tla- (q) → (◯p) |-tla- (◯q)

theorem TLA.always_monotone {σ : Type u} (p q : pred σ) : (p) |-tla- (q) → (□p) |-tla- (□q)

theorem TLA.eventually_monotone {σ : Type u} (p q : pred σ) : (p) |-tla- (q) → (◇p) |-tla- (◇q)

theorem TLA.always_eventually_monotone {σ : Type u} (p q : pred σ) : (p) |-tla- (q) → (□◇p) |-tla- (□◇q)

theorem TLA.eventually_always_monotone {σ : Type u} (p q : pred σ) : (p) |-tla- (q) → (◇□p) |-tla- (◇□q)

theorem TLA.until_induction {σ : Type u} (p q : pred σ) : (p ∧ □(p ∧ ¬q → ◯p)) |-tla- (□(p ∧ ¬q) ∨ (p 𝑈 p ∧ q))

theorem TLA.later_forall {σ : Type u} {α : Sort v} (p : α → pred σ) : (◯∀ x, (p x)) =tla= (∀ x, ◯(p x))

theorem TLA.later_exists {σ : Type u} {α : Sort v} (p : α → pred σ) : (◯∃ x, (p x)) =tla= (∃ x, ◯(p x))

theorem TLA.always_forall {σ : Type u} {α : Sort v} (p : α → pred σ) : (□∀ x, (p x)) =tla= (∀ x, □(p x))

theorem TLA.eventually_exists {σ : Type u} {α : Sort v} (p : α → pred σ) : (◇∃ x, (p x)) =tla= (∃ x, ◇(p x))

theorem TLA.exists_into_always {σ : Type u} {α : Sort v} (p : α → pred σ) : (∃ x, □(p x)) |-tla- (□∃ x, (p x))

uni-direction, moving ∃ into □

theorem TLA.eventually_into_forall {σ : Type u} {α : Sort v} (p : α → pred σ) : (◇∀ x, (p x)) |-tla- (∀ x, ◇(p x))

uni-direction, moving ◇ into ∀

theorem TLA.later_and {σ : Type u} (p q : pred σ) : (◯(p ∧ q)) =tla= (◯p ∧ ◯q)

theorem TLA.later_or {σ : Type u} (p q : pred σ) : (◯(p ∨ q)) =tla= (◯p ∨ ◯q)

theorem TLA.always_and {σ : Type u} (p q : pred σ) : (□(p ∧ q)) =tla= (□p ∧ □q)

theorem TLA.eventually_or {σ : Type u} (p q : pred σ) : (◇(p ∨ q)) =tla= (◇p ∨ ◇q)

theorem TLA.always_or_merge {σ : Type u} (p q : pred σ) : (□p ∨ □q) |-tla- (□(p ∨ q))

uni-direction, merging the ∨ outside ◇ in

theorem TLA.eventually_and_split {σ : Type u} (p q : pred σ) : (◇(p ∧ q)) |-tla- (◇p ∧ ◇q)

uni-direction, splitting the ∧ inside ◇

theorem TLA.eventually_always_and_distrib {σ : Type u} (p q : pred σ) : (◇□(p ∧ q)) =tla= (◇□p ∧ ◇□q)

theorem TLA.always_eventually_or_distrib {σ : Type u} (p q : pred σ) : (□◇(p ∨ q)) =tla= (□◇p ∨ □◇q)

theorem TLA.forall_elim {α : Type u} {β : Sort v} {p : β → pred α} {Γ : pred α} : (∀ (x : β), (Γ) |-tla- ((p x))) = (Γ) |-tla- (∀ x, (p x))

theorem TLA.exists_elim {α : Type u} {β : Sort v} {p : β → pred α} {Γ : pred α} (x : β) : (Γ) |-tla- ((p x)) → (Γ) |-tla- (∃ x, (p x))

theorem TLA.valid_pure {α : Type u_1} {p : Prop} : p → |-tla- (⌞ p ⌟)

theorem TLA.pred_implies_pure {α : Type u_1} {q : pred α} {p : Prop} : p → (q) |-tla- (⌞ p ⌟)

theorem TLA.pure_fact_intro {α : Type u} {Γ p : pred α} {q : Prop} : (q → (Γ) |-tla- (p)) = (Γ) |-tla- (⌞ q ⌟ → p)

theorem TLA.pure_implies_to_forall {σ✝ : Type u_1} {q : pred σ✝} {p : Prop} : (⌞ p ⌟ → q) =tla= (∀ _x, q)

theorem TLA.pure_and_to_exists {σ✝ : Type u_1} {q : pred σ✝} {p : Prop} : (⌞ p ⌟ ∧ q) =tla= (∃ _x, q)