internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
specialize h1_ih h2 h3
Proof state after:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (P_u.iff_ P_v))
Proof state after:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_ ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_)))

case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_ ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_)))
Tactic:
simp only [def_iff_]
Proof state after:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).and_ (P_v.not_.imp_ P_u.not_))))
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).and_ (P_v.not_.imp_ P_u.not_))))
Tactic:
simp only [def_and_]
Proof state after:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).imp_ (P_v.not_.imp_ P_u.not_).not_).not_))
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).imp_ (P_v.not_.imp_ P_u.not_).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Tactic:
exact h1_ih
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬isBoundIn r (P_u.imp_ Q_u)
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
simp only [isBoundIn] at h2
Proof state after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬(isBoundIn r P_u ∨ isBoundIn r Q_u)
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬(isBoundIn r P_u ∨ isBoundIn r Q_u)
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
push_neg at h2
Proof state after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
h2 : ¬isBoundIn r P_u ∧ ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
h2 : ¬isBoundIn r P_u ∧ ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
cases h2
Proof state after:
case intro
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
left✝ : ¬isBoundIn r P_u
right✝ : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
simp only [isBoundIn] at h3
Proof state after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬(isBoundIn s P_u ∨ isBoundIn s Q_u)
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬(isBoundIn s P_u ∨ isBoundIn s Q_u)
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
push_neg at h3
Proof state after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3 : ¬isBoundIn s P_u ∧ ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3 : ¬isBoundIn s P_u ∧ ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
cases h3
Proof state after:
case intro
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
left✝ : ¬isBoundIn s P_u
right✝ : ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
specialize h1_ih_1 h2_left h3_left
Proof state after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
specialize h1_ih_2 h2_right h3_right
Proof state after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (Q_u.iff_ Q_v))
Proof state after:
case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v))))

case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (Q_u.iff_ Q_v))
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v))))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (P_u.iff_ P_v))
Proof state after:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_
      (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))))

case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_
      (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).and_ (Q_v.imp_ Q_u))).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).and_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u))))))
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).and_ (Q_v.imp_ Q_u))).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).and_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u))))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).imp_ (Q_v.imp_ Q_u).not_).not_).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).imp_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u)).not_).not_)))
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).imp_ (Q_v.imp_ Q_u).not_).not_).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).imp_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u)).not_).not_)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Tactic:
exact h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (Q_u.iff_ Q_v))
Tactic:
exact h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r (forall_ x P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
simp only [isBoundIn] at h2
Proof state after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬(r = x ∨ isBoundIn r P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬(r = x ∨ isBoundIn r P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
push_neg at h2
Proof state after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
h2 : r ≠ x ∧ ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
h2 : r ≠ x ∧ ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
cases h2
Proof state after:
case intro
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
left✝ : r ≠ x
right✝ : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
simp only [isBoundIn] at h3
Proof state after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬(s = x ∨ isBoundIn s P_u)
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬(s = x ∨ isBoundIn s P_u)
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
push_neg at h3
Proof state after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3 : s ≠ x ∧ ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3 : s ≠ x ∧ ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
cases h3
Proof state after:
case intro
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
left✝ : s ≠ x
right✝ : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct (∅ ∪ {eq_ r s}) ((forall_ x P_u).iff_ (forall_ x P_v))