internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_
        (((forall_ u P_u).imp_ (forall_ v P_v)).imp_ ((forall_ v P_v).imp_ (forall_ u P_u)).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ u P_u).imp_ (forall_ v P_v))
Tactic:
apply deduction_theorem
Proof state after:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ u P_u}) (forall_ v P_v)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ u P_u}) (forall_ v P_v)
Tactic:
simp
Proof state after:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} (forall_ v P_v)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} (forall_ v P_v)
Tactic:
apply generalization
Proof state after:
case a.a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} P_v

case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ u P_u}, ¬isFreeIn v H
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ u P_u} P_v
Tactic:
subst h1_right_right_right_right_left
Proof state after:
case a.a.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (fastReplaceFree u v P_u)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (fastReplaceFree u v P_u)
Tactic:
apply spec
Proof state after:
case a.a.h1.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (forall_ u P_u)

case a.a.h1.h1.h2
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ fastAdmits u v P_u
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h1.h1
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ IsDeduct {forall_ u P_u} (forall_ u P_u)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a.a.h1.h1.h1.a
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ forall_ u P_u ∈ {forall_ u P_u}
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h1.h1.a
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ forall_ u P_u ∈ {forall_ u P_u}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h1.h2
P_u : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_right_left : fastAdmits u v P_u
h1_right_left : ¬isFreeIn u (fastReplaceFree u v P_u)
h1_right_right_right_left : fastAdmits v u (fastReplaceFree u v P_u)
h1_right_right_right_right_right : P_u = fastReplaceFree v u (fastReplaceFree u v P_u)
⊢ fastAdmits u v P_u
Tactic:
exact h1_right_right_left
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ u P_u}, ¬isFreeIn v H
Tactic:
intro H a1
Proof state after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ u P_u}
⊢ ¬isFreeIn v H
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ u P_u}
⊢ ¬isFreeIn v H
Tactic:
simp at a1
Proof state after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ u P_u
⊢ ¬isFreeIn v H
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ u P_u
⊢ ¬isFreeIn v H
Tactic:
subst a1
Proof state after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v (forall_ u P_u)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v (forall_ u P_u)
Tactic:
simp only [isFreeIn]
Proof state after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬v = u ∧ isFreeIn v P_u)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬v = u ∧ isFreeIn v P_u)
Tactic:
simp
Proof state after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬v = u → ¬isFreeIn v P_u
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬v = u → ¬isFreeIn v P_u
Tactic:
intro _
Proof state after:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬v = u
⊢ ¬isFreeIn v P_u
Theorem: FOL.NV.T_18_6
Proof state before:
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬v = u
⊢ ¬isFreeIn v P_u
Tactic:
exact h1_left
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof state before:
case a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ v P_v).imp_ (forall_ u P_u))
Tactic:
apply deduction_theorem
Proof state after:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ v P_v}) (forall_ u P_u)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct (∅ ∪ {forall_ v P_v}) (forall_ u P_u)
Tactic:
simp
Proof state after:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} (forall_ u P_u)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} (forall_ u P_u)
Tactic:
apply generalization
Proof state after:
case a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} P_u

case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ v P_v}, ¬isFreeIn u H
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h1
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct {forall_ v P_v} P_u
Tactic:
subst h1_right_right_right_right_right
Proof state after:
case a.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (fastReplaceFree v u P_v)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (fastReplaceFree v u P_v)
Tactic:
apply spec
Proof state after:
case a.h1.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (forall_ v P_v)

case a.h1.h1.h2
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ fastAdmits v u P_v
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h1.h1
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ IsDeduct {forall_ v P_v} (forall_ v P_v)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a.h1.h1.h1.a
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ forall_ v P_v ∈ {forall_ v P_v}
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h1.h1.a
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ forall_ v P_v ∈ {forall_ v P_v}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h1.h2
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ fastAdmits v u P_v
Tactic:
exact h1_right_right_right_left
Proof state after:
no goals
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ∀ H ∈ {forall_ v P_v}, ¬isFreeIn u H
Tactic:
intro H a1
Proof state after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ v P_v}
⊢ ¬isFreeIn u H
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H ∈ {forall_ v P_v}
⊢ ¬isFreeIn u H
Tactic:
simp at a1
Proof state after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ v P_v
⊢ ¬isFreeIn u H
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
H : Formula
a1 : H = forall_ v P_v
⊢ ¬isFreeIn u H
Tactic:
subst a1
Proof state after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn u (forall_ v P_v)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn u (forall_ v P_v)
Tactic:
simp only [isFreeIn]
Proof state after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬u = v ∧ isFreeIn u P_v)
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬(¬u = v ∧ isFreeIn u P_v)
Tactic:
simp
Proof state after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬u = v → ¬isFreeIn u P_v
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬u = v → ¬isFreeIn u P_v
Tactic:
intro _
Proof state after:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬u = v
⊢ ¬isFreeIn u P_v
Theorem: FOL.NV.T_18_6
Proof state before:
case a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬u = v
⊢ ¬isFreeIn u P_v
Tactic:
exact h1_right_left
Proof state after:
no goals