Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
F : Formula
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ F) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) F
Tactic:
induction F
Proof state after:
case pred_const_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (pred_const_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (pred_const_ a✝¹ a✝)

case pred_var_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (pred_var_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (pred_var_ a✝¹ a✝)

case eq_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : VarName
⊢ evalPrime V (substPrime σ (eq_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (eq_ a✝¹ a✝)

case true_
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ true_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) true_

case false_
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ false_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) false_

case not_
σ : Formula → Formula
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ a✝.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝.not_

case imp_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.imp_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.imp_ a✝)

case and_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.and_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.and_ a✝)

case or_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.or_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.or_ a✝)

case iff_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.iff_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.iff_ a✝)

case forall_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (forall_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (forall_ a✝¹ a✝)

case exists_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (exists_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (exists_ a✝¹ a✝)

case def_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)