---

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

---

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 


By

ProveDatatypeExt

---

Home Index