---

Step * of Lemma pi_term-ext

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

---

Latex:

---

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


By

---

Latex:
ProveDatatypeExt

---

Home Index