Well-formed terms and factory functions

This file proves basic lemmas about well-formedness of terms and Factory functions.

theorem Cedar.Thm.wf_term_var_implies {εs : SymCC.SymEntities} {v : SymCC.TermVar} : SymCC.Term.WellFormed εs (SymCC.Term.var v) → SymCC.TermVar.WellFormed εs v

theorem Cedar.Thm.wf_term_some_implies {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormed εs t.some → SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_term_none_implies {εs : SymCC.SymEntities} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs (SymCC.Term.none ty) → SymCC.TermType.WellFormed εs ty

theorem Cedar.Thm.wf_term_set_implies_wf_elt {εs : SymCC.SymEntities} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} {t : SymCC.Term} : SymCC.Term.WellFormed εs (SymCC.Term.set s ty) → t ∈ s → SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_term_set_implies_typeOf_elt {εs : SymCC.SymEntities} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} {t : SymCC.Term} : SymCC.Term.WellFormed εs (SymCC.Term.set s ty) → t ∈ s → t.typeOf = ty

theorem Cedar.Thm.wf_term_set_implies_wf_type {εs : SymCC.SymEntities} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs (SymCC.Term.set s ty) → SymCC.TermType.WellFormed εs ty

theorem Cedar.Thm.wf_term_set_implies_wf_set {εs : SymCC.SymEntities} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs (SymCC.Term.set s ty) → s.WellFormed

theorem Cedar.Thm.wf_term_set_cons {εs : SymCC.SymEntities} {hd : SymCC.Term} {tl : List SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs (SymCC.Term.set (Data.Set.mk (hd :: tl)) ty) → SymCC.Term.WellFormed εs hd ∧ hd.typeOf = ty ∧ SymCC.Term.WellFormed εs (SymCC.Term.set (Data.Set.mk tl) ty)

theorem Cedar.Thm.wf_term_record_implies {t : SymCC.Term} {εs : SymCC.SymEntities} {r : Data.Map Spec.Attr SymCC.Term} {a : Spec.Attr} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.record r)) (h₂ : r.find? a = some t) : SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_term_record_implies_wf_value {t : SymCC.Term} {εs : SymCC.SymEntities} {r : Data.Map Spec.Attr SymCC.Term} {a : Spec.Attr} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.record r)) (h₂ : (a, t) ∈ r.toList) : SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_term_record_implies_wf_map {εs : SymCC.SymEntities} {r : Data.Map Spec.Attr SymCC.Term} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.record r)) : r.WellFormed

theorem Cedar.Thm.wf_prods_implies_wf_map_snd {εs : SymCC.SymEntities} {ats : List (Spec.Attr × SymCC.Term)} (h₁ : ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs t) (t : SymCC.Term) : t ∈ List.map Prod.snd ats → SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_prods_option_implies_wf_prods {εs : SymCC.SymEntities} {ats : List (Spec.Attr × SymCC.Term)} : (∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs t ∧ ∃ (ty : SymCC.TermType), t.typeOf = ty.option) → ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_bool {εs : SymCC.SymEntities} {b : Bool} : SymCC.Term.WellFormed εs (SymCC.Term.prim (SymCC.TermPrim.bool b))

theorem Cedar.Thm.wf_bv {εs : SymCC.SymEntities} {n : Nat} {bv : BitVec n} : SymCC.Term.WellFormed εs (SymCC.Term.prim (SymCC.TermPrim.bitvec bv))

theorem Cedar.Thm.wf_string {s : String} {εs : SymCC.SymEntities} : SymCC.Term.WellFormed εs (SymCC.Term.prim (SymCC.TermPrim.string s))

theorem Cedar.Thm.wf_datetime {ε : SymCC.SymEntities} {dt : Spec.Ext.Datetime} : SymCC.Term.WellFormed ε (SymCC.Term.ext (Spec.Ext.datetime dt))

theorem Cedar.Thm.wf_duration {ε : SymCC.SymEntities} {dt : Spec.Ext.Datetime.Duration} : SymCC.Term.WellFormed ε (SymCC.Term.ext (Spec.Ext.duration dt))

theorem Cedar.Thm.wf_term_some {t : SymCC.Term} {ty : SymCC.TermType} {εs : SymCC.SymEntities} : SymCC.Term.WellFormed εs t → t.typeOf = ty → SymCC.Term.WellFormed εs t.some ∧ t.some.typeOf = ty.option

def Cedar.Thm.WFArg (εs : SymCC.SymEntities) (t : SymCC.Term) (ty : SymCC.TermType) : Prop

Equations

• Cedar.Thm.WFArg εs t ty = (Cedar.SymCC.Term.WellFormed εs t ∧ t.typeOf = ty)

def Cedar.Thm.WFUnary (εs : SymCC.SymEntities) (ts : List SymCC.Term) (ty : SymCC.TermType) : Prop

Equations

• Cedar.Thm.WFUnary εs ts ty = ∃ (t : Cedar.SymCC.Term), ts = [t] ∧ Cedar.Thm.WFArg εs t ty

def Cedar.Thm.WFBinary (εs : SymCC.SymEntities) (ts : List SymCC.Term) (ty : SymCC.TermType) : Prop

