internlm/Lean-Github huggingface dataset:
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'))
Tactic:
apply h1_ih_2
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
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l
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
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l
Tactic:
intro v a2
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
v : VarName
a2 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q
⊢ v ∈ l
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
v : VarName
a2 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q
⊢ v ∈ l
Tactic:
apply h2 v
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
v : VarName
a2 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v 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
v : VarName
a2 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)
Tactic:
tauto
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_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'))
Tactic:
apply h1_ih_1
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
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
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
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
Tactic:
intro v a1
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
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l
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
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l
Tactic:
apply h2 v
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
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)
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
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)
Tactic:
cases a1
Proof state after:
case a.intro
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
v : VarName
left✝ : isFreeIn v U ∨ isFreeIn v V
right✝ : isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v 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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)
Tactic:
constructor
Proof state after:
case left
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isFreeIn v U ∨ isFreeIn v V

case right
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P ∨ isBoundIn v h1_Q
Theorem: FOL.NV.T_18_2
Proof state before:
case left
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isFreeIn v U ∨ isFreeIn v V
Tactic:
exact a1_left
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case right
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P ∨ isBoundIn v h1_Q
Tactic:
left
Proof state after:
case right.h
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P
Theorem: FOL.NV.T_18_2
Proof state before:
case right.h
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P
Tactic:
exact a1_right
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_x : 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 (forall_ h1_x h1_P) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
simp only [isBoundIn] at h2
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_x : 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) ∧ (v = h1_x ∨ isBoundIn v h1_P) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_x : 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) ∧ (v = h1_x ∨ isBoundIn v h1_P) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
simp at h2
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
apply deduction_theorem
Proof state after:
case h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct (∅ ∪ {Forall_ l (U.iff_ V)}) ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct (∅ ∪ {Forall_ l (U.iff_ V)}) ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))
Tactic:
simp
Proof state after:
case h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))
Tactic:
apply IsDeduct.mp_ (forall_ h1_x (h1_P.iff_ h1_P'))
Proof state after:
case h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)}
    ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))

case h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} (forall_ h1_x (h1_P.iff_ h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)}
    ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
apply T_18_1
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} (forall_ h1_x (h1_P.iff_ h1_P'))
Tactic:
apply generalization
Proof state after:
case h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} (h1_P.iff_ h1_P')

case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : 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 → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ∀ H ∈ {Forall_ l (U.iff_ V)}, ¬isFreeIn h1_x H