This file contains useful definitions and theorems for comparing booleans to terms.

instance Cedar.Thm.instSameBoolTerm : Spec.Same Bool SymCC.Term

Equations

• Cedar.Thm.instSameBoolTerm = { same := fun (b : Bool) (t : Cedar.SymCC.Term) => t = Cedar.SymCC.Term.bool b }

theorem Cedar.Thm.same_bool_def {b : Bool} {t : SymCC.Term} : b ∼ t ↔ t = SymCC.Term.bool b

theorem Cedar.Thm.same_bool_not_true_implies_false {b : Bool} {t : SymCC.Term} : b ∼ t → SymCC.Factory.not t = SymCC.Term.bool true → b = false

theorem Cedar.Thm.same_bool_not_not_true_implies_true {b : Bool} {t : SymCC.Term} : b ∼ t → ¬SymCC.Factory.not t = SymCC.Term.bool true → b = true