Equations

• Cedar.Thm.WFBinary εs ts ty = ∃ (t₁ : Cedar.SymCC.Term), ∃ (t₂ : Cedar.SymCC.Term), ts = [t₁, t₂] ∧ Cedar.Thm.WFArg εs t₁ ty ∧ Cedar.Thm.WFArg εs t₂ ty

theorem Cedar.Thm.wf_term_app_not {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.not ts ty)) : ty = SymCC.TermType.bool ∧ WFUnary εs ts SymCC.TermType.bool

theorem Cedar.Thm.wf_term_app_not_exact {εs : SymCC.SymEntities} {t : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.not [t] ty)) : ty = SymCC.TermType.bool ∧ WFArg εs t SymCC.TermType.bool

theorem Cedar.Thm.wf_term_app_string_like {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} {p : Spec.Pattern} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.string.like p) ts ty)) : ty = SymCC.TermType.bool ∧ WFUnary εs ts SymCC.TermType.string

theorem Cedar.Thm.wf_term_app_option_get {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.option.get ts ty)) : WFUnary εs ts ty.option

theorem Cedar.Thm.wf_term_app_ext_decimal_val {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.decimal.val) ts ty)) : ty = SymCC.TermType.bitvec 64 ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.decimal)

theorem Cedar.Thm.wf_term_app_ext_ipaddr_isV4 {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.isV4) ts ty)) : ty = SymCC.TermType.bool ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.ipAddr)

theorem Cedar.Thm.wf_term_app_ext_ipaddr_addrV4 {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.addrV4) ts ty)) : ty = SymCC.TermType.bitvec 32 ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.ipAddr)

theorem Cedar.Thm.wf_term_app_ext_ipaddr_prefixV4 {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.prefixV4) ts ty)) : ty = (SymCC.TermType.bitvec 5).option ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.ipAddr)

theorem Cedar.Thm.wf_term_app_ext_ipaddr_addrV6 {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.addrV6) ts ty)) : ty = SymCC.TermType.bitvec 128 ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.ipAddr)

theorem Cedar.Thm.wf_term_app_ext_ipaddr_prefixV6 {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.prefixV6) ts ty)) : ty = (SymCC.TermType.bitvec 7).option ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.ipAddr)

theorem Cedar.Thm.wf_term_app_ext_datetime_val {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.datetime.val) ts ty)) : ty = SymCC.TermType.bitvec 64 ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.datetime)

theorem Cedar.Thm.wf_term_app_ext_datetime_ofBitVec {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.datetime.ofBitVec) ts ty)) : ty = SymCC.TermType.ext Validation.ExtType.datetime ∧ WFUnary εs ts (SymCC.TermType.bitvec 64)

theorem Cedar.Thm.wf_term_app_ext_duration_val {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.duration.val) ts ty)) : ty = SymCC.TermType.bitvec 64 ∧ WFUnary εs ts (SymCC.TermType.ext Validation.ExtType.duration)

theorem Cedar.Thm.wf_term_app_ext_duration_ofBitVec {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.duration.ofBitVec) ts ty)) : ty = SymCC.TermType.ext Validation.ExtType.duration ∧ WFUnary εs ts (SymCC.TermType.bitvec 64)

theorem Cedar.Thm.wf_term_app_uuf {εs : SymCC.SymEntities} {ts : List SymCC.Term} {f : SymCC.UUF} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.uuf f) ts ty)) : ty = f.out ∧ WFUnary εs ts f.arg ∧ SymCC.UUF.WellFormed εs f

theorem Cedar.Thm.wf_term_app_record_get {εs : SymCC.SymEntities} {ts : List SymCC.Term} {a : Spec.Attr} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.record.get a) ts ty)) : ∃ (rty : Data.Map Spec.Attr SymCC.TermType), rty.find? a = some ty ∧ WFUnary εs ts (SymCC.TermType.record rty)

theorem Cedar.Thm.wf_term_app_and {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.and ts ty)) : ty = SymCC.TermType.bool ∧ WFBinary εs ts SymCC.TermType.bool

theorem Cedar.Thm.wf_term_app_or {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.or ts ty)) : ty = SymCC.TermType.bool ∧ WFBinary εs ts SymCC.TermType.bool

theorem Cedar.Thm.wf_term_app_eq {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.eq ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (ty' : SymCC.TermType), WFBinary εs ts ty'

theorem Cedar.Thm.wf_term_app_ite {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.ite ts ty)) : ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ∃ (t₃ : SymCC.Term), ts = [t₁, t₂, t₃] ∧ WFArg εs t₁ SymCC.TermType.bool ∧ WFArg εs t₂ ty ∧ WFArg εs t₃ ty

theorem Cedar.Thm.wf_term_app_ite_exact {εs : SymCC.SymEntities} {t₁ t₂ t₃ : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.ite [t₁, t₂, t₃] ty)) : WFArg εs t₁ SymCC.TermType.bool ∧ WFArg εs t₂ ty ∧ WFArg εs t₃ ty

