---

pi-replace(t;x;P) ==
  F(P) where 
  F(0) = 0  
  F(pre.P) = prefix-replace(t;x;pre).P1 where  
              P1 = F(P)   
  F(P + Q) = (P1 + Q1) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(P | Q) = (P1 | Q1) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(!P) = !P1 where  
           P1 = F(P)  
  F(new v.R) = let v1 = if name_eq(v;x) then t else v fi  in
                   (new v1. P1) where  
                P1 = F(R)

---

Definitions :  pi_term_ind: pi_term_ind,  pizero: 0,  picomm: pre.body,  prefix-replace: prefix-replace(t;x;pre),  pioption: (left + right),  pipar: (left | right),  pirep: !body,  let: let,  ifthenelse: if b then t else f fi ,  name_eq: name_eq(x;y),  pinew: (new name. body)
FDL editor aliases :  pi-replace

---

pi-replace(t;x;P)  ==
    F(P)  where 
    F(0)  =  0   
    F(pre.P)  =  prefix-replace(t;x;pre).P1  where   
                            P1  =  F(P)     
    F(P  +  Q)  =  (P1  +  Q1)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(P  |  Q)  =  (P1  |  Q1)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(!P)  =  !P1  where   
                      P1  =  F(P)   
    F(new  v.R)  =  let  v1  =  if  name\_eq(v;x)  then  t  else  v  fi    in
                                      (new  v1.  P1)  where   
                                P1  =  F(R)


Date html generated: 2010_08_27-PM-08_41_11
Last ObjectModification: 2010_02_15-PM-06_23_02

Home Index