Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D (I' D I V'' (E_hd :: E_tl) τ) V' E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
h✝¹ : X = E_hd.name ∧ xs.length = E_hd.args.length
h✝ : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
h✝¹ : X = E_hd.name ∧ xs.length = E_hd.args.length
h✝ : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I V E_tl (def_ X (List.map σ xs))

case pos
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
h✝¹ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h✝ : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) V' E_tl (def_ X xs) ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
h✝¹ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h✝ : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))