internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_18_7
Proof state before:
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q'
Tactic:
apply C_18_4 (forall_ u P_u) (forall_ v P_v) Q Q' Δ h2
Proof state after:
case h2
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

case h3
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q
Theorem: FOL.NV.T_18_7
Proof state before:
case h2
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
Tactic:
apply T_18_6 P_u P_v u v h3
Proof state after:
no goals
Theorem: FOL.NV.T_18_7
Proof state before:
case h3
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.similar_not
Proof state before:
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ Similar P_u.not_ P_v.not_ u v
Tactic:
simp only [Similar] at *
Proof state after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u.not_ ∧
    ¬isFreeIn u P_v.not_ ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Theorem: FOL.NV.similar_not
Proof state before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u.not_ ∧
    ¬isFreeIn u P_v.not_ ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [isFreeIn] at *
Proof state after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Theorem: FOL.NV.similar_not
Proof state before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [fastAdmits] at *
Proof state after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u.not_ ∧
        fastAdmitsAux v u ∅ P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Theorem: FOL.NV.similar_not
Proof state before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u.not_ ∧
        fastAdmitsAux v u ∅ P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [fastAdmitsAux] at *
Proof state after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Theorem: FOL.NV.similar_not
Proof state before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [fastReplaceFree] at *
Proof state after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = (fastReplaceFree u v P_u).not_ ∧ P_u.not_ = (fastReplaceFree v u P_v).not_
Theorem: FOL.NV.similar_not
Proof state before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = (fastReplaceFree u v P_u).not_ ∧ P_u.not_ = (fastReplaceFree v u P_v).not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.T_18_8
Proof state before:
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsProof ((exists_ u P_u).iff_ (exists_ v P_v))
Tactic:
simp only [def_exists_]
Proof state after:
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u.not_).not_.iff_ (forall_ v P_v.not_).not_)
Theorem: FOL.NV.T_18_8
Proof state before:
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u.not_).not_.iff_ (forall_ v P_v.not_).not_)
Tactic:
apply IsDeduct.mp_ ((forall_ u P_u.not_).iff_ (forall_ v P_v.not_))
Proof state after:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅
    (((forall_ u P_u.not_).iff_ (forall_ v P_v.not_)).imp_ ((forall_ u P_u.not_).not_.iff_ (forall_ v P_v.not_).not_))

case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅ ((forall_ u P_u.not_).iff_ (forall_ v P_v.not_))
Theorem: FOL.NV.T_18_8
Proof state before:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅
    (((forall_ u P_u.not_).iff_ (forall_ v P_v.not_)).imp_ ((forall_ u P_u.not_).not_.iff_ (forall_ v P_v.not_).not_))
Tactic:
simp only [def_iff_]
Proof state after:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅
    ((((forall_ u P_u.not_).imp_ (forall_ v P_v.not_)).and_ ((forall_ v P_v.not_).imp_ (forall_ u P_u.not_))).imp_
      (((forall_ u P_u.not_).not_.imp_ (forall_ v P_v.not_).not_).and_
        ((forall_ v P_v.not_).not_.imp_ (forall_ u P_u.not_).not_)))
Theorem: FOL.NV.T_18_8
Proof state before:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅
    ((((forall_ u P_u.not_).imp_ (forall_ v P_v.not_)).and_ ((forall_ v P_v.not_).imp_ (forall_ u P_u.not_))).imp_
      (((forall_ u P_u.not_).not_.imp_ (forall_ v P_v.not_).not_).and_
        ((forall_ v P_v.not_).not_.imp_ (forall_ u P_u.not_).not_)))
Tactic:
simp only [def_and_]
Proof state after:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅
    ((((forall_ u P_u.not_).imp_ (forall_ v P_v.not_)).imp_
            ((forall_ v P_v.not_).imp_ (forall_ u P_u.not_)).not_).not_.imp_
      (((forall_ u P_u.not_).not_.imp_ (forall_ v P_v.not_).not_).imp_
          ((forall_ v P_v.not_).not_.imp_ (forall_ u P_u.not_).not_).not_).not_)
