Nuprl Lemma : C_LVALUEco-ext

C_LVALUEco() ≡ lbl:Atom × if lbl =a "Ground" then C_LOCATION()
                          if lbl =a "Index" then lval:C_LVALUEco() × ℤ
                          if lbl =a "Scomp" then lval:C_LVALUEco() × Atom
                          else Void
                          fi 


Proof



Definitions occuring in Statement :  C_LVALUEco: C_LVALUEco(),  C_LOCATION: C_LOCATION(),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  ext-eq: A ≡ B,  product: x:A × B[x],  int: ℤ,  token: "$token",  atom: Atom,  void: Void
Definitions unfolded in proof :  C_LVALUEco: C_LVALUEco(),  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  member: t ∈ T,  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],  prop: ℙ,  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,  C_LOCATION_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_wf,  strong-continuous-depproduct,  continuous-constant,  strong-continuous-product,  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,  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,  functionEquality
Latex:
C\_LVALUEco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Ground"  then  C\_LOCATION()
                                                    if  lbl  =a  "Index"  then  lval:C\_LVALUEco()  \mtimes{}  \mBbbZ{}
                                                    if  lbl  =a  "Scomp"  then  lval:C\_LVALUEco()  \mtimes{}  Atom
                                                    else  Void
                                                    fi 


Date html generated: 2016_05_16-AM-08_46_31
Last ObjectModification: 2015_12_28-PM-06_57_28

Theory : C-semantics


Home Index