Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
case ax
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case impI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)

case impE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case andI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)

case andE1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case andE2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case orI1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orI2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝

case botC
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
solve_by_elim
Proof state after:
case impI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)

case impE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case andI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)

case andE1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case andE2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case orI1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orI2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝

case botC
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