Theorem: FOL.NV.is_tauto_def_iff (FOL/NV/Margaris/Prop.lean)

State before:
P Q : Formula
⊢ (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
        (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
State after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    evalPrime V
      (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_

State before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    evalPrime V
      (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_
Tactic:
simp only [eval_iff, eval_not, eval_imp]
State after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    ¬(((evalPrime V P ↔ evalPrime V Q) → ¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P))) →
        ¬(¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P)) → (evalPrime V P ↔ evalPrime V Q)))

State before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    ¬(((evalPrime V P ↔ evalPrime V Q) → ¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P))) →
        ¬(¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P)) → (evalPrime V P ↔ evalPrime V Q)))
Tactic:
tauto
State after:
no goals