Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
h1 : IsDeduct Δ F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ, Holds D I V E H) → Holds D I V E F
Tactic:
induction h1
Proof state after:
case struct_1_
Δ : List Formula
F : Formula
Δ✝ : List Formula
H✝ phi✝ : Formula
a✝ : IsDeduct Δ✝ phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝

case struct_2_
Δ : List Formula
F : Formula
Δ✝ : List Formula
H✝ phi✝ : Formula
a✝ : IsDeduct (H✝ :: H✝ :: Δ✝) phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝

case struct_3_
Δ : List Formula
F : Formula
Δ_1✝ Δ_2✝ : List Formula
H_1✝ H_2✝ phi✝ : Formula
a✝ : IsDeduct (Δ_1✝ ++ [H_1✝] ++ [H_2✝] ++ Δ_2✝) phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1✝ ++ [H_1✝] ++ [H_2✝] ++ Δ_2✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1✝ ++ [H_2✝] ++ [H_1✝] ++ Δ_2✝, Holds D I V E H) → Holds D I V E phi✝

case assume_
Δ : List Formula
F phi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [phi✝], Holds D I V E H) → Holds D I V E phi✝

case prop_0_
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E true_

case prop_1_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2_
Δ : List Formula
F phi✝ psi✝ chi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case mp_
Δ : List Formula
F : Formula
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ✝ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ✝ phi✝
a_ih✝¹ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E (phi✝.imp_ psi✝)
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E psi✝

case dt_
Δ : List Formula
F : Formula
Δ✝ : List Formula
H✝ phi✝ : Formula
a✝ : IsDeduct (H✝ :: Δ✝) phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E (H✝.imp_ phi✝)

case pred_1_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v✝ (phi✝.imp_ psi✝)).imp_ ((forall_ v✝ phi✝).imp_ (forall_ v✝ psi✝)))

case pred_2_
Δ : List Formula
F : Formula
v✝ t✝ : VarName
phi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v✝ phi✝).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v✝ t✝) freshChar phi✝))

case pred_3_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : ¬isFreeIn v✝ phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi✝.imp_ (forall_ v✝ phi✝))

case gen_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : IsDeduct [] phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (forall_ v✝ phi✝)

case eq_1_
Δ : List Formula
F : Formula
v✝ : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (eq_ v✝ v✝)

case eq_2_pred_var_
Δ : List Formula
F : Formula
name✝ : PredName
xs✝ ys✝ : List VarName
a✝ : xs✝.length = ys✝.length
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        ((List.foldr and_ true_ (List.zipWith eq_ xs✝ ys✝)).imp_ ((pred_var_ name✝ xs✝).iff_ (pred_var_ name✝ ys✝)))

case eq_2_eq_
Δ : List Formula
F : Formula
x_0✝ x_1✝ y_0✝ y_1✝ : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E (((eq_ x_0✝ y_0✝).and_ (eq_ x_1✝ y_1✝)).imp_ ((eq_ x_0✝ x_1✝).iff_ (eq_ y_0✝ y_1✝)))

case def_false_
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (false_.iff_ true_.not_)

case def_and_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
            (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)

case sub_
Δ : List Formula
F : Formula
Δ✝ : List Formula
phi✝ : Formula
τ✝ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ✝ phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ✝) Δ✝, Holds D I V E H) →
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ✝ phi✝)