This file proves inversion lemmas for compile.

def Cedar.Thm.CompileIfSym (t t₁ : SymCC.Term) (r₂ r₃ : SymCC.Result SymCC.Term) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.compile_ite_ok_implies {x₁ x₂ x₃ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : SymCC.compile (x₁.ite x₂ x₃) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ match t₁ with | (SymCC.Term.prim (SymCC.TermPrim.bool true)).some => Except.ok t = SymCC.compile x₂ εnv | (SymCC.Term.prim (SymCC.TermPrim.bool false)).some => Except.ok t = SymCC.compile x₃ εnv | t₁ => CompileIfSym t t₁ (SymCC.compile x₂ εnv) (SymCC.compile x₃ εnv)

def Cedar.Thm.CompileAndSym (t t₁ : SymCC.Term) (r₂ : SymCC.Result SymCC.Term) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.compile_and_ok_implies {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : SymCC.compile (x₁.and x₂) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ match t₁ with | (SymCC.Term.prim (SymCC.TermPrim.bool false)).some => t = t₁ | x => CompileAndSym t t₁ (SymCC.compile x₂ εnv)

def Cedar.Thm.CompileOrSym (t t₁ : SymCC.Term) (r₂ : SymCC.Result SymCC.Term) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.compile_or_ok_implies {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : SymCC.compile (x₁.or x₂) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ match t₁ with | (SymCC.Term.prim (SymCC.TermPrim.bool true)).some => t = t₁ | x => CompileOrSym t t₁ (SymCC.compile x₂ εnv)

theorem Cedar.Thm.compileAttrsOf_ok_implies {t t₁ : SymCC.Term} {εs : SymCC.SymEntities} (h₁ : SymCC.compileAttrsOf t₁ εs = Except.ok t) : (∃ (rty : Data.Map Spec.Attr SymCC.TermType), t₁.typeOf = SymCC.TermType.record rty ∧ t = t₁) ∨ ∃ (ety : Spec.EntityType), ∃ (fₐ : SymCC.UnaryFunction), t₁.typeOf = SymCC.TermType.entity ety ∧ εs.attrs ety = some fₐ ∧ t = SymCC.Factory.app fₐ t₁

def Cedar.Thm.RecordHasAttr (t t₁ : SymCC.Term) (rty : Data.Map Spec.Attr SymCC.TermType) (a : Spec.Attr) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.compileHasAttr_ok_implies {t t₁ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} (h₁ : SymCC.compileHasAttr t₁ a εs = Except.ok t) : ∃ (t₂ : SymCC.Term), ∃ (rty : Data.Map Spec.Attr SymCC.TermType), SymCC.compileAttrsOf t₁ εs = Except.ok t₂ ∧ RecordHasAttr t t₂ rty a

theorem Cedar.Thm.compile_hasAttr_ok_implies {a : Spec.Attr} {x₁ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : SymCC.compile (x₁.hasAttr a) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ SymCC.compileHasAttr (SymCC.Factory.option.get t₁) a εnv.entities = Except.ok t₂ ∧ t = SymCC.Factory.ifSome t₁ t₂

def Cedar.Thm.RecordGetAttr (t t₁ : SymCC.Term) (rty : Data.Map Spec.Attr SymCC.TermType) (a : Spec.Attr) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.compileGetAttr_ok_implies {t t₁ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} (h₁ : SymCC.compileGetAttr t₁ a εs = Except.ok t) : ∃ (t₂ : SymCC.Term), ∃ (rty : Data.Map Spec.Attr SymCC.TermType), SymCC.compileAttrsOf t₁ εs = Except.ok t₂ ∧ RecordGetAttr t t₂ rty a

theorem Cedar.Thm.compile_getAttr_ok_implies {a : Spec.Attr} {x₁ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : SymCC.compile (x₁.getAttr a) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ SymCC.compileGetAttr (SymCC.Factory.option.get t₁) a εnv.entities = Except.ok t₂ ∧ t = SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.compileApp₁_ok_implies {op₁ : Spec.UnaryOp} {t t₁ : SymCC.Term} (h₁ : SymCC.compileApp₁ op₁ t₁ = Except.ok t) : match op₁, h₁ with | Spec.UnaryOp.not, h₁ => t₁.typeOf = SymCC.TermType.bool ∧ t = (SymCC.Factory.not t₁).some | Spec.UnaryOp.neg, h₁ => t₁.typeOf = SymCC.TermType.bitvec 64 ∧ t = SymCC.Factory.ifFalse (SymCC.Factory.bvnego t₁) (SymCC.Factory.bvneg t₁) | Spec.UnaryOp.like p, h₁ => t₁.typeOf = SymCC.TermType.string ∧ t = (SymCC.Factory.string.like t₁ p).some | Spec.UnaryOp.is ety₁, h₁ => ∃ (ety₂ : Spec.EntityType), t₁.typeOf = SymCC.TermType.entity ety₂ ∧ t = (SymCC.Term.prim (SymCC.TermPrim.bool (decide (ety₁ = ety₂)))).some | Spec.UnaryOp.isEmpty, h₁ => (∃ (ty : SymCC.TermType), t₁.typeOf = ty.set) ∧ t = (SymCC.Factory.set.isEmpty t₁).some

theorem Cedar.Thm.compile_unaryApp_ok_implies {op₁ : Spec.UnaryOp} {x₁ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : SymCC.compile (Spec.Expr.unaryApp op₁ x₁) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ SymCC.compileApp₁ op₁ (SymCC.Factory.option.get t₁) = Except.ok t₂ ∧ t = SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.compileApp₂_less_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.less t₁ t₂ εs = Except.ok t → t₁.typeOf = SymCC.TermType.bitvec 64 ∧ t₂.typeOf = SymCC.TermType.bitvec 64 ∧ t = (SymCC.Factory.bvslt t₁ t₂).some ∨ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.duration ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.duration ∧ t = (SymCC.Factory.bvslt (SymCC.Factory.ext.duration.val t₁) (SymCC.Factory.ext.duration.val t₂)).some ∨ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.datetime ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.datetime ∧ t = (SymCC.Factory.bvslt (SymCC.Factory.ext.datetime.val t₁) (SymCC.Factory.ext.datetime.val t₂)).some

theorem Cedar.Thm.compileApp₂_lessEq_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.lessEq t₁ t₂ εs = Except.ok t → t₁.typeOf = SymCC.TermType.bitvec 64 ∧ t₂.typeOf = SymCC.TermType.bitvec 64 ∧ t = (SymCC.Factory.bvsle t₁ t₂).some ∨ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.duration ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.duration ∧ t = (SymCC.Factory.bvsle (SymCC.Factory.ext.duration.val t₁) (SymCC.Factory.ext.duration.val t₂)).some ∨ t₁.typeOf = SymCC.TermType.ext Validation.ExtType.datetime ∧ t₂.typeOf = SymCC.TermType.ext Validation.ExtType.datetime ∧ t = (SymCC.Factory.bvsle (SymCC.Factory.ext.datetime.val t₁) (SymCC.Factory.ext.datetime.val t₂)).some

theorem Cedar.Thm.compileApp₂_add_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.add t₁ t₂ εs = Except.ok t → t₁.typeOf = SymCC.TermType.bitvec 64 ∧ t₂.typeOf = SymCC.TermType.bitvec 64 ∧ t = SymCC.Factory.ifFalse (SymCC.Factory.bvsaddo t₁ t₂) (SymCC.Factory.bvadd t₁ t₂)

theorem Cedar.Thm.compileApp₂_sub_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.sub t₁ t₂ εs = Except.ok t → t₁.typeOf = SymCC.TermType.bitvec 64 ∧ t₂.typeOf = SymCC.TermType.bitvec 64 ∧ t = SymCC.Factory.ifFalse (SymCC.Factory.bvssubo t₁ t₂) (SymCC.Factory.bvsub t₁ t₂)

theorem Cedar.Thm.compileApp₂_mul_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.mul t₁ t₂ εs = Except.ok t → t₁.typeOf = SymCC.TermType.bitvec 64 ∧ t₂.typeOf = SymCC.TermType.bitvec 64 ∧ t = SymCC.Factory.ifFalse (SymCC.Factory.bvsmulo t₁ t₂) (SymCC.Factory.bvmul t₁ t₂)

theorem Cedar.Thm.reducibleEq_ok_false_implies {ty₁ ty₂ : SymCC.TermType} : SymCC.reducibleEq ty₁ ty₂ = Except.ok false → ¬ty₁ = ty₂ ∧ ty₁.isPrimType = true ∧ ty₂.isPrimType = true

theorem Cedar.Thm.reducibleEq_ok_true_implies {ty₁ ty₂ : SymCC.TermType} : SymCC.reducibleEq ty₁ ty₂ = Except.ok true → ty₁ = ty₂

theorem Cedar.Thm.compileApp₂_eq_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.eq t₁ t₂ εs = Except.ok t → SymCC.reducibleEq t₁.typeOf t₂.typeOf = Except.ok true ∧ t = (SymCC.Factory.eq t₁ t₂).some ∨ SymCC.reducibleEq t₁.typeOf t₂.typeOf = Except.ok false ∧ t = (SymCC.Term.prim (SymCC.TermPrim.bool false)).some

theorem Cedar.Thm.compileApp₂_contains_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.contains t₁ t₂ εs = Except.ok t → t₁.typeOf = t₂.typeOf.set ∧ t = (SymCC.Factory.set.member t₂ t₁).some

theorem Cedar.Thm.compileApp₂_containsAll_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.containsAll t₁ t₂ εs = Except.ok t → ∃ (ty : SymCC.TermType), t₁.typeOf = ty.set ∧ t₂.typeOf = ty.set ∧ t = (SymCC.Factory.set.subset t₂ t₁).some

theorem Cedar.Thm.compileApp₂_containsAny_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.containsAny t₁ t₂ εs = Except.ok t → ∃ (ty : SymCC.TermType), t₁.typeOf = ty.set ∧ t₂.typeOf = ty.set ∧ t = (SymCC.Factory.set.intersects t₁ t₂).some

theorem Cedar.Thm.compileHasTag_ok_implies {t t₁ t₂ : SymCC.Term} {tags : Option (Option SymCC.SymTags)} : SymCC.compileHasTag t₁ t₂ tags = Except.ok t → tags = some none ∧ t = (SymCC.Term.prim (SymCC.TermPrim.bool false)).some ∨ ∃ (τs : SymCC.SymTags), tags = some (some τs) ∧ t = (τs.hasTag t₁ t₂).some

theorem Cedar.Thm.compileApp₂_hasTag_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.hasTag t₁ t₂ εs = Except.ok t → ∃ (ety : Spec.EntityType), t₁.typeOf = SymCC.TermType.entity ety ∧ t₂.typeOf = SymCC.TermType.string ∧ SymCC.compileHasTag t₁ t₂ (εs.tags ety) = Except.ok t

theorem Cedar.Thm.compileGetTag_ok_implies {t t₁ t₂ : SymCC.Term} {tags : Option (Option SymCC.SymTags)} : SymCC.compileGetTag t₁ t₂ tags = Except.ok t → ∃ (τs : SymCC.SymTags), tags = some (some τs) ∧ t = τs.getTag t₁ t₂

theorem Cedar.Thm.compileApp₂_getTag_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.getTag t₁ t₂ εs = Except.ok t → ∃ (ety : Spec.EntityType), t₁.typeOf = SymCC.TermType.entity ety ∧ t₂.typeOf = SymCC.TermType.string ∧ SymCC.compileGetTag t₁ t₂ (εs.tags ety) = Except.ok t

def Cedar.Thm.compileInₑ.isEq (t₁ t₂ : SymCC.Term) : SymCC.Term

Equations

• Cedar.Thm.compileInₑ.isEq t₁ t₂ = if t₁.typeOf = t₂.typeOf then Cedar.SymCC.Factory.eq t₁ t₂ else Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

theorem Cedar.Thm.compileInₑ.isEq_def {t₁ t₂ : SymCC.Term} : isEq t₁ t₂ = SymCC.compileInₑ.isEq t₁ t₂

def Cedar.Thm.compileInₑ.isIn (t₁ t₂ : SymCC.Term) (ancs? : Option SymCC.UnaryFunction) : SymCC.Term

Equations

• Cedar.Thm.compileInₑ.isIn t₁ t₂ (some ancs) = Cedar.SymCC.Factory.set.member t₂ (Cedar.SymCC.Factory.app ancs t₁)
• Cedar.Thm.compileInₑ.isIn t₁ t₂ none = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

theorem Cedar.Thm.compileInₑ.isIn_def {t₁ t₂ : SymCC.Term} {ancs? : Option SymCC.UnaryFunction} : isIn t₁ t₂ ancs? = SymCC.compileInₑ.isIn t₁ t₂ ancs?

theorem Cedar.Thm.compileInₑ_def {t₁ t₂ : SymCC.Term} {ancs? : Option SymCC.UnaryFunction} : SymCC.compileInₑ t₁ t₂ ancs? = SymCC.Factory.or (compileInₑ.isEq t₁ t₂) (compileInₑ.isIn t₁ t₂ ancs?)

def Cedar.Thm.compileInₛ.isIn₁ (t ts : SymCC.Term) : SymCC.Term

Equations

• Cedar.Thm.compileInₛ.isIn₁ t ts = if ts.typeOf = t.typeOf.set then Cedar.SymCC.Factory.set.member t ts else Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

theorem Cedar.Thm.compileInₛ.isIn₁_def {t ts : SymCC.Term} : isIn₁ t ts = SymCC.compileInₛ.isIn₁ t ts

def Cedar.Thm.compileInₛ.isIn₂ (t ts : SymCC.Term) (ancs? : Option SymCC.UnaryFunction) : SymCC.Term

Equations

• Cedar.Thm.compileInₛ.isIn₂ t ts (some ancs) = Cedar.SymCC.Factory.set.intersects ts (Cedar.SymCC.Factory.app ancs t)
• Cedar.Thm.compileInₛ.isIn₂ t ts none = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

theorem Cedar.Thm.compileInₛ.isIn₂_def {t ts : SymCC.Term} {ancs? : Option SymCC.UnaryFunction} : isIn₂ t ts ancs? = SymCC.compileInₛ.isIn₂ t ts ancs?

theorem Cedar.Thm.compileInₛ_def {t ts : SymCC.Term} {ancs? : Option SymCC.UnaryFunction} : SymCC.compileInₛ t ts ancs? = SymCC.Factory.or (compileInₛ.isIn₁ t ts) (compileInₛ.isIn₂ t ts ancs?)

theorem Cedar.Thm.compileApp₂_mem_ok_implies {t t₁ t₂ : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.compileApp₂ Spec.BinaryOp.mem t₁ t₂ εs = Except.ok t → ∃ (ety₁ : Spec.EntityType), ∃ (ety₂ : Spec.EntityType), t₁.typeOf = SymCC.TermType.entity ety₁ ∧ (t₂.typeOf = SymCC.TermType.entity ety₂ ∧ t = (SymCC.compileInₑ t₁ t₂ (εs.ancestorsOfType ety₁ ety₂)).some ∨ t₂.typeOf = (SymCC.TermType.entity ety₂).set ∧ t = (SymCC.compileInₛ t₁ t₂ (εs.ancestorsOfType ety₁ ety₂)).some)

theorem Cedar.Thm.compile_binaryApp_ok_implies {op₂ : Spec.BinaryOp} {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (hok : SymCC.compile (Spec.Expr.binaryApp op₂ x₁ x₂) εnv = Except.ok t) : ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ∃ (t₃ : SymCC.Term), SymCC.compile x₁ εnv = Except.ok t₁ ∧ SymCC.compile x₂ εnv = Except.ok t₂ ∧ SymCC.compileApp₂ op₂ (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂) εnv.entities = Except.ok t₃ ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ t₃)

theorem Cedar.Thm.compileSet_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} (hok : SymCC.compileSet ts = Except.ok t) : ∃ (ty : SymCC.TermType), ∃ (hd : SymCC.Term), ∃ (tl : List SymCC.Term), ts = hd :: tl ∧ (∀ (t : SymCC.Term), t ∈ ts → t.typeOf = ty.option) ∧ t = SymCC.Factory.ifAllSome ts (SymCC.Factory.setOf (List.map SymCC.Factory.option.get ts) ty).some

theorem Cedar.Thm.compile_set_ok_implies {xs : List Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (hok : SymCC.compile (Spec.Expr.set xs) εnv = Except.ok t) : ∃ (ts : List SymCC.Term), List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => SymCC.compile x εnv = Except.ok t) xs ts ∧ SymCC.compileSet ts = Except.ok t

theorem Cedar.Thm.compile_record_ok_implies {axs : List (Spec.Attr × Spec.Expr)} {εnv : SymCC.SymEnv} {t : SymCC.Term} (hok : SymCC.compile (Spec.Expr.record axs) εnv = Except.ok t) : ∃ (ats : List (Spec.Attr × SymCC.Term)), List.Forall₂ (fun (px : Spec.Attr × Spec.Expr) (pt : Spec.Attr × SymCC.Term) => px.fst = pt.fst ∧ SymCC.compile px.snd εnv = Except.ok pt.snd) axs ats ∧ t = SymCC.compileRecord ats

theorem Cedar.Thm.compileCall_decimal_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.decimal ts = Except.ok t → ∃ (s : String), ∃ (d : Spec.Ext.Decimal), ts = [(SymCC.Term.prim (SymCC.TermPrim.string s)).some] ∧ Spec.Ext.Decimal.decimal s = some d ∧ t = (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.decimal d))).some

theorem Cedar.Thm.compileCall_decimal_lessThan_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.lessThan ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.Decimal.lessThan (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).some)

theorem Cedar.Thm.compileCall_decimal_lessThanOrEqual_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.lessThanOrEqual ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.Decimal.lessThanOrEqual (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).some)

theorem Cedar.Thm.compileCall_decimal_greaterThan_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.greaterThan ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.Decimal.greaterThan (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).some)

theorem Cedar.Thm.compileCall_decimal_greaterThanOrEqual_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.greaterThanOrEqual ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.Decimal.greaterThanOrEqual (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).some)

