internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Forall_isFreeIn
Proof state before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ x ∉ xs_tl ∧ isFreeIn x P ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = h1_P'
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
case same_ h1_P h1_P' h1_1 =>
  subst h1_1
  simp only [def_iff_]
  simp only [def_and_]
  SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = U
h1_2 : h1_P' = V
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
case diff_ h1_P h1_P' h1_1 h1_2 =>
  subst h1_1
  subst h1_2
  apply Forall_spec_id
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case and_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.and_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.and_ Q_u✝).iff_ (P_v✝.and_ Q_v✝)))

case or_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.or_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.or_ Q_u✝).iff_ (P_v✝.or_ Q_v✝)))

case iff_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.iff_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.iff_ Q_u✝).iff_ (P_v✝.iff_ Q_v✝)))

case exists_
U V P_U P_V : Formula
l : List VarName
x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (exists_ x✝ P_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((exists_ x✝ P_u✝).iff_ (exists_ x✝ P_v✝)))
Tactic:
all_goals
  sorry
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = h1_P'
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
subst h1_1
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P))
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P))
Tactic:
simp only [def_iff_]
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P).and_ (h1_P.imp_ h1_P)))
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P).and_ (h1_P.imp_ h1_P)))
Tactic:
simp only [def_and_]
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P).imp_ (h1_P.imp_ h1_P).not_).not_)
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P).imp_ (h1_P.imp_ h1_P).not_).not_)
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = U
h1_2 : h1_P' = V
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
subst h1_1
Proof state after:
V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_2 : h1_P' = V
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_2 : h1_P' = V
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
subst h1_2
Proof state after:
P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v h1_P') ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ h1_P')).imp_ (h1_P.iff_ h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v h1_P') ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ h1_P')).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply Forall_spec_id
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P.not_ → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_))
Tactic:
simp only [isBoundIn] at h2
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_))
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_))
Tactic:
apply IsDeduct.mp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Proof state after:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_)))

case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_)))
Tactic:
simp only [def_iff_]
Proof state after:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
      ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.not_.imp_ h1_P'.not_).and_ (h1_P'.not_.imp_ h1_P.not_))))
Theorem: FOL.NV.T_18_2
Proof state before:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
      ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.not_.imp_ h1_P'.not_).and_ (h1_P'.not_.imp_ h1_P.not_))))
Tactic:
simp only [def_and_]
Proof state after:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
      ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
        ((h1_P.not_.imp_ h1_P'.not_).imp_ (h1_P'.not_.imp_ h1_P.not_).not_).not_))
Theorem: FOL.NV.T_18_2
Proof state before:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
      ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
        ((h1_P.not_.imp_ h1_P'.not_).imp_ (h1_P'.not_.imp_ h1_P.not_).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
exact h1_ih h2
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (h1_P.imp_ h1_Q) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))
Tactic:
simp only [isBoundIn] at h2
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))
Tactic:
apply IsDeduct.mp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Proof state after:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
      ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q'))))

case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
case a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
      ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q'))))
Tactic:
apply IsDeduct.mp_ ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
Proof state after:
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q')).imp_
      (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
        ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))))

case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
Theorem: FOL.NV.T_18_2
Proof state before:
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q')).imp_
      (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
        ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_Q.imp_ h1_Q').and_ (h1_Q'.imp_ h1_Q))).imp_
      (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
        ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).and_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q))))))
Theorem: FOL.NV.T_18_2
Proof state before:
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_Q.imp_ h1_Q').and_ (h1_Q'.imp_ h1_Q))).imp_
      (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
        ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).and_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q))))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_Q.imp_ h1_Q').imp_ (h1_Q'.imp_ h1_Q).not_).not_).imp_
      (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
            ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
        ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).imp_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q)).not_).not_)))
Theorem: FOL.NV.T_18_2
Proof state before:
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_Q.imp_ h1_Q').imp_ (h1_Q'.imp_ h1_Q).not_).not_).imp_
      (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
            ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
        ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).imp_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q)).not_).not_)))
Tactic:
SC
Proof state after:
no goals