internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
s2 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [s2] at s1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s2 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s2 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
clear s2
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ (if xs.length = (τ X xs.length).1.length then
      Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ (if xs.length = (τ X xs.length).1.length then
      Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)
Tactic:
simp only [if_pos h1_right_right]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
Tactic:
exact s1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
Tactic:
apply Holds_coincide_Var
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ ∀ (v : VarName),
    isFreeIn v (τ X xs.length).2 →
      Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
        Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ ∀ (v : VarName),
    isFreeIn v (τ X xs.length).2 →
      Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
        Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
intro v a1
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
by_cases c1 : v ∈ (τ X xs.length).fst
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
apply Function.updateListITE_mem_eq_len V V' v (τ X xs.length).fst (List.map V xs) c1
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ (τ X xs.length).1.length = (List.map V xs).length
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ (τ X xs.length).1.length = (List.map V xs).length
Tactic:
simp
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ (τ X xs.length).1.length = xs.length