---

pi-level(p) ==
  F(p) where 
  F(0) = 0  
  F(pre.P) = lvl where  
              lvl = F(P)   
  F(P + Q) = imax(lvl_P;lvl_Q) where  
              lvl_P = F(P)  
              lvl_Q = F(Q)  
  F(P | Q) = imax(lvl_P;lvl_Q) + 1 where  
              lvl_P = F(P)  
              lvl_Q = F(Q)  
  F(!P) = lvl_P + 1 where  
           lvl_P = F(P)  
  F(new v.R) = lvl_R where  
                lvl_R = F(R)

---

Definitions :  pi_term_ind: pi_term_ind,  imax: imax(a;b),  add: n + m,  natural_number: $n
FDL editor aliases :  pi-level

---

pi-level(p)  ==
    F(p)  where 
    F(0)  =  0   
    F(pre.P)  =  lvl  where   
                            lvl  =  F(P)     
    F(P  +  Q)  =  imax(lvl$_{P}$;lvl$_{Q}$)  where   
                            lvl$_{P}$  =  F(P)   
                            lvl$_{Q}$  =  F(Q)   
    F(P  |  Q)  =  imax(lvl$_{P}$;lvl$_{Q}$)  +  1  where   
                            lvl$_{P}$  =  F(P)   
                            lvl$_{Q}$  =  F(Q)   
    F(!P)  =  lvl$_{P}$  +  1  where   
                      lvl$_{P}$  =  F(P)   
    F(new  v.R)  =  lvl$_{R}$  where   
                                lvl$_{R}$  =  F(R)


Date html generated: 2010_08_27-PM-08_41_02
Last ObjectModification: 2010_04_02-PM-02_01_09

Home Index