theorem Cedar.Thm.compileCall_ipAddr_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.ip ts = Except.ok t → ∃ (s : String), ∃ (ip : Spec.Ext.IPAddr.IPNet), ts = [(SymCC.Term.prim (SymCC.TermPrim.string s)).some] ∧ Spec.Ext.IPAddr.ip s = some ip ∧ t = (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr ip))).some

theorem Cedar.Thm.compileCall_ipAddr_isIpv4_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.isIpv4 ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.IPAddr.isIpv4 (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_ipAddr_isIpv6_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.isIpv6 ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.IPAddr.isIpv6 (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_ipAddr_isLoopback_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.isLoopback ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.IPAddr.isLoopback (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_ipAddr_isMulticast_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.isMulticast ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.IPAddr.isMulticast (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_ipAddr_isInRange_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.isInRange ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.IPAddr.isInRange (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).some)

theorem Cedar.Thm.compileCall_datetime_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.datetime ts = Except.ok t → ∃ (s : String), ∃ (d : Spec.Ext.Datetime), ts = [(SymCC.Term.prim (SymCC.TermPrim.string s)).some] ∧ Spec.Ext.Datetime.datetime s = some d ∧ t = (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime d))).some

theorem Cedar.Thm.compileCall_datetime_offset_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.offset ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.Datetime.offset (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)))

