---

pi_level(pi-term) ==
  F(pi-term) where 
  F(0) = 0  
  F(pr.P) = l where  
             l = F(P)   
  F(P + Q) = imax(l_P;l_Q) where  
              l_P = F(P)  
              l_Q = F(Q)  
  F(P | Q) = imax(l_P;l_Q) + 1 where  
              l_P = F(P)  
              l_Q = F(Q)  
  F(!P) = l + 1 where  
           l = F(P)  
  F(new x.P) = l where  
                l = F(P)

---

Definitions :  pi_term_ind: Error :pi_term_ind,  imax: imax(a;b),  add: n + m,  natural_number: $n
FDL editor aliases :  pi_level

---

pi\_level(pi-term)  ==
    F(pi-term)  where 
    F(0)  =  0   
    F(pr.P)  =  l  where   
                          l  =  F(P)     
    F(P  +  Q)  =  imax(l$_{P}$;l$_{Q}$)  where   
                            l$_{P}$  =  F(P)   
                            l$_{Q}$  =  F(Q)   
    F(P  |  Q)  =  imax(l$_{P}$;l$_{Q}$)  +  1  where   
                            l$_{P}$  =  F(P)   
                            l$_{Q}$  =  F(Q)   
    F(!P)  =  l  +  1  where   
                      l  =  F(P)   
    F(new  x.P)  =  l  where   
                                l  =  F(P)


Date html generated: 2010_08_27-PM-08_42_08
Last ObjectModification: 2010_02_09-PM-05_10_32

Home Index