---

Step * of 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 
BY
{ ProveCoDatatypeExt }

---

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 


By

ProveCoDatatypeExt

---

Home Index