internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (I' D I V'' E τ).pred_var_ X (List.map V' xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Tactic:
simp only [I']
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (Interpretation.usingPred D I fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds).pred_var_
      X (List.map V' xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (Interpretation.usingPred D I fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds).pred_var_
      X (List.map V' xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (if h : (τ X (List.map V' xs).length).isSome = true then
      if (List.map V' xs).length = ((τ X (List.map V' xs).length).get ⋯).1.length then
        Holds D I (Function.updateListITE V'' ((τ X (List.map V' xs).length).get ⋯).1 (List.map V' xs)) E
          ((τ X (List.map V' xs).length).get ⋯).2
      else I.pred_var_ X (List.map V' xs)
    else I.pred_var_ X (List.map V' xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (if h : (τ X (List.map V' xs).length).isSome = true then
      if (List.map V' xs).length = ((τ X (List.map V' xs).length).get ⋯).1.length then
        Holds D I (Function.updateListITE V'' ((τ X (List.map V' xs).length).get ⋯).1 (List.map V' xs)) E
          ((τ X (List.map V' xs).length).get ⋯).2
      else I.pred_var_ X (List.map V' xs)
    else I.pred_var_ X (List.map V' xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V' xs)
    else I.pred_var_ X (List.map V' xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V' xs)
    else I.pred_var_ X (List.map V' xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
h✝¹ : (τ X xs.length).isSome = true
h✝ : xs.length = ((τ X xs.length).get ⋯).1.length
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
h✝¹ : (τ X xs.length).isSome = true
h✝ : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
h✝ : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))
Tactic:
case _ c1 c2 =>
  simp only [Holds]
  simp
  congr! 1
  simp only [List.map_eq_map_iff]
  intro x a1
  simp
  exact h1 x a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))
Tactic:
case _ c1 =>
  simp only [Holds]
  simp
  congr! 1
  simp only [List.map_eq_map_iff]
  intro x a1
  simp
  exact h1 x a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)
Tactic:
simp only [c1] at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
h2 :
  ∀ x ∈ if h : True then ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset else ∅, V'' x = V x
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
h2 :
  ∀ x ∈ if h : True then ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset else ∅, V'' x = V x
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)
Tactic:
simp at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
h2 : ∀ x ∈ ((τ X xs.length).get ⋯).2.freeVarSet, x ∉ ((τ X xs.length).get ⋯).1 → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
h2 : ∀ x ∈ ((τ X xs.length).get ⋯).2.freeVarSet, x ∉ ((τ X xs.length).get ⋯).1 → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)
Tactic:
set zs := (Option.get (τ X (List.length xs)) (_ : Option.isSome (τ X (List.length xs)) = true)).1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
h2 : ∀ x ∈ ((τ X xs.length).get ⋯).2.freeVarSet, x ∉ zs → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c ((τ X xs.length).get ⋯).2)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
h2 : ∀ x ∈ ((τ X xs.length).get ⋯).2.freeVarSet, x ∉ zs → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c ((τ X xs.length).get ⋯).2)
Tactic:
set H := (Option.get (τ X (List.length xs)) (_ : Option.isSome (τ X (List.length xs)) = true)).2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Tactic:
obtain s1 := Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateListITE id zs (xs.map σ)) c H
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (V ∘ Function.updateListITE id zs (List.map σ xs)) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (V ∘ Function.updateListITE id zs (List.map σ xs)) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Tactic:
simp only [Function.updateListITE_comp] at s1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (Function.updateListITE (V ∘ id) zs (List.map V (List.map σ xs))) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (Function.updateListITE (V ∘ id) zs (List.map V (List.map σ xs))) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Tactic:
simp at s1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H)
Tactic:
simp only [s1]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs (List.map σ xs)) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H
⊢ Holds D I (Function.updateListITE V'' zs (List.map V' xs)) E H ↔
    Holds D I (Function.updateListITE V zs (List.map (V ∘ σ) xs)) E H