theorem Cedar.Thm.compileCall_datetime_durationSince_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.durationSince ts = Except.ok t → ∃ (t₁ : SymCC.Term), ∃ (t₂ : SymCC.Term), ts = [t₁, t₂] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option ∧ t₂.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (SymCC.Datetime.durationSince (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)))

theorem Cedar.Thm.compileCall_datetime_toDate_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toDate ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Datetime.toDate (SymCC.Factory.option.get t₁))

theorem Cedar.Thm.compileCall_datetime_toTime_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toTime ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Datetime.toTime (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_duration_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.duration ts = Except.ok t → ∃ (s : String), ∃ (d : Spec.Ext.Datetime.Duration), ts = [(SymCC.Term.prim (SymCC.TermPrim.string s)).some] ∧ Spec.Ext.Datetime.duration s = some d ∧ t = (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration d))).some

theorem Cedar.Thm.compileCall_duration_toMilliseconds_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toMilliseconds ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Duration.toMilliseconds (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_duration_toSeconds_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toSeconds ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Duration.toSeconds (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_duration_toMinutes_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toMinutes ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Duration.toMinutes (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_duration_toHours_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toHours ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Duration.toHours (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compileCall_duration_toDays_ok_implies {ts : List SymCC.Term} {t : SymCC.Term} : SymCC.compileCall Spec.ExtFun.toDays ts = Except.ok t → ∃ (t₁ : SymCC.Term), ts = [t₁] ∧ t₁.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option ∧ t = SymCC.Factory.ifSome t₁ (SymCC.Duration.toDays (SymCC.Factory.option.get t₁)).some

theorem Cedar.Thm.compile_call_ok_implies {f : Spec.ExtFun} {xs : List Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} (hok : SymCC.compile (Spec.Expr.call f xs) εnv = Except.ok t) : ∃ (ts : List SymCC.Term), List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => SymCC.compile x εnv = Except.ok t) xs ts ∧ SymCC.compileCall f ts = Except.ok t