Interpretation of Factory functions

This file basic lemmas about the interpretation of Factory functions.

theorem Cedar.Thm.interpret_not {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.not t) = SymCC.Factory.not (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_and {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → t₁.typeOf = SymCC.TermType.bool → t₂.typeOf = SymCC.TermType.bool → SymCC.Term.interpret I (SymCC.Factory.and t₁ t₂) = SymCC.Factory.and (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_or {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → t₁.typeOf = SymCC.TermType.bool → t₂.typeOf = SymCC.TermType.bool → SymCC.Term.interpret I (SymCC.Factory.or t₁ t₂) = SymCC.Factory.or (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_ite {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ t₃ : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → SymCC.Term.WellFormed εs t₃ → t₁.typeOf = SymCC.TermType.bool → t₂.typeOf = t₃.typeOf → SymCC.Term.interpret I (SymCC.Factory.ite t₁ t₂ t₃) = SymCC.Factory.ite (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂) (SymCC.Term.interpret I t₃)

theorem Cedar.Thm.interpret_implies {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → t₁.typeOf = SymCC.TermType.bool → t₂.typeOf = SymCC.TermType.bool → SymCC.Term.interpret I (SymCC.Factory.implies t₁ t₂) = SymCC.Factory.implies (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_eq {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → SymCC.Term.interpret I (SymCC.Factory.eq t₁ t₂) = SymCC.Factory.eq (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_isNone {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.isNone t) = SymCC.Factory.isNone (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_isSome {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.isSome t) = SymCC.Factory.isSome (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_noneOf {I : SymCC.Interpretation} {ty : SymCC.TermType} : SymCC.Term.interpret I (SymCC.Factory.noneOf ty) = SymCC.Term.none ty

theorem Cedar.Thm.interpret_someOf {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (⊙t) = (SymCC.Term.interpret I t).some

theorem Cedar.Thm.interpret_option_get {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs t → t.typeOf = ty.option → SymCC.Term.interpret I (SymCC.Factory.option.get t) = SymCC.Factory.option.get' I (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_option_get' {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {ty : SymCC.TermType} : I.WellFormed εs → SymCC.Term.WellFormed εs t → t.typeOf = ty.option → SymCC.Term.interpret I (SymCC.Factory.option.get' I t) = SymCC.Factory.option.get' I (SymCC.Term.interpret I t)

theorem Cedar.Thm.map_interpret_option_get {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ty : SymCC.TermType} {ts : List SymCC.Term} (hts : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t ∧ t.typeOf = ty.option) : List.map (SymCC.Term.interpret I) (List.map SymCC.Factory.option.get ts) = List.map (SymCC.Factory.option.get' I) (List.map (SymCC.Term.interpret I) ts)

map (interpret ∘ option.get) commutes with map (option.get' ∘ interpret).

theorem Cedar.Thm.interpret_record_get {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t : SymCC.Term} {a : Spec.Attr} {rty : Data.Map Spec.Attr SymCC.TermType} {ty : SymCC.TermType} : SymCC.Term.WellFormed εs t → t.typeOf = SymCC.TermType.record rty → rty.find? a = some ty → SymCC.Term.interpret I (SymCC.Factory.record.get t a) = SymCC.Factory.record.get (SymCC.Term.interpret I t) a

theorem Cedar.Thm.interpret_app {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {f : SymCC.UnaryFunction} : I.WellFormed εs → SymCC.Term.WellFormed εs t → SymCC.UnaryFunction.WellFormed εs f → t.typeOf = f.argType → SymCC.Term.interpret I (SymCC.Factory.app f t) = SymCC.Factory.app (SymCC.UnaryFunction.interpret I f) (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ifFalse {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {g t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs g → g.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.ifFalse g t) = SymCC.Factory.ifFalse (SymCC.Term.interpret I g) (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ifTrue {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {g t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs g → g.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.ifTrue g t) = SymCC.Factory.ifTrue (SymCC.Term.interpret I g) (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ifSome {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {g t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs g → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.ifSome g t) = SymCC.Factory.ifSome (SymCC.Term.interpret I g) (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_foldr_ifSome {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ty : SymCC.TermType} {P : SymCC.Term} (hI : I.WellFormed εs) (hP : SymCC.Term.WellFormed εs P) (hPty : P.typeOf = ty.option) (ts : List SymCC.Term) : (∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t) → SymCC.Term.interpret I (List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) P ts) = List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) (SymCC.Term.interpret I P) (List.map (SymCC.Term.interpret I) ts)

Push interpret through a foldr ifSome over well-formed guards.

theorem Cedar.Thm.interpret_string_like {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {p : Spec.Pattern} : I.WellFormed εs → SymCC.Term.WellFormed εs t → t.typeOf = SymCC.TermType.string → SymCC.Term.interpret I (SymCC.Factory.string.like t p) = SymCC.Factory.string.like (SymCC.Term.interpret I t) p

theorem Cedar.Thm.interpret_bvnego {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {n : Nat} : I.WellFormed εs → SymCC.Term.WellFormed εs t → t.typeOf = SymCC.TermType.bitvec n → SymCC.Term.interpret I (SymCC.Factory.bvnego t) = SymCC.Factory.bvnego (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_bvneg {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {n : Nat} : I.WellFormed εs → SymCC.Term.WellFormed εs t → t.typeOf = SymCC.TermType.bitvec n → SymCC.Term.interpret I (SymCC.Factory.bvneg t) = SymCC.Factory.bvneg (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_bvslt {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvslt t₁ t₂) = SymCC.Factory.bvslt (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsle {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsle t₁ t₂) = SymCC.Factory.bvsle (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvule {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvule t₁ t₂) = SymCC.Factory.bvule (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsaddo {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsaddo t₁ t₂) = SymCC.Factory.bvsaddo (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvssubo {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvssubo t₁ t₂) = SymCC.Factory.bvssubo (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsmulo {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsmulo t₁ t₂) = SymCC.Factory.bvsmulo (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvadd {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvadd t₁ t₂) = SymCC.Factory.bvadd (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsub {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsub t₁ t₂) = SymCC.Factory.bvsub (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvmul {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvmul t₁ t₂) = SymCC.Factory.bvmul (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsdiv {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsdiv t₁ t₂) = SymCC.Factory.bvsdiv (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvudiv {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvudiv t₁ t₂) = SymCC.Factory.bvudiv (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsrem {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsrem t₁ t₂) = SymCC.Factory.bvsrem (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsmod {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvsmod t₁ t₂) = SymCC.Factory.bvsmod (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvurem {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvurem t₁ t₂) = SymCC.Factory.bvurem (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvshl {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvshl t₁ t₂) = SymCC.Factory.bvshl (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvlshr {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.bvlshr t₁ t₂) = SymCC.Factory.bvlshr (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvaddChecked {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {n : Nat} (hI : I.WellFormed εs) (hwf₁ : SymCC.Term.WellFormed εs t₁) (hwf₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.bitvec n) (hty₂ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.interpret I (SymCC.Factory.bvaddChecked t₁ t₂) = SymCC.Factory.bvaddChecked (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvsubChecked {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {n : Nat} (hI : I.WellFormed εs) (hwf₁ : SymCC.Term.WellFormed εs t₁) (hwf₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.bitvec n) (hty₂ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.interpret I (SymCC.Factory.bvsubChecked t₁ t₂) = SymCC.Factory.bvsubChecked (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_bvmulChecked {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {n : Nat} (hI : I.WellFormed εs) (hwf₁ : SymCC.Term.WellFormed εs t₁) (hwf₂ : SymCC.Term.WellFormed εs t₂) (hty₁ : t₁.typeOf = SymCC.TermType.bitvec n) (hty₂ : t₂.typeOf = SymCC.TermType.bitvec n) : SymCC.Term.interpret I (SymCC.Factory.bvmulChecked t₁ t₂) = SymCC.Factory.bvmulChecked (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_zero_extend {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {n : Nat} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormed εs t → SymCC.Term.interpret I (SymCC.Factory.zero_extend n t) = SymCC.Factory.zero_extend n (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_set_member {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → SymCC.Term.interpret I (SymCC.Factory.set.member t₁ t₂) = SymCC.Factory.set.member (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_set_subset {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → SymCC.Term.interpret I (SymCC.Factory.set.subset t₁ t₂) = SymCC.Factory.set.subset (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_set_inter {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → t₁.typeOf = ty.set → t₂.typeOf = ty.set → SymCC.Term.interpret I (SymCC.Factory.set.inter t₁ t₂) = SymCC.Factory.set.inter (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

theorem Cedar.Thm.interpret_set_isEmpty {I : SymCC.Interpretation} {εs : SymCC.SymEntities} {t : SymCC.Term} {ty : SymCC.TermType} : I.WellFormed εs → SymCC.Term.WellFormed εs t → t.typeOf = ty.set → SymCC.Term.interpret I (SymCC.Factory.set.isEmpty t) = SymCC.Factory.set.isEmpty (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_set_intersects {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} : I.WellFormed εs → SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → t₁.typeOf = ty.set → t₂.typeOf = ty.set → SymCC.Term.interpret I (SymCC.Factory.set.intersects t₁ t₂) = SymCC.Factory.set.intersects (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)

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

theorem Cedar.Thm.interpret_anyNone {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {gs : List SymCC.Term} : I.WellFormed εs → (∀ (g : SymCC.Term), g ∈ gs → SymCC.Term.WellFormed εs g) → SymCC.Term.interpret I (SymCC.Factory.anyNone gs) = SymCC.Factory.anyNone (List.map (SymCC.Term.interpret I) gs)

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

theorem Cedar.Thm.interpret_setOf {I : SymCC.Interpretation} {ts : List SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.interpret I (SymCC.Factory.setOf ts ty) = SymCC.Factory.setOf (List.map (SymCC.Term.interpret I) ts) ty

theorem Cedar.Thm.interpret_recordOf {I : SymCC.Interpretation} {ats : List (Spec.Attr × SymCC.Term)} : SymCC.Term.interpret I (SymCC.Factory.recordOf ats) = SymCC.Factory.recordOf (List.map (Prod.map id (SymCC.Term.interpret I)) ats)

theorem Cedar.Thm.interpret_ext_decimal_val {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.decimal.val t) = SymCC.Factory.ext.decimal.val (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_ipaddr_isV4 {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.ipaddr.isV4 t) = SymCC.Factory.ext.ipaddr.isV4 (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_ipaddr_addrV4 {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.ipaddr.addrV4 t) = SymCC.Factory.ext.ipaddr.addrV4' I (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_ipaddr_prefixV4 {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.ipaddr.prefixV4 t) = SymCC.Factory.ext.ipaddr.prefixV4' I (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_ipaddr_addrV6 {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.ipaddr.addrV6 t) = SymCC.Factory.ext.ipaddr.addrV6' I (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_ipaddr_prefixV6 {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.ipaddr.prefixV6 t) = SymCC.Factory.ext.ipaddr.prefixV6' I (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_datetime_val {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.datetime.val t) = SymCC.Factory.ext.datetime.val (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_datetime_ofBitVec {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.datetime.ofBitVec t) = SymCC.Factory.ext.datetime.ofBitVec (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_duration_val {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.duration.val t) = SymCC.Factory.ext.duration.val (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_ext_duration_ofBitVec {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.ext.duration.ofBitVec t) = SymCC.Factory.ext.duration.ofBitVec (SymCC.Term.interpret I t)

theorem Cedar.Thm.interpret_tagOf {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} : SymCC.Term.interpret I (SymCC.Factory.tagOf t₁ t₂) = SymCC.Factory.tagOf (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)