Theorem: FOL.NV.T_17_7 (FOL/NV/Margaris/Fol.lean)

State before:
F : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ F
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
⊢ IsDeduct Δ (forall_ v F)
Tactic:
induction h1
State after:
case axiom_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ (forall_ v phi✝)

case assume_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ : Formula
a✝ : phi✝ ∈ Δ
⊢ IsDeduct Δ (forall_ v phi✝)

case mp_
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ phi✝
a_ih✝¹ : IsDeduct Δ (forall_ v (phi✝.imp_ psi✝))
a_ih✝ : IsDeduct Δ (forall_ v phi✝)
⊢ IsDeduct Δ (forall_ v psi✝)

State before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
case axiom_ h1_phi h1_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.gen_
  exact h1_1
State after:
no goals

State before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (forall_ v h1_phi)

State before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (forall_ v h1_phi)
Tactic:
apply IsAxiom.gen_
State after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi

State before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
State after:
no goals

State before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
apply IsDeduct.mp_ h1_phi
State after:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (forall_ v h1_phi))

case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi

State before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (forall_ v h1_phi))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (forall_ v h1_phi))

State before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (forall_ v h1_phi))
Tactic:
apply IsAxiom.pred_3_
State after:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ ¬isFreeIn v h1_phi

State before:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ ¬isFreeIn v h1_phi
Tactic:
exact h2 h1_phi h1_1
State after:
no goals

State before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.assume_
State after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ

State before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Tactic:
exact h1_1
State after:
no goals

State before:
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v h1_psi)
Tactic:
apply IsDeduct.mp_ (forall_ v h1_phi)
State after:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v h1_phi).imp_ (forall_ v h1_psi))

case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v h1_phi)

State before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v h1_phi).imp_ (forall_ v h1_psi))
Tactic:
apply IsDeduct.mp_ (forall_ v (h1_phi.imp_ h1_psi))
State after:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))

case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))

State before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsAxiom ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))

State before:
case a.a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsAxiom ((forall_ v (h1_phi.imp_ h1_psi)).imp_ ((forall_ v h1_phi).imp_ (forall_ v h1_psi)))
Tactic:
apply IsAxiom.pred_1_
State after:
no goals

State before:
case a.a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
Tactic:
exact h1_ih_1
State after:
no goals

State before:
case a
F : Formula
v : VarName
Δ : Set Formula
h2 : ∀ H ∈ Δ, ¬isFreeIn v H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct Δ (forall_ v (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (forall_ v h1_phi)
⊢ IsDeduct Δ (forall_ v h1_phi)
Tactic:
exact h1_ih_2
State after:
no goals