Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
⊢ (if X' = hd.name ∧ xs'.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs')) tl hd.q
    else Holds D I V tl (def_ X' xs')) ↔
    if X' = hd.name ∧ (List.map σ' xs').length = hd.args.length then
      Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q
    else Holds D I V' tl (def_ X' (List.map σ' xs'))
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
h✝¹ : X' = hd.name ∧ xs'.length = hd.args.length
h✝ : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs')) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q

case neg
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
h✝¹ : X' = hd.name ∧ xs'.length = hd.args.length
h✝ : ¬(X' = hd.name ∧ (List.map σ' xs').length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs')) tl hd.q ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))

case pos
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
h✝¹ : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
h✝ : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q

case neg
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
h✝¹ : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
h✝ : ¬(X' = hd.name ∧ (List.map σ' xs').length = hd.args.length)
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))