---

Step * of Lemma pi_prefix-ext

pi_prefix() ≡ lbl:Atom × if lbl =a "send" then chan:Name × Name
                         if lbl =a "rcv" then chan:Name × Name
                         else Void
                         fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
pi\_prefix()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "send"  then  chan:Name  \mtimes{}  Name
                                                  if  lbl  =a  "rcv"  then  chan:Name  \mtimes{}  Name
                                                  else  Void
                                                  fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index