internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux
Proof state before:
case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_admits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admits t v (replaceFree v t F)
Tactic:
simp only [replaceFree]
Proof state after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admits t v (replaceFreeAux v t ∅ F)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_admits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admits t v (replaceFreeAux v t ∅ F)
Tactic:
simp only [admits]
Proof state after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admitsAux t v ∅ (replaceFreeAux v t ∅ F)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_admits
Proof state before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admitsAux t v ∅ (replaceFreeAux v t ∅ F)
Tactic:
exact replaceFreeAux_admitsAux F v t ∅ h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs ∧ v ∉ S → u ∉ S
⊢ v ∈ xs ∧ v ∉ S ∪ T → u ∉ S ∪ T
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y |def_ X xs =>
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u S phi → admitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x}) phi
⊢ admitsAux v u (S ∪ T ∪ {x}) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [Finset.union_right_comm S T {x}]
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
case not_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝ : Formula
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝

case imp_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), admitsAux v u S a✝¹ → admitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝¹ ∧ admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝¹ ∧ admitsAux v u (S ∪ T) a✝

case and_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), admitsAux v u S a✝¹ → admitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝¹ ∧ admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝¹ ∧ admitsAux v u (S ∪ T) a✝

case or_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), admitsAux v u S a✝¹ → admitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝¹ ∧ admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝¹ ∧ admitsAux v u (S ∪ T) a✝

case iff_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), admitsAux v u S a✝¹ → admitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝¹ ∧ admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝¹ ∧ admitsAux v u (S ∪ T) a✝
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : admitsAux v u S (def_ a✝¹ a✝)
⊢ admitsAux v u (S ∪ T) (def_ a✝¹ a✝)
Tactic:
simp only [admitsAux] at h1
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S → u ∉ S
⊢ admitsAux v u (S ∪ T) (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S → u ∉ S
⊢ admitsAux v u (S ∪ T) (def_ a✝¹ a✝)
Tactic:
simp only [admitsAux]
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S → u ∉ S
⊢ v ∈ a✝ ∧ v ∉ S ∪ T → u ∉ S ∪ T
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs ∧ v ∉ S → u ∉ S
⊢ v ∈ xs ∧ v ∉ S ∪ T → u ∉ S ∪ T
Tactic:
simp
Proof state after:
v u : VarName
T : Finset VarName
h2 : u ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs ∧ v ∉ S → u ∉ S
⊢ v ∈ xs → v ∉ S → v ∉ T → u ∉ S ∧ u ∉ T
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs ∧ v ∉ S → u ∉ S
⊢ v ∈ xs → v ∉ S → v ∉ T → u ∉ S ∧ u ∉ T
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u S phi → admitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x}) phi
⊢ admitsAux v u (S ∪ T ∪ {x}) phi
Tactic:
simp only [Finset.union_right_comm S T {x}]
Proof state after:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u S phi → admitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x}) phi
⊢ admitsAux v u (S ∪ {x} ∪ T) phi
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u S phi → admitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x}) phi
⊢ admitsAux v u (S ∪ {x} ∪ T) phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_add_binders
Proof state before:
case iff_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (S : Finset VarName), admitsAux v u S a✝¹ → admitsAux v u (S ∪ T) a✝¹
a_ih✝ : ∀ (S : Finset VarName), admitsAux v u S a✝ → admitsAux v u (S ∪ T) a✝
S : Finset VarName
h1 : admitsAux v u S a✝¹ ∧ admitsAux v u S a✝
⊢ admitsAux v u (S ∪ T) a✝¹ ∧ admitsAux v u (S ∪ T) a✝
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs ∧ v ∉ S ∪ T → u ∉ S ∪ T
⊢ v ∈ xs ∧ v ∉ S → u ∉ S
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y | def_ X xs =>
  simp at h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ T) phi
⊢ admitsAux v u S phi
Tactic:
case not_ phi phi_ih =>
  exact phi_ih S h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
phi psi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
psi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) psi → admitsAux v u S psi
S : Finset VarName
h1 : admitsAux v u (S ∪ T) phi ∧ admitsAux v u (S ∪ T) psi
⊢ admitsAux v u S phi ∧ admitsAux v u S psi
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ T ∪ {x}) phi
⊢ admitsAux v u (S ∪ {x}) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [Finset.union_right_comm S T {x}] at h1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : v ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : admitsAux v u (S ∪ T) (def_ a✝¹ a✝)
⊢ admitsAux v u S (def_ a✝¹ a✝)
Tactic:
simp only [admitsAux] at h1
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : v ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S ∪ T → u ∉ S ∪ T
⊢ admitsAux v u S (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
case def_
v u : VarName
T : Finset VarName
h2 : v ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S ∪ T → u ∉ S ∪ T
⊢ admitsAux v u S (def_ a✝¹ a✝)
Tactic:
simp only [admitsAux]
Proof state after:
case def_
v u : VarName
T : Finset VarName
h2 : v ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S ∪ T → u ∉ S ∪ T
⊢ v ∈ a✝ ∧ v ∉ S → u ∉ S
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs ∧ v ∉ S ∪ T → u ∉ S ∪ T
⊢ v ∈ xs ∧ v ∉ S → u ∉ S
Tactic:
simp at h1
Proof state after:
v u : VarName
T : Finset VarName
h2 : v ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs → v ∉ S → v ∉ T → u ∉ S ∧ u ∉ T
⊢ v ∈ xs ∧ v ∉ S → u ∉ S
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
X : DefName
xs : List VarName
S : Finset VarName
h1 : v ∈ xs → v ∉ S → v ∉ T → u ∉ S ∧ u ∉ T
⊢ v ∈ xs ∧ v ∉ S → u ∉ S
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ T) phi
⊢ admitsAux v u S phi
Tactic:
exact phi_ih S h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
phi psi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
psi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) psi → admitsAux v u S psi
S : Finset VarName
h1 : admitsAux v u (S ∪ T) phi ∧ admitsAux v u (S ∪ T) psi
⊢ admitsAux v u S phi ∧ admitsAux v u S psi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ T ∪ {x}) phi
⊢ admitsAux v u (S ∪ {x}) phi
Tactic:
simp only [Finset.union_right_comm S T {x}] at h1
Proof state after:
v u : VarName
T : Finset VarName
h2 : v ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x} ∪ T) phi
⊢ admitsAux v u (S ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_del_binders
Proof state before:
v u : VarName
T : Finset VarName
h2 : v ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x} ∪ T) phi
⊢ admitsAux v u (S ∪ {x}) phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case pred_const_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : v ∈ a✝
h3 : v ∉ binders
⊢ u ∉ binders

