Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
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))
⊢ (if h1_X = hd.name ∧ h1_xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
        tl hd.q
    else Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs)) ↔
    if h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
        tl hd.q
    else Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
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))
h✝¹ : h1_X = hd.name ∧ h1_xs.length = hd.args.length
h✝ : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q

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))
h✝¹ : h1_X = hd.name ∧ h1_xs.length = hd.args.length
h✝ : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

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))
h✝¹ : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
h✝ : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q

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))
h✝¹ : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
h✝ : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ 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))