---

Step * of Lemma pi_termco-ext

pi_termco() ≡ lbl:Atom × if lbl =a "zero" then Unit
                         if lbl =a "comm" then pre:pi_prefix() × pi_termco()
                         if lbl =a "option" then left:pi_termco() × pi_termco()
                         if lbl =a "par" then left:pi_termco() × pi_termco()
                         if lbl =a "rep" then pi_termco()
                         if lbl =a "new" then name:Name × pi_termco()
                         else Void
                         fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
pi\_termco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "zero"  then  Unit
                                                  if  lbl  =a  "comm"  then  pre:pi\_prefix()  \mtimes{}  pi\_termco()
                                                  if  lbl  =a  "option"  then  left:pi\_termco()  \mtimes{}  pi\_termco()
                                                  if  lbl  =a  "par"  then  left:pi\_termco()  \mtimes{}  pi\_termco()
                                                  if  lbl  =a  "rep"  then  pi\_termco()
                                                  if  lbl  =a  "new"  then  name:Name  \mtimes{}  pi\_termco()
                                                  else  Void
                                                  fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index