---

pi-names(p) ==
  F(p) where 
  F(0) = []  
  F(pre.P) = l-union(NameDeq;pi-prefix-names(pre);P1) where  
              P1 = F(P)   
  F(P + Q) = l-union(NameDeq;P1;Q1) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(P | Q) = l-union(NameDeq;P1;Q1) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(!P) = P1 where  
           P1 = F(P)  
  F(new v.R) = [v / R1] where  
                R1 = F(R)

---

Definitions :  pi_term_ind: pi_term_ind,  nil: [],  l-union: l-union(eq;as;bs),  name-deq: NameDeq,  cons: [car / cdr]
FDL editor aliases :  pi-names

---

pi-names(p)  ==
    F(p)  where 
    F(0)  =  []   
    F(pre.P)  =  l-union(NameDeq;pi-prefix-names(pre);P1)  where   
                            P1  =  F(P)     
    F(P  +  Q)  =  l-union(NameDeq;P1;Q1)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(P  |  Q)  =  l-union(NameDeq;P1;Q1)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(!P)  =  P1  where   
                      P1  =  F(P)   
    F(new  v.R)  =  [v  /  R1]  where   
                                R1  =  F(R)


Date html generated: 2010_08_27-PM-08_41_31
Last ObjectModification: 2010_02_16-PM-01_19_42

Home Index