internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi)
Tactic:
apply psi_ih V V' σ
Proof state after:
case a.h.e'_2.a.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)

case a.h.e'_2.a.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)
Tactic:
intro x a1
Proof state after:
case a.h.e'_2.a.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : isFreeIn x psi
⊢ V' x = V (σ x)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : isFreeIn x psi
⊢ V' x = V (σ x)
Tactic:
apply h1
Proof state after:
case a.h.e'_2.a.h1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : isFreeIn x psi
⊢ isFreeIn x phi ∨ isFreeIn x psi
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : isFreeIn x psi
⊢ isFreeIn x phi ∨ isFreeIn x psi
Tactic:
right
Proof state after:
case a.h.e'_2.a.h1.a.h
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : isFreeIn x psi
⊢ isFreeIn x psi
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h1.a.h
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : isFreeIn x psi
⊢ isFreeIn x psi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
Tactic:
intro x a1
Proof state after:
case a.h.e'_2.a.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ V'' x = V x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ V'' x = V x
Tactic:
apply h2
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Tactic:
simp only [Finset.mem_biUnion, Finset.mem_union] at a1
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Tactic:
apply Exists.elim a1
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
⊢ ∀ (a : PredName × ℕ),
    a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a → x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
⊢ ∀ (a : PredName × ℕ),
    a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a → x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Tactic:
intro a a2
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
Tactic:
simp only [Finset.mem_biUnion, Finset.mem_union]
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ psi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ psi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ ∃ a, (a ∈ phi.predVarSet ∨ a ∈ psi.predVarSet) ∧ x ∈ predVarFreeVarSet τ a