Theorem: FOL.NV.T_18_8
Proof state before:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅
    ((((forall_ u P_u.not_).imp_ (forall_ v P_v.not_)).imp_
            ((forall_ v P_v.not_).imp_ (forall_ u P_u.not_)).not_).not_.imp_
      (((forall_ u P_u.not_).not_.imp_ (forall_ v P_v.not_).not_).imp_
          ((forall_ v P_v.not_).not_.imp_ (forall_ u P_u.not_).not_).not_).not_)
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_8
Proof state before:
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅ ((forall_ u P_u.not_).iff_ (forall_ v P_v.not_))
Tactic:
apply T_18_6
Proof state after:
case a.h1
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ Similar P_u.not_ P_v.not_ u v
Theorem: FOL.NV.T_18_8
Proof state before:
case a.h1
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ Similar P_u.not_ P_v.not_ u v
Tactic:
exact similar_not P_u P_v u v h1
Proof state after:
no goals
Theorem: FOL.NV.T18_9
Proof state before:
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q'
Tactic:
apply C_18_4 (exists_ u P_u) (exists_ v P_v) Q Q' Δ h2
Proof state after:
case h2
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((exists_ u P_u).iff_ (exists_ v P_v))

case h3
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q
Theorem: FOL.NV.T18_9
Proof state before:
case h2
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((exists_ u P_u).iff_ (exists_ v P_v))
Tactic:
exact T_18_8 P_u P_v u v h3
Proof state after:
no goals
Theorem: FOL.NV.T18_9
Proof state before:
case h3
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_19_1
Proof state before:
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v P).iff_ P)
Tactic:
apply IsDeduct.mp_ ((forall_ v P).imp_ P)
Proof state after:
case a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ (((forall_ v P).imp_ P).imp_ ((forall_ v P).iff_ P))

case a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v P).imp_ P)
Theorem: FOL.NV.T_19_1
Proof state before:
case a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ (((forall_ v P).imp_ P).imp_ ((forall_ v P).iff_ P))
Tactic:
apply IsDeduct.mp_ (P.imp_ (forall_ v P))
Proof state after:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((P.imp_ (forall_ v P)).imp_ (((forall_ v P).imp_ P).imp_ ((forall_ v P).iff_ P)))

case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ (P.imp_ (forall_ v P))
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((P.imp_ (forall_ v P)).imp_ (((forall_ v P).imp_ P).imp_ ((forall_ v P).iff_ P)))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    ((P.imp_ (forall_ v P)).imp_ (((forall_ v P).imp_ P).imp_ (((forall_ v P).imp_ P).and_ (P.imp_ (forall_ v P)))))
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    ((P.imp_ (forall_ v P)).imp_ (((forall_ v P).imp_ P).imp_ (((forall_ v P).imp_ P).and_ (P.imp_ (forall_ v P)))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    ((P.imp_ (forall_ v P)).imp_
      (((forall_ v P).imp_ P).imp_ (((forall_ v P).imp_ P).imp_ (P.imp_ (forall_ v P)).not_).not_))
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    ((P.imp_ (forall_ v P)).imp_
      (((forall_ v P).imp_ P).imp_ (((forall_ v P).imp_ P).imp_ (P.imp_ (forall_ v P)).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ (P.imp_ (forall_ v P))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom (P.imp_ (forall_ v P))
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom (P.imp_ (forall_ v P))
Tactic:
exact IsAxiom.pred_3_ v P h1
Proof state after:
no goals
Theorem: FOL.NV.T_19_1
Proof state before:
case a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v P).imp_ P)
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom ((forall_ v P).imp_ P)
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom ((forall_ v P).imp_ P)
Tactic:
apply IsAxiom.pred_2_ v v P P
Proof state after:
case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ fastAdmits v v P

case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ fastReplaceFree v v P = P
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ fastAdmits v v P
Tactic:
apply fastAdmits_self
Proof state after:
no goals
Theorem: FOL.NV.T_19_1
Proof state before:
case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ fastReplaceFree v v P = P
Tactic:
apply fastReplaceFree_self
Proof state after:
no goals
Theorem: FOL.NV.T_19_2
Proof state before:
P : Formula
u v : VarName
⊢ IsProof ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P)))
Tactic:
apply IsDeduct.mp_ ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))
Proof state after:
case a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
      ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P))))

case a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))
Theorem: FOL.NV.T_19_2
Proof state before:
case a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
      ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P))))
Tactic:
apply IsDeduct.mp_ ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P)))
Proof state after:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P)))))

case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P)))
Theorem: FOL.NV.T_19_2
Proof state before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P)))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).and_
          ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))))))