case pred_var_
v u : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : v ∈ a✝
h3 : v ∉ binders
⊢ u ∉ binders

case eq_
v u a✝¹ a✝ : VarName
binders : Finset VarName
h1 : (v = a✝¹ ∨ v = a✝) ∧ v ∉ binders → u ∉ binders
h2 : v = a✝¹ ∨ v = a✝
h3 : v ∉ binders
⊢ u ∉ binders

case not_
v u : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), admitsAux v u binders a✝ → isFreeIn v a✝ → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u binders a✝
h2 : isFreeIn v a✝
h3 : v ∉ binders
⊢ u ∉ binders

case imp_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), admitsAux v u binders a✝¹ → isFreeIn v a✝¹ → v ∉ binders → u ∉ binders
a_ih✝ : ∀ (binders : Finset VarName), admitsAux v u binders a✝ → isFreeIn v a✝ → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝
h2 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
h3 : v ∉ binders
⊢ u ∉ binders

case and_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), admitsAux v u binders a✝¹ → isFreeIn v a✝¹ → v ∉ binders → u ∉ binders
a_ih✝ : ∀ (binders : Finset VarName), admitsAux v u binders a✝ → isFreeIn v a✝ → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝
h2 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
h3 : v ∉ binders
⊢ u ∉ binders

case or_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), admitsAux v u binders a✝¹ → isFreeIn v a✝¹ → v ∉ binders → u ∉ binders
a_ih✝ : ∀ (binders : Finset VarName), admitsAux v u binders a✝ → isFreeIn v a✝ → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝
h2 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
h3 : v ∉ binders
⊢ u ∉ binders

case iff_
v u : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), admitsAux v u binders a✝¹ → isFreeIn v a✝¹ → v ∉ binders → u ∉ binders
a_ih✝ : ∀ (binders : Finset VarName), admitsAux v u binders a✝ → isFreeIn v a✝ → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u binders a✝¹ ∧ admitsAux v u binders a✝
h2 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
h3 : v ∉ binders
⊢ u ∉ binders

case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : v ∈ a✝
h3 : v ∉ binders
⊢ u ∉ binders
Tactic:
all_goals
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : admitsAux v u binders (def_ a✝¹ a✝)
h2 : isFreeIn v (def_ a✝¹ a✝)
h3 : v ∉ binders
⊢ u ∉ binders
Tactic:
simp only [admitsAux] at h1
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : isFreeIn v (def_ a✝¹ a✝)
h3 : v ∉ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : isFreeIn v (def_ a✝¹ a✝)
h3 : v ∉ binders
⊢ u ∉ binders
Tactic:
simp only [isFreeIn] at h2
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : v ∈ a✝
h3 : v ∉ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h2 : ¬v = x ∧ isFreeIn v phi
h3 : v ∉ binders
⊢ u ∉ binders
Tactic:
cases h2
Proof state after:
case intro
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
left✝ : ¬v = x
right✝ : isFreeIn v phi
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ u ∉ binders
Tactic:
apply phi_ih binders
Proof state after:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ admitsAux v u binders phi

case h2
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ isFreeIn v phi

case h3
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ admitsAux v u binders phi
Tactic:
apply admitsAux_del_binders phi v u binders {x} h1
Proof state after:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ v ∉ {x}
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ v ∉ {x}
Tactic:
simp
Proof state after:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ ¬v = x
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ ¬v = x
Tactic:
exact h2_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case h2
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact h2_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case h3
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ v ∉ binders
Tactic:
exact h3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.admitsAux_isFreeIn
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : v ∈ a✝
h3 : v ∉ binders
⊢ u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
v t : VarName
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Tactic:
induction E generalizing F binders V
Proof state after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
V : VarAssignment D
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) [] F ↔ Holds D I V [] (fastReplaceFree v t F)

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) F ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t F)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map V (List.map (fun x => if v = x then t else x) xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  simp
  congr! 1
  simp only [List.map_eq_map_iff]
  intro x a1
  simp
  simp only [Function.updateITE]
  split_ifs
  case _ c1 c2 =>
    subst c1
    tauto
  case _ c1 c2 =>
    subst c1
    contradiction
  case _ c1 c2 =>
    subst c2
    contradiction
  case _ c1 c2 =>
    rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Function.updateITE V v (V' t) x = Function.updateITE V v (V' t) y ↔
    V (if v = x then t else x) = V (if v = y then t else y)
Tactic:
case eq_ x y =>
  simp only [Function.updateITE]
  simp only [eq_comm]
  congr! 1
  all_goals
    split_ifs
    case _ c1 =>
      subst c1
      tauto
    case _ c1 =>
      rfl
Proof state after:
no goals