Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
binders : Finset VarName
F : Formula
h1 : admitsAux τ binders F
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 F ↔
    Holds D I V E (replace τ F)
Tactic:
induction F generalizing binders V
Proof state after:
case pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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_const_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (pred_const_ a✝¹ a✝))

case pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_var_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (pred_var_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (eq_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders true_
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 true_ ↔
    Holds D I V E (replace τ true_)

case false_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 false_ ↔
    Holds D I V E (replace τ false_)

case not_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders a✝.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 a✝.not_ ↔
    Holds D I V E (replace τ a✝.not_)

case imp_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.imp_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (a✝¹.imp_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.imp_ a✝))

case and_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.and_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (a✝¹.and_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.and_ a✝))

case or_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.or_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (a✝¹.or_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.or_ a✝))

case iff_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.iff_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (a✝¹.iff_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.iff_ a✝))

case forall_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (forall_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (forall_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (forall_ a✝¹ a✝))

case exists_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (exists_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (exists_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ 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 (def_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (def_ a✝¹ a✝))