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
Lemmas :  corec-ext,  eq_atom_wf,  bool_wf,  eqtt_to_assert,  assert_of_eq_atom,  C_LOCATION_wf,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_atom,  subtype_rel_product,  subtype_rel_self,  subtype_rel_wf,  strong-continuous-depproduct,  continuous-constant,  strong-continuous-product,  continuous-id,  subtype_rel_weakening,  nat_wf
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: 2015_07_17-AM-07_43_03
Last ObjectModification: 2015_01_27-AM-09_47_16

Home Index