Nuprl Lemma : C_DVALUEpco-ext

C_DVALUEpco() ≡ lbl:Atom × if lbl =a "Null" then Unit
                           if lbl =a "Int" then ℤ
                           if lbl =a "Pointer" then C_LVALUE()?
                           if lbl =a "Array" then lower:ℤ × upper:ℤ × ({lower..upper-} ⟶ C_DVALUEpco())
                           if lbl =a "Struct" then lbls:Atom List × ({a:Atom| (a ∈ lbls)}  ⟶ C_DVALUEpco())
                           else Void
                           fi 


Proof



Definitions occuring in Statement :  C_DVALUEpco: C_DVALUEpco(),  C_LVALUE: C_LVALUE(),  l_member: (x ∈ l),  list: T List,  int_seg: {i..j-},  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  ext-eq: A ≡ B,  unit: Unit,  set: {x:A| B[x]} ,  function: x:A ⟶ B[x],  product: x:A × B[x],  union: left + right,  int: ℤ,  token: "$token",  atom: Atom,  void: Void
Definitions unfolded in proof :  C_DVALUEpco: C_DVALUEpco(),  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  member: t ∈ T,  prop: ℙ,  so_apply: x[s],  uimplies: b supposing a,  continuous-monotone: ContinuousMonotone(T.F[T]),  and: P ∧ Q,  type-monotone: Monotone(T.F[T]),  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  ifthenelse: if b then t else f fi ,  bfalse: ff,  exists: ∃x:A. B[x],  or: P ∨ Q,  sq_type: SQType(T),  guard: {T},  bnot: ¬bb,  assert: ↑b,  false: False,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  strong-type-continuous: Continuous+(T.F[T]),  type-continuous: Continuous(T.F[T])
Lemmas referenced :  corec-ext,  ifthenelse_wf,  eq_atom_wf,  unit_wf2,  C_LVALUE_wf,  int_seg_wf,  list_wf,  l_member_wf,  subtype_rel_product,  bool_wf,  eqtt_to_assert,  assert_of_eq_atom,  subtype_rel_self,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_atom,  subtype_rel_dep_function,  set_wf,  subtype_rel_wf,  strong-continuous-depproduct,  continuous-constant,  strong-continuous-function,  continuous-id,  subtype_rel_weakening,  nat_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  cut,  lemma_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  sqequalRule,  lambdaEquality,  productEquality,  atomEquality,  instantiate,  hypothesisEquality,  tokenEquality,  hypothesis,  universeEquality,  intEquality,  unionEquality,  functionEquality,  setEquality,  voidEquality,  independent_isectElimination,  independent_pairFormation,  isect_memberFormation,  introduction,  because_Cache,  lambdaFormation,  unionElimination,  equalityElimination,  productElimination,  dependent_pairFormation,  equalityTransitivity,  equalitySymmetry,  promote_hyp,  dependent_functionElimination,  independent_functionElimination,  voidElimination,  equalityEquality,  axiomEquality,  isect_memberEquality,  cumulativity,  isectEquality,  applyEquality
Latex:
C\_DVALUEpco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Null"  then  Unit
                                                      if  lbl  =a  "Int"  then  \mBbbZ{}
                                                      if  lbl  =a  "Pointer"  then  C\_LVALUE()?
                                                      if  lbl  =a  "Array"
                                                          then  lower:\mBbbZ{}  \mtimes{}  upper:\mBbbZ{}  \mtimes{}  (\{lower..upper\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEpco())
                                                      if  lbl  =a  "Struct"
                                                          then  lbls:Atom  List  \mtimes{}  (\{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEpco())
                                                      else  Void
                                                      fi 


Date html generated: 2016_05_16-AM-08_48_45
Last ObjectModification: 2015_12_28-PM-06_57_41

Theory : C-semantics


Home Index