Theorem: FOL.NV.T_19_2
Proof state before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).and_
          ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
            ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).not_).not_))
Theorem: FOL.NV.T_19_2
Proof state before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
            ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_2
Proof state before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P)))
Tactic:
apply T_17_10
Proof state after:
no goals
Theorem: FOL.NV.T_19_2
Proof state before:
case a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))
Tactic:
apply T_17_10
Proof state after:
no goals
Theorem: FOL.NV.T_19_3
Proof state before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P.not_).iff_ (exists_ v P).not_)
Tactic:
simp only [def_exists_]
Proof state after:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P.not_).iff_ (forall_ v P.not_).not_.not_)
Theorem: FOL.NV.T_19_3
Proof state before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P.not_).iff_ (forall_ v P.not_).not_.not_)
Tactic:
simp only [def_iff_]
Proof state after:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).and_ ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)))
Theorem: FOL.NV.T_19_3
Proof state before:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).and_ ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)))
Tactic:
simp only [def_and_]
Proof state after:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).imp_
        ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)).not_).not_
Theorem: FOL.NV.T_19_3
Proof state before:
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).imp_
        ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)).not_).not_
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_4
Proof state before:
P : Formula
u v : VarName
⊢ IsProof ((exists_ u (forall_ v P)).imp_ (forall_ v (exists_ u P)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {exists_ u (forall_ v P)}) (forall_ v (exists_ u P))
Theorem: FOL.NV.T_19_4
Proof state before:
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {exists_ u (forall_ v P)}) (forall_ v (exists_ u P))
Tactic:
simp
Proof state after:
case h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (forall_ v (exists_ u P))
Theorem: FOL.NV.T_19_4
Proof state before:
case h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (forall_ v (exists_ u P))
Tactic:
apply generalization
Proof state after:
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u P)

case h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn v H
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u P)
Tactic:
apply rule_C (forall_ v P) (exists_ u P) u {exists_ u (forall_ v P)}
Proof state after:
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u (forall_ v P))

case h1.h1.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (exists_ u P)

case h1.h1.h3
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn u H

case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u P)
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (exists_ u (forall_ v P))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.a
P : Formula
u v : VarName
⊢ exists_ u (forall_ v P) ∈ {exists_ u (forall_ v P)}
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h1.a
P : Formula
u v : VarName
⊢ exists_ u (forall_ v P) ∈ {exists_ u (forall_ v P)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (exists_ u P)
Tactic:
apply exists_intro P u u
Proof state after:
case h1.h1.h2.h1
P : Formula
u v : VarName
⊢ fastAdmits u u P

case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (fastReplaceFree u u P)
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h2.h1
P : Formula
u v : VarName
⊢ fastAdmits u u P
Tactic:
apply fastAdmits_self
Proof state after:
no goals
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (fastReplaceFree u u P)
Tactic:
simp only [fastReplaceFree_self]
Proof state after:
case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) P
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h2.h2
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) P
Tactic:
apply specId v
Proof state after:
case h1.h1.h2.h2.h1
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (forall_ v P)
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h2.h2.h1
P : Formula
u v : VarName
⊢ IsDeduct ({exists_ u (forall_ v P)} ∪ {forall_ v P}) (forall_ v P)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h2.h2.h1.a
P : Formula
u v : VarName
⊢ forall_ v P ∈ {exists_ u (forall_ v P)} ∪ {forall_ v P}
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h2.h2.h1.a
P : Formula
u v : VarName
⊢ forall_ v P ∈ {exists_ u (forall_ v P)} ∪ {forall_ v P}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn u H
Tactic:
simp
Proof state after:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u (forall_ v P))
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u (forall_ v P))
Tactic:
simp only [def_exists_]
Proof state after:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u (forall_ v P).not_).not_
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u (forall_ v P).not_).not_
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬(¬True ∧ ¬u = v ∧ isFreeIn u P)
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h3
P : Formula
u v : VarName
⊢ ¬(¬True ∧ ¬u = v ∧ isFreeIn u P)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u P)
Tactic:
simp only [def_exists_]
Proof state after:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u P.not_).not_
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u P.not_).not_
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬(¬True ∧ isFreeIn u P)
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬(¬True ∧ isFreeIn u P)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {exists_ u (forall_ v P)}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (exists_ u (forall_ v P))
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (exists_ u (forall_ v P))
Tactic:
simp only [def_exists_]
Proof state after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P).not_).not_