Nuprl Lemma : C_DVALUEp-ext

C_DVALUEp() ≡ 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_DVALUEp())
                         if lbl =a "Struct" then lbls:Atom List × ({a:Atom| (a ∈ lbls)}  ⟶ C_DVALUEp())
                         else Void
                         fi 


Proof



Definitions occuring in Statement :  C_DVALUEp: C_DVALUEp(),  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 :  ext-eq: A ≡ B,  and: P ∧ Q,  subtype_rel: A ⊆r B,  member: t ∈ T,  C_DVALUEp: C_DVALUEp(),  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  uimplies: b supposing a,  ifthenelse: if b then t else f fi ,  sq_type: SQType(T),  guard: {T},  eq_atom: x =a y,  C_DVALUEpco_size: C_DVALUEpco_size(p),  has-value: (a)↓,  bfalse: ff,  exists: ∃x:A. B[x],  prop: ℙ,  or: P ∨ Q,  bnot: ¬bb,  assert: ↑b,  false: False,  pi1: fst(t),  pi2: snd(t),  nat: ℕ,  nequal: a ≠ b ∈ T ,  int_seg: {i..j-},  lelt: i ≤ j < k,  decidable: Dec(P),  satisfiable_int_formula: satisfiable_int_formula(fmla),  not: ¬A,  top: Top,  sum: Σ(f[x] | x < k),  sum_aux: sum_aux(k;v;i;x.f[x]),  so_lambda: λ2x.t[x],  iff: P ⇐⇒ Q,  true: True,  rev_implies: P ⇐ Q,  so_apply: x[s],  l_member: (x ∈ l),  cand: A c∧ B,  ge: i ≥ j ,  less_than: a < b,  squash: ↓T,  C_DVALUEp_size: C_DVALUEp_size(p),  le: A ≤ B,  less_than': less_than'(a;b)
Lemmas referenced :  partial_wf,  value-type_wf,  squash_wf,  and_wf,  assert_of_bnot,  iff_weakening_uiff,  not_wf,  bnot_wf,  iff_transitivity,  C_DVALUEp_size_wf,  bool_cases,  sum-nat,  false_wf,  add-nat,  set_wf,  C_DVALUEpco_wf,  subtype_rel_dep_function,  list_wf,  C_LVALUE_wf,  unit_wf2,  equal-wf-base-T,  less_than_wf,  length_wf,  nat_properties,  list-subtype,  l_member_wf,  select_wf,  length_wf_nat,  C_DVALUEp_wf,  set-value-type,  has-value_wf-partial,  trivial-int-eq1,  ifthenelse_wf,  decidable__lt,  sum-partial-has-value,  int-value-type,  value-type-has-value,  int_subtype_base,  set_subtype_base,  nat_wf,  subtype_partial_sqtype_base,  int_seg_wf,  lelt_wf,  iff_wf,  assert_wf,  true_wf,  btrue_wf,  iff_imp_equal_bool,  add-member-int_seg1,  C_DVALUEpco_size_wf,  int_formula_prop_less_lemma,  intformless_wf,  le_wf,  int_formula_prop_wf,  int_term_value_var_lemma,  int_term_value_subtract_lemma,  int_term_value_constant_lemma,  int_formula_prop_le_lemma,  int_formula_prop_not_lemma,  int_formula_prop_and_lemma,  itermVar_wf,  itermSubtract_wf,  itermConstant_wf,  intformle_wf,  intformnot_wf,  intformand_wf,  satisfiable-full-omega-tt,  decidable__le,  int_seg_properties,  subtract_wf,  assert_of_le_int,  le_int_wf,  sum-partial-nat,  neg_assert_of_eq_atom,  assert-bnot,  bool_subtype_base,  bool_cases_sqequal,  equal_wf,  eqff_to_assert,  it_wf,  unit_subtype_base,  atom_subtype_base,  subtype_base_sq,  assert_of_eq_atom,  eqtt_to_assert,  bool_wf,  eq_atom_wf,  C_DVALUEpco-ext
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  independent_pairFormation,  lambdaEquality,  sqequalHypSubstitution,  setElimination,  thin,  rename,  cut,  lemma_by_obid,  hypothesis,  promote_hyp,  productElimination,  hypothesis_subsumption,  hypothesisEquality,  applyEquality,  sqequalRule,  dependent_pairEquality,  isectElimination,  tokenEquality,  lambdaFormation,  unionElimination,  equalityElimination,  equalityTransitivity,  equalitySymmetry,  independent_isectElimination,  because_Cache,  instantiate,  cumulativity,  atomEquality,  dependent_functionElimination,  independent_functionElimination,  dependent_pairFormation,  voidElimination,  functionExtensionality,  callbyvalueAdd,  baseClosed,  dependent_set_memberEquality,  natural_numberEquality,  int_eqEquality,  intEquality,  isect_memberEquality,  voidEquality,  computeAll,  callbyvalueReduce,  sqleReflexivity,  equalityEquality,  addLevel,  impliesFunctionality,  functionEquality,  productEquality,  setEquality,  imageElimination,  universeEquality,  unionEquality,  imageMemberEquality,  introduction,  substitution
Latex:
C\_DVALUEp()  \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\_DVALUEp())
                                                  if  lbl  =a  "Struct"
                                                      then  lbls:Atom  List  \mtimes{}  (\{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp())
                                                  else  Void
                                                  fi 


Date html generated: 2016_05_16-AM-08_49_06
Last ObjectModification: 2016_01_17-AM-09_43_45

Theory : C-semantics


Home Index