---

pi-normal(t) ==
  F(t) where 
  F(0) = tt  
  F(pr.A) = nm where  
             nm = F(A)   
  F(A + B) = na
              nb
              (picomm?(A) pioption?(A))
              (picomm?(B) pioption?(B)) where  
              na = F(A)  
              nb = F(B)  
  F(A | B) = na  nb where  
              na = F(A)  
              nb = F(B)  
  F(!A) = na where  
           na = F(A)  
  F(new x.A) = na where  
                na = F(A)

---

Definitions :  pi_term_ind: Error :pi_term_ind,  btrue: tt,  bor: p q,  picomm?: Error :picomm?,  pioption?: Error :pioption?,  band: p  q
FDL editor aliases :  pi-normal

---

pi-normal(t)  ==
    F(t)  where 
    F(0)  =  tt   
    F(pr.A)  =  nm  where   
                          nm  =  F(A)     
    F(A  +  B)  =  na  \mwedge{}\msubb{}  nb  \mwedge{}\msubb{}  (picomm?(A)  \mvee{}\msubb{}pioption?(A))  \mwedge{}\msubb{}  (picomm?(B)  \mvee{}\msubb{}pioption?(B))  where   
                            na  =  F(A)   
                            nb  =  F(B)   
    F(A  |  B)  =  na  \mwedge{}\msubb{}  nb  where   
                            na  =  F(A)   
                            nb  =  F(B)   
    F(!A)  =  na  where   
                      na  =  F(A)   
    F(new  x.A)  =  na  where   
                                na  =  F(A)


Date html generated: 2010_08_27-PM-08_42_07
Last ObjectModification: 2010_02_05-PM-05_32_38

Home Index