theorem Cedar.Thm.wf_term_app_bvneg {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvneg ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFUnary εs ts ty

theorem Cedar.Thm.wf_term_app_bvnego {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvnego ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFUnary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_zero_extend {εs : SymCC.SymEntities} {ts : List SymCC.Term} {n : Nat} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app (SymCC.Op.zero_extend n) ts ty)) : ∃ (m : Nat), ty = SymCC.TermType.bitvec (n + m) ∧ WFUnary εs ts (SymCC.TermType.bitvec m)

theorem Cedar.Thm.wf_term_app_bvadd {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvadd ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvsub {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsub ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvmul {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvmul ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvsdiv {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsdiv ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvudiv {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvudiv ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvsrem {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsrem ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvsmod {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsmod ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvurem {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvurem ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvshl {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvshl ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvlshr {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvlshr ts ty)) : ∃ (n : Nat), ty = SymCC.TermType.bitvec n ∧ WFBinary εs ts ty

theorem Cedar.Thm.wf_term_app_bvsaddo {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsaddo ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_bvssubo {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvssubo ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_bvsmulo {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsmulo ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_bvslt {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvslt ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_bvsle {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvsle ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_bvult {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvult ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_bvule {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.bvule ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (n : Nat), WFBinary εs ts (SymCC.TermType.bitvec n)

theorem Cedar.Thm.wf_term_app_set_subset {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.set.subset ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (ty : SymCC.TermType), WFBinary εs ts ty.set

theorem Cedar.Thm.wf_term_app_set_inter {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.set.inter ts ty)) : ∃ (ty' : SymCC.TermType), ty = ty'.set ∧ WFBinary εs ts ty'.set

theorem Cedar.Thm.wf_term_app_set_member {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app SymCC.Op.set.member ts ty)) : ty = SymCC.TermType.bool ∧ ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ SymCC.Term.WellFormed εs t₁ ∧ WFArg εs t₂ t₁.typeOf.set

theorem Cedar.Thm.wf_arg {εs : SymCC.SymEntities} {t₁ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (t : SymCC.Term) : t ∈ [t₁] → SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_args {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (t : SymCC.Term) : t ∈ [t₁, t₂] → SymCC.Term.WellFormed εs t

theorem Cedar.Thm.wf_arg' {εs : SymCC.SymEntities} {t₁ : SymCC.Term} (h₁ : ∀ (t : SymCC.Term), t ∈ [t₁] → SymCC.Term.WellFormed εs t) : SymCC.Term.WellFormed εs t₁

theorem Cedar.Thm.wf_args' {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h : ∀ (t : SymCC.Term), t ∈ [t₁, t₂] → SymCC.Term.WellFormed εs t) : SymCC.Term.WellFormed εs t₁ ∧ SymCC.Term.WellFormed εs t₂

theorem Cedar.Thm.wf_setOf {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (h₁ : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t) (h₂ : ∀ (t : SymCC.Term), t ∈ ts → t.typeOf = ty) (h₃ : SymCC.TermType.WellFormed εs ty) : SymCC.Term.WellFormed εs (SymCC.Factory.setOf ts ty) ∧ (SymCC.Factory.setOf ts ty).typeOf = ty.set

theorem Cedar.Thm.wf_setOf_map {εs : SymCC.SymEntities} {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} {ty : SymCC.TermType} (hwf : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs (f t) ∧ (f t).typeOf = ty) (hwty : SymCC.TermType.WellFormed εs ty) : SymCC.Term.WellFormed εs (SymCC.Factory.setOf (List.map f ts) ty) ∧ (SymCC.Factory.setOf (List.map f ts) ty).typeOf = ty.set

theorem Cedar.Thm.wf_some_setOf_map {εs : SymCC.SymEntities} {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} {ty : SymCC.TermType} (hwf : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs (f t) ∧ (f t).typeOf = ty) (hwty : SymCC.TermType.WellFormed εs ty) : SymCC.Term.WellFormed εs (SymCC.Factory.setOf (List.map f ts) ty).some ∧ (SymCC.Factory.setOf (List.map f ts) ty).some.typeOf = ty.set.option

theorem Cedar.Thm.wf_recordOf {εs : SymCC.SymEntities} {ats : List (Spec.Attr × SymCC.Term)} (h₁ : ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs t) : SymCC.Term.WellFormed εs (SymCC.Factory.recordOf ats)

theorem Cedar.Thm.wf_recordOf_map {εs : SymCC.SymEntities} {f : SymCC.Term → SymCC.Term} {ats : List (Spec.Attr × SymCC.Term)} (hwf : ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs (f t)) : SymCC.Term.WellFormed εs (SymCC.Factory.recordOf (List.map (Prod.map id f) ats))

theorem Cedar.Thm.wf_some_recordOf_map {εs : SymCC.SymEntities} {f : SymCC.Term → SymCC.Term} {ats : List (Spec.Attr × SymCC.Term)} (hwf : ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs (f t)) : SymCC.Term.WellFormed εs (SymCC.Factory.recordOf (List.map (Prod.map id f) ats)).some ∧ ∃ (ty : SymCC.TermType), (SymCC.Factory.recordOf (List.map (Prod.map id f) ats)).some.typeOf = ty.option

theorem Cedar.Thm.wf_not {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.bool) : SymCC.Term.WellFormed εs (SymCC.Factory.not t) ∧ (SymCC.Factory.not t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_eq {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = t₂.typeOf) : SymCC.Term.WellFormed εs (SymCC.Factory.eq t₁ t₂) ∧ (SymCC.Factory.eq t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_and {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bool) (h₄ : t₂.typeOf = SymCC.TermType.bool) : SymCC.Term.WellFormed εs (SymCC.Factory.and t₁ t₂) ∧ (SymCC.Factory.and t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_or {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bool) (h₄ : t₂.typeOf = SymCC.TermType.bool) : SymCC.Term.WellFormed εs (SymCC.Factory.or t₁ t₂) ∧ (SymCC.Factory.or t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ite {εs : SymCC.SymEntities} {t₁ t₂ t₃ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : SymCC.Term.WellFormed εs t₃) (h₄ : t₁.typeOf = SymCC.TermType.bool) (h₅ : t₂.typeOf = t₃.typeOf) : SymCC.Term.WellFormed εs (SymCC.Factory.ite t₁ t₂ t₃) ∧ (SymCC.Factory.ite t₁ t₂ t₃).typeOf = t₂.typeOf

theorem Cedar.Thm.wf_foldr {α : Type u_1} {εs : SymCC.SymEntities} {xs : List α} {t : SymCC.Term} {f : α → SymCC.Term → SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : ∀ (x : α) (t' : SymCC.Term), x ∈ xs → SymCC.Term.WellFormed εs t' → t'.typeOf = t.typeOf → SymCC.Term.WellFormed εs (f x t') ∧ (f x t').typeOf = t.typeOf) : SymCC.Term.WellFormed εs (List.foldr f t xs) ∧ (List.foldr f t xs).typeOf = t.typeOf

theorem Cedar.Thm.wf_app {εs : SymCC.SymEntities} {t : SymCC.Term} {f : SymCC.UnaryFunction} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = f.argType) (h₃ : SymCC.UnaryFunction.WellFormed εs f) : SymCC.Term.WellFormed εs (SymCC.Factory.app f t) ∧ (SymCC.Factory.app f t).typeOf = f.outType

theorem Cedar.Thm.wf_bvneg {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvneg t) ∧ (SymCC.Factory.bvneg t).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvnego {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvnego t) ∧ (SymCC.Factory.bvnego t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvadd {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvadd t₁ t₂) ∧ (SymCC.Factory.bvadd t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvsub {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsub t₁ t₂) ∧ (SymCC.Factory.bvsub t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvmul {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvmul t₁ t₂) ∧ (SymCC.Factory.bvmul t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvsdiv {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsdiv t₁ t₂) ∧ (SymCC.Factory.bvsdiv t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvudiv {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvudiv t₁ t₂) ∧ (SymCC.Factory.bvudiv t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvsrem {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsrem t₁ t₂) ∧ (SymCC.Factory.bvsrem t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvsmod {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsmod t₁ t₂) ∧ (SymCC.Factory.bvsmod t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvurem {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvurem t₁ t₂) ∧ (SymCC.Factory.bvurem t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvshl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvshl t₁ t₂) ∧ (SymCC.Factory.bvshl t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvlshr {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvlshr t₁ t₂) ∧ (SymCC.Factory.bvlshr t₁ t₂).typeOf = SymCC.TermType.bitvec n

theorem Cedar.Thm.wf_bvsaddo {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsaddo t₁ t₂) ∧ (SymCC.Factory.bvsaddo t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvssubo {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvssubo t₁ t₂) ∧ (SymCC.Factory.bvssubo t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvsmulo {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsmulo t₁ t₂) ∧ (SymCC.Factory.bvsmulo t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvslt {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvslt t₁ t₂) ∧ (SymCC.Factory.bvslt t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvsle {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsle t₁ t₂) ∧ (SymCC.Factory.bvsle t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvult {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvult t₁ t₂) ∧ (SymCC.Factory.bvult t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_bvule {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvule t₁ t₂) ∧ (SymCC.Factory.bvule t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_zero_extend {εs : SymCC.SymEntities} {t : SymCC.Term} {n m : Nat} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.bitvec m) : SymCC.Term.WellFormed εs (SymCC.Factory.zero_extend n t) ∧ (SymCC.Factory.zero_extend n t).typeOf = SymCC.TermType.bitvec (n + m)

theorem Cedar.Thm.wf_set_member {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₂.typeOf = t₁.typeOf.set) : SymCC.Term.WellFormed εs (SymCC.Factory.set.member t₁ t₂) ∧ (SymCC.Factory.set.member t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_set_subset {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = ty.set) (h₄ : t₂.typeOf = ty.set) : SymCC.Term.WellFormed εs (SymCC.Factory.set.subset t₁ t₂) ∧ (SymCC.Factory.set.subset t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_set_inter {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = ty.set) (h₄ : t₂.typeOf = ty.set) : SymCC.Term.WellFormed εs (SymCC.Factory.set.inter t₁ t₂) ∧ (SymCC.Factory.set.inter t₁ t₂).typeOf = ty.set

theorem Cedar.Thm.wf_term_set_empty {εs : SymCC.SymEntities} {ty : SymCC.TermType} (h₁ : SymCC.TermType.WellFormed εs ty) : SymCC.Term.WellFormed εs (SymCC.Term.set Data.Set.empty ty) ∧ (SymCC.Term.set Data.Set.empty ty).typeOf = ty.set

theorem Cedar.Thm.wf_set_isEmpty {εs : SymCC.SymEntities} {t₁ : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : t₁.typeOf = ty.set) : SymCC.Term.WellFormed εs (SymCC.Factory.set.isEmpty t₁) ∧ (SymCC.Factory.set.isEmpty t₁).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_set_intersects {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = ty.set) (h₄ : t₂.typeOf = ty.set) : SymCC.Term.WellFormed εs (SymCC.Factory.set.intersects t₁ t₂) ∧ (SymCC.Factory.set.intersects t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_record_get {a : Spec.Attr} {εs : SymCC.SymEntities} {t : SymCC.Term} {rty : Data.Map Spec.Attr SymCC.TermType} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.record rty) (h₃ : rty.find? a = some ty) : SymCC.Term.WellFormed εs (SymCC.Factory.record.get t a) ∧ (SymCC.Factory.record.get t a).typeOf = ty

theorem Cedar.Thm.wf_option_get {εs : SymCC.SymEntities} {t : SymCC.Term} {ty : SymCC.TermType} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = ty.option) : SymCC.Term.WellFormed εs (SymCC.Factory.option.get t) ∧ (SymCC.Factory.option.get t).typeOf = ty

theorem Cedar.Thm.wf_option_get_mem_of_type {εs : SymCC.SymEntities} {ts : List SymCC.Term} {ty : SymCC.TermType} (hwf : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t) (hty : ∀ (t : SymCC.Term), t ∈ ts → t.typeOf = ty.option) (t : SymCC.Term) : t ∈ ts → SymCC.Term.WellFormed εs (SymCC.Factory.option.get t) ∧ (SymCC.Factory.option.get t).typeOf = ty

theorem Cedar.Thm.wf_option_get_mem_of_type_snd {εs : SymCC.SymEntities} {ats : List (Spec.Attr × SymCC.Term)} (hwf : ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ ats → SymCC.Term.WellFormed εs t ∧ ∃ (ty : SymCC.TermType), t.typeOf = ty.option) (a : Spec.Attr) (t : SymCC.Term) : (a, t) ∈ ats → SymCC.Term.WellFormed εs (SymCC.Factory.option.get t)

theorem Cedar.Thm.wf_option_get' {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {ty : SymCC.TermType} (h₀ : I.WellFormed εs) (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = ty.option) : SymCC.Term.WellFormed εs (SymCC.Factory.option.get' I t) ∧ (SymCC.Factory.option.get' I t).typeOf = ty

theorem Cedar.Thm.wf_string_like {εs : SymCC.SymEntities} {t : SymCC.Term} {p : Spec.Pattern} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.string) : SymCC.Term.WellFormed εs (SymCC.Factory.string.like t p) ∧ (SymCC.Factory.string.like t p).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ext_decimal_val {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.decimal.val t) ∧ (SymCC.Factory.ext.decimal.val t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_ext_ipaddr_isV4 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.ipaddr.isV4 t) ∧ (SymCC.Factory.ext.ipaddr.isV4 t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ext_ipaddr_addrV4 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.ipaddr.addrV4 t) ∧ (SymCC.Factory.ext.ipaddr.addrV4 t).typeOf = SymCC.TermType.bitvec 32

theorem Cedar.Thm.wf_ext_ipaddr_prefixV4 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.ipaddr.prefixV4 t) ∧ (SymCC.Factory.ext.ipaddr.prefixV4 t).typeOf = (SymCC.TermType.bitvec 5).option

theorem Cedar.Thm.wf_ext_ipaddr_addrV6 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.ipaddr.addrV6 t) ∧ (SymCC.Factory.ext.ipaddr.addrV6 t).typeOf = SymCC.TermType.bitvec 128

theorem Cedar.Thm.wf_ext_ipaddr_prefixV6 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.ipaddr.prefixV6 t) ∧ (SymCC.Factory.ext.ipaddr.prefixV6 t).typeOf = (SymCC.TermType.bitvec 7).option

theorem Cedar.Thm.wf_ext_datetime_val {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.datetime.val t) ∧ (SymCC.Factory.ext.datetime.val t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_ext_datetime_ofBitVec {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.prim (SymCC.TermPrimType.bitvec 64)) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.datetime.ofBitVec t) ∧ (SymCC.Factory.ext.datetime.ofBitVec t).typeOf = SymCC.TermType.ext Validation.ExtType.datetime

theorem Cedar.Thm.wf_ext_duration_val {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.duration.val t) ∧ (SymCC.Factory.ext.duration.val t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_ext_duration_ofBitVec {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : t.typeOf = SymCC.TermType.prim (SymCC.TermPrimType.bitvec 64)) : SymCC.Term.WellFormed εs (SymCC.Factory.ext.duration.ofBitVec t) ∧ (SymCC.Factory.ext.duration.ofBitVec t).typeOf = SymCC.TermType.ext Validation.ExtType.duration

theorem Cedar.Thm.wf_isNone {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) : SymCC.Term.WellFormed εs (SymCC.Factory.isNone t) ∧ (SymCC.Factory.isNone t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_isSome {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) : SymCC.Term.WellFormed εs (SymCC.Factory.isSome t) ∧ (SymCC.Factory.isSome t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ifSome_option {εs : SymCC.SymEntities} {g t : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs g → SymCC.Term.WellFormed εs t → t.typeOf = ty.option → SymCC.Term.WellFormed εs (SymCC.Factory.ifSome g t) ∧ (SymCC.Factory.ifSome g t).typeOf = ty.option

theorem Cedar.Thm.wf_ifFalse {εs : SymCC.SymEntities} {g t : SymCC.Term} : SymCC.Term.WellFormed εs g → SymCC.Term.WellFormed εs t → g.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormed εs (SymCC.Factory.ifFalse g t) ∧ (SymCC.Factory.ifFalse g t).typeOf = t.typeOf.option

theorem Cedar.Thm.wf_ifTrue {εs : SymCC.SymEntities} {g t : SymCC.Term} : SymCC.Term.WellFormed εs g → SymCC.Term.WellFormed εs t → g.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormed εs (SymCC.Factory.ifTrue g t) ∧ (SymCC.Factory.ifTrue g t).typeOf = t.typeOf.option

theorem Cedar.Thm.wf_foldl {α : Type u_1} {εs : SymCC.SymEntities} {xs : List α} {t : SymCC.Term} {f : SymCC.Term → α → SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t) (h₂ : ∀ (x : α) (t' : SymCC.Term), x ∈ xs → SymCC.Term.WellFormed εs t' → t'.typeOf = t.typeOf → SymCC.Term.WellFormed εs (f t' x) ∧ (f t' x).typeOf = t.typeOf) : SymCC.Term.WellFormed εs (List.foldl f t xs) ∧ (List.foldl f t xs).typeOf = t.typeOf

theorem Cedar.Thm.wf_foldr_ifSome {εs : SymCC.SymEntities} {ts : List SymCC.Term} {body : SymCC.Term} {ty : SymCC.TermType} (hbody : SymCC.Term.WellFormed εs body) (hbodyty : body.typeOf = ty.option) (hts : ∀ (tᵢ : SymCC.Term), tᵢ ∈ ts → SymCC.Term.WellFormed εs tᵢ) : SymCC.Term.WellFormed εs (List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) body ts) ∧ (List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) body ts).typeOf = ty.option

Folding ifSome guards over an option-typed body preserves well-formedness and the body's option type. Used for the variadic isInRange compilation, which guards the result on every argument being some.

theorem Cedar.Thm.typeOf_foldr_ifSome {ts : List SymCC.Term} {P : SymCC.Term} {ty : SymCC.TermType} (hP : P.typeOf = ty.option) : (List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) P ts).typeOf = ty.option

Folding ifSome guards over an option-typed body preserves the body's option type.

theorem Cedar.Thm.wf_anyTrue {εs : SymCC.SymEntities} {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} : (∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs (f t) ∧ (f t).typeOf = SymCC.TermType.bool) → SymCC.Term.WellFormed εs (SymCC.Factory.anyTrue f ts) ∧ (SymCC.Factory.anyTrue f ts).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_anyNone {εs : SymCC.SymEntities} {gs : List SymCC.Term} : (∀ (g : SymCC.Term), g ∈ gs → SymCC.Term.WellFormed εs g) → SymCC.Term.WellFormed εs (SymCC.Factory.anyNone gs) ∧ (SymCC.Factory.anyNone gs).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ifAllSome {εs : SymCC.SymEntities} {gs : List SymCC.Term} {t : SymCC.Term} {ty : SymCC.TermType} : (∀ (g : SymCC.Term), g ∈ gs → SymCC.Term.WellFormed εs g) → SymCC.Term.WellFormed εs t → t.typeOf = ty.option → SymCC.Term.WellFormed εs (SymCC.Factory.ifAllSome gs t) ∧ (SymCC.Factory.ifAllSome gs t).typeOf = ty.option

theorem Cedar.Thm.wf_bvaddChecked {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvaddChecked t₁ t₂) ∧ (SymCC.Factory.bvaddChecked t₁ t₂).typeOf = (SymCC.TermType.bitvec n).option

theorem Cedar.Thm.wf_bvsubChecked {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvsubChecked t₁ t₂) ∧ (SymCC.Factory.bvsubChecked t₁ t₂).typeOf = (SymCC.TermType.bitvec n).option

theorem Cedar.Thm.wf_bvmulChecked {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} (h₁ : SymCC.Term.WellFormed εs t₁) (h₂ : SymCC.Term.WellFormed εs t₂) (h₃ : t₁.typeOf = SymCC.TermType.bitvec n) (h₄ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.WellFormed εs (SymCC.Factory.bvmulChecked t₁ t₂) ∧ (SymCC.Factory.bvmulChecked t₁ t₂).typeOf = (SymCC.TermType.bitvec n).option

theorem Cedar.Thm.wf_decimal_lessThan {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) : SymCC.Term.WellFormed εs (SymCC.Decimal.lessThan t₁ t₂) ∧ (SymCC.Decimal.lessThan t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_decimal_lessThanOrEqual {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) : SymCC.Term.WellFormed εs (SymCC.Decimal.lessThanOrEqual t₁ t₂) ∧ (SymCC.Decimal.lessThanOrEqual t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_decimal_greaterThan {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) : SymCC.Term.WellFormed εs (SymCC.Decimal.greaterThan t₁ t₂) ∧ (SymCC.Decimal.greaterThan t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_decimal_greaterThanOrEqual {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.decimal) : SymCC.Term.WellFormed εs (SymCC.Decimal.greaterThanOrEqual t₁ t₂) ∧ (SymCC.Decimal.greaterThanOrEqual t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_isIpv4 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.isIpv4 t) ∧ (SymCC.IPAddr.isIpv4 t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_isIpv6 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.isIpv6 t) ∧ (SymCC.IPAddr.isIpv6 t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_subnetWidth {εs : SymCC.SymEntities} {w : Nat} {ipPre : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs ipPre ∧ ipPre.typeOf = (SymCC.TermType.bitvec w).option) : SymCC.Term.WellFormed εs (SymCC.IPAddr.subnetWidth w ipPre) ∧ (SymCC.IPAddr.subnetWidth w ipPre).typeOf = SymCC.TermType.bitvec (Spec.Ext.IPAddr.ADDR_SIZE w)

def Cedar.Thm.WFIPRange (εs : SymCC.SymEntities) (p : SymCC.Term × SymCC.Term) (w : Nat) : Prop

Equations

• Cedar.Thm.WFIPRange εs p w = (Cedar.Thm.WFArg εs p.fst (Cedar.SymCC.TermType.bitvec w) ∧ Cedar.Thm.WFArg εs p.snd (Cedar.SymCC.TermType.bitvec w))

theorem Cedar.Thm.wf_ipaddr_range {εs : SymCC.SymEntities} {w : Nat} {ipAddr ipPre : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs ipAddr ∧ ipAddr.typeOf = SymCC.TermType.bitvec (Spec.Ext.IPAddr.ADDR_SIZE w)) (h₂ : SymCC.Term.WellFormed εs ipPre ∧ ipPre.typeOf = (SymCC.TermType.bitvec w).option) : WFIPRange εs (SymCC.IPAddr.range w ipAddr ipPre) (Spec.Ext.IPAddr.ADDR_SIZE w)

theorem Cedar.Thm.wf_ipaddr_rangeV4 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : WFIPRange εs (SymCC.IPAddr.rangeV4 t) (Spec.Ext.IPAddr.ADDR_SIZE Spec.Ext.IPAddr.V4_WIDTH)

theorem Cedar.Thm.wf_ipaddr_rangeV6 {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : WFIPRange εs (SymCC.IPAddr.rangeV6 t) (Spec.Ext.IPAddr.ADDR_SIZE Spec.Ext.IPAddr.V6_WIDTH)

theorem Cedar.Thm.wf_ipaddr_inRange {εs : SymCC.SymEntities} {w : Nat} {range : SymCC.Term → SymCC.Term × SymCC.Term} {t₁ t₂ : SymCC.Term} (h₁ : WFIPRange εs (range t₁) w) (h₂ : WFIPRange εs (range t₂) w) : SymCC.Term.WellFormed εs (SymCC.IPAddr.inRange range t₁ t₂) ∧ (SymCC.IPAddr.inRange range t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_inRangeV {εs : SymCC.SymEntities} {w : Nat} {isIp : SymCC.Term → SymCC.Term} {rangeV : SymCC.Term → SymCC.Term × SymCC.Term} {t₁ t₂ : SymCC.Term} (h₁ : WFIPRange εs (rangeV t₁) w) (h₂ : WFIPRange εs (rangeV t₂) w) (h₃ : SymCC.Term.WellFormed εs (isIp t₁) ∧ (isIp t₁).typeOf = SymCC.TermType.bool) (h₄ : SymCC.Term.WellFormed εs (isIp t₂) ∧ (isIp t₂).typeOf = SymCC.TermType.bool) : SymCC.Term.WellFormed εs (SymCC.IPAddr.inRangeV isIp rangeV t₁ t₂) ∧ (SymCC.IPAddr.inRangeV isIp rangeV t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_isInRange {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.isInRange t₁ t₂) ∧ (SymCC.IPAddr.isInRange t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_inRangeVs {εs : SymCC.SymEntities} {w : Nat} {isIp : SymCC.Term → SymCC.Term} {range : SymCC.Term → SymCC.Term × SymCC.Term} {t : SymCC.Term} {ts : List SymCC.Term} (hrt : WFIPRange εs (range t) w) (hit : SymCC.Term.WellFormed εs (isIp t) ∧ (isIp t).typeOf = SymCC.TermType.bool) (hrs : ∀ (t₂ : SymCC.Term), t₂ ∈ ts → WFIPRange εs (range t₂) w) (his : ∀ (t₂ : SymCC.Term), t₂ ∈ ts → SymCC.Term.WellFormed εs (isIp t₂) ∧ (isIp t₂).typeOf = SymCC.TermType.bool) : SymCC.Term.WellFormed εs (SymCC.IPAddr.inRangeVs isIp range t ts) ∧ (SymCC.IPAddr.inRangeVs isIp range t ts).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_isInRangeV {εs : SymCC.SymEntities} {t₁ : SymCC.Term} {ts : List SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) (h₂ : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.isInRangeV t₁ ts) ∧ (SymCC.IPAddr.isInRangeV t₁ ts).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_ipTerm (εs : SymCC.SymEntities) (ip : Spec.IPAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.ipTerm ip) ∧ (SymCC.IPAddr.ipTerm ip).typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr

theorem Cedar.Thm.wf_ipaddr_isLoopback {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.isLoopback t) ∧ (SymCC.IPAddr.isLoopback t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_ipaddr_isMulticast {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr) : SymCC.Term.WellFormed εs (SymCC.IPAddr.isMulticast t) ∧ (SymCC.IPAddr.isMulticast t).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_datetime_offset {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.datetime) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Datetime.offset t₁ t₂) ∧ (SymCC.Datetime.offset t₁ t₂).typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option

theorem Cedar.Thm.wf_datetime_durationSince {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t₁ ∧ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.datetime) (h₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.datetime) : SymCC.Term.WellFormed εs (SymCC.Datetime.durationSince t₁ t₂) ∧ (SymCC.Datetime.durationSince t₁ t₂).typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option

theorem Cedar.Thm.wf_datetime_toDate {εs : SymCC.SymEntities} {t : SymCC.Term} (h : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime) : SymCC.Term.WellFormed εs (SymCC.Datetime.toDate t) ∧ (SymCC.Datetime.toDate t).typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option

theorem Cedar.Thm.wf_datetime_toTime {εs : SymCC.SymEntities} {t : SymCC.Term} (h : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime) : SymCC.Term.WellFormed εs (SymCC.Datetime.toTime t) ∧ (SymCC.Datetime.toTime t).typeOf = SymCC.TermType.ext Validation.ExtType.duration

theorem Cedar.Thm.wf_duration_toMilliseconds {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Duration.toMilliseconds t) ∧ (SymCC.Duration.toMilliseconds t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_duration_toSeconds {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Duration.toSeconds t) ∧ (SymCC.Duration.toSeconds t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_duration_toMinutes {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Duration.toMinutes t) ∧ (SymCC.Duration.toMinutes t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_duration_toHours {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Duration.toHours t) ∧ (SymCC.Duration.toHours t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_duration_toDays {εs : SymCC.SymEntities} {t : SymCC.Term} (h₁ : SymCC.Term.WellFormed εs t ∧ t.typeOf = SymCC.TermType.ext Validation.ExtType.duration) : SymCC.Term.WellFormed εs (SymCC.Duration.toDays t) ∧ (SymCC.Duration.toDays t).typeOf = SymCC.TermType.bitvec 64

theorem Cedar.Thm.wf_tags_hasTag {εs : SymCC.SymEntities} {τs : SymCC.SymTags} {t₁ t₂ : SymCC.Term} {ety : Spec.EntityType} (hwτ : SymCC.SymTags.WellFormed εs ety τs) (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.entity ety) (hty₂ : t₂.typeOf = SymCC.TermType.string) : SymCC.Term.WellFormed εs (τs.hasTag t₁ t₂) ∧ (τs.hasTag t₁ t₂).typeOf = SymCC.TermType.bool

theorem Cedar.Thm.wf_tagOf {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ety : Spec.EntityType} (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.entity ety) (hty₂ : t₂.typeOf = SymCC.TermType.string) : SymCC.Term.WellFormed εs (SymCC.Factory.tagOf t₁ t₂) ∧ (SymCC.Factory.tagOf t₁ t₂).typeOf = SymCC.TermType.tagFor ety

theorem Cedar.Thm.wf_tags_getTag! {εs : SymCC.SymEntities} {τs : SymCC.SymTags} {t₁ t₂ : SymCC.Term} {ety : Spec.EntityType} (hwτ : SymCC.SymTags.WellFormed εs ety τs) (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.entity ety) (hty₂ : t₂.typeOf = SymCC.TermType.string) : SymCC.Term.WellFormed εs (τs.getTag! t₁ t₂) ∧ (τs.getTag! t₁ t₂).typeOf = τs.vals.outType

theorem Cedar.Thm.wf_tags_getTag {εs : SymCC.SymEntities} {τs : SymCC.SymTags} {t₁ t₂ : SymCC.Term} {ety : Spec.EntityType} (hwτ : SymCC.SymTags.WellFormed εs ety τs) (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.entity ety) (hty₂ : t₂.typeOf = SymCC.TermType.string) : SymCC.Term.WellFormed εs (τs.getTag t₁ t₂) ∧ (τs.getTag t₁ t₂).typeOf = τs.vals.outType.option