---

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

---

Latex:

---

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 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index