---

Step * of Lemma C_LVALUE-ext

C_LVALUE() ≡ lbl:Atom × if lbl =a "Ground" then C_LOCATION()
                        if lbl =a "Index" then lval:C_LVALUE() × ℤ
                        if lbl =a "Scomp" then lval:C_LVALUE() × Atom
                        else Void
                        fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
C\_LVALUE()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Ground"  then  C\_LOCATION()
                                                if  lbl  =a  "Index"  then  lval:C\_LVALUE()  \mtimes{}  \mBbbZ{}
                                                if  lbl  =a  "Scomp"  then  lval:C\_LVALUE()  \mtimes{}  Atom
                                                else  Void
                                                fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index