Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = V (if h1_v = x then h1_t else x)

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
h✝ : h1_v = x
⊢ V h1_t = V h1_t

case neg
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
h✝ : ¬h1_v = x
⊢ V x = V x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'