internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi) ↔
    (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
apply h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
Tactic:
apply h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
simp only [isFreeIn] at h1_1
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
simp at h1_1
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply Holds_coincide_Var
Proof state after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi → Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v = Function.updateITE V h1_x d v
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi → Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v = Function.updateITE V h1_x d v
Tactic:
intro x a1
Proof state after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x = Function.updateITE V h1_x d x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x = Function.updateITE V h1_x d x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) = if x = h1_x then d else V x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) = if x = h1_x then d else V x
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝ : x = h1_x
⊢ d = d

case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝¹ : ¬x = h1_x
h✝ : x = h1_v
⊢ V h1_t = V x

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝¹ : ¬x = h1_x
h✝ : ¬x = h1_v
⊢ V x = V x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : x = h1_x
⊢ d = d
Tactic:
case _ c1 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : x = h1_v
⊢ V h1_t = V x
Tactic:
case _ c1 c2 =>
  subst c2
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : ¬x = h1_v
⊢ V x = V x
Tactic:
case _ c1 c2 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : x = h1_x
⊢ d = d
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : x = h1_v
⊢ V h1_t = V x
Tactic:
subst c2
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_t : VarName
V : VarAssignment D
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
h1_1 : ¬x = h1_x → ¬isFreeIn x h1_phi
⊢ V h1_t = V x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_t : VarName
V : VarAssignment D
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
h1_1 : ¬x = h1_x → ¬isFreeIn x h1_phi
⊢ V h1_t = V x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : ¬x = h1_v
⊢ V x = V x
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Tactic:
simp only [isFreeIn] at h1_1
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi'
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
specialize h1_ih (Function.updateITE V h1_x d)
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
simp only [← h1_ih]
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi
Tactic:
apply Holds_coincide_Var
Proof state after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi →
      Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v =
        Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t) v