This file proves auxiliary lemmas about Asserts, which are lists of (well-formed) boolean Terms.

theorem Cedar.Thm.asserts_satisfiedBy_true {I : SymCC.Interpretation} {asserts : SymCC.Asserts} : SymCC.Asserts.satisfiedBy I asserts = true ↔ ∀ (t : SymCC.Term), t ∈ asserts → SymCC.Term.interpret I t = SymCC.Term.prim (SymCC.TermPrim.bool true)

theorem Cedar.Thm.asserts_satisfiable_def {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv ⊧ asserts ↔ ∃ (I : SymCC.Interpretation), I.WellFormed εnv.entities ∧ ∀ (t : SymCC.Term), t ∈ asserts → SymCC.Term.interpret I t = SymCC.Term.prim (SymCC.TermPrim.bool true)

theorem Cedar.Thm.asserts_unsatisfiable_def {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv ⊭ asserts ↔ ∀ (I : SymCC.Interpretation), I.WellFormed εnv.entities → ∃ (t : SymCC.Term), t ∈ asserts ∧ SymCC.Term.interpret I t ≠ SymCC.Term.prim (SymCC.TermPrim.bool true)

theorem Cedar.Thm.asserts_last_not_true {I : SymCC.Interpretation} {ts : SymCC.Asserts} {t t' : SymCC.Term} : SymCC.Asserts.satisfiedBy I ts = true → t ∈ ts ++ [t'] → SymCC.Term.interpret I t ≠ SymCC.Term.prim (SymCC.TermPrim.bool true) → t = t'

theorem Cedar.Thm.asserts_all_true {I : SymCC.Interpretation} {ts : SymCC.Asserts} {t' : SymCC.Term} : (∀ (t : SymCC.Term), t ∈ ts ++ [t'] → SymCC.Term.interpret I t = SymCC.Term.prim (SymCC.TermPrim.bool true)) → SymCC.Asserts.satisfiedBy I ts = true ∧ SymCC.Term.interpret I t' = SymCC.Term.prim (SymCC.TermPrim.bool true)