---

pi-simple-subst-aux(t;x;P;avoid) ==
  Y 
  (pi-simple-subst-aux,P,avoid.
    F(P) where 
    F(0) = 0  
    F(pre.R) = G(pre) where   
               G(c<v>) = let c1 = if name_eq(c;x) then t else c fi  in
                          let v1 = if name_eq(v;x) then t else v fi  in
                          c1<v1>.pi-simple-subst-aux R avoid  
               G(c?(v)) = let w = maybe-new(v;avoid) in
                           let c1 = if name_eq(c;x) then t else c fi  in
                           let R1 = pi-replace(w;v;R) in
                           c1?(w).pi-simple-subst-aux R1 [w / avoid] where  
                A = F(R)   
    F(P + Q) = (pi-simple-subst-aux P avoid + pi-simple-subst-aux Q 
                                              avoid) where  
                A = F(P)  
                B = F(Q)  
    F(P | Q) = (pi-simple-subst-aux P avoid | pi-simple-subst-aux Q 
                                              avoid) where  
                A = F(P)  
                B = F(Q)  
    F(!P) = !pi-simple-subst-aux P avoid where  
             A = F(P)  
    F(new v.P) = let w = maybe-new(v;avoid) in
                  let P1 = pi-replace(w;v;P) in
                  (new w. pi-simple-subst-aux P1 [w / avoid]) where  
                  A = F(P)) 
  P 
  avoid

---

Definitions :  ycomb: Y,  lambda: x.A[x],  pi_term_ind: pi_term_ind,  pizero: 0,  pi_prefix_ind: pi_prefix_ind,  pisend: chan<val>,  ifthenelse: if b then t else f fi ,  name_eq: name_eq(x;y),  picomm: pre.body,  pircv: chan?(var),  pioption: (left + right),  pipar: (left | right),  pirep: !body,  maybe-new: maybe-new(s;avoid),  let: let,  pi-replace: pi-replace(t;x;P),  pinew: (new name. body),  apply: f a,  cons: [car / cdr]
FDL editor aliases :  pi-simple-subst-aux

---

pi-simple-subst-aux(t;x;P;avoid)  ==
    Y 
    (\mlambda{}pi-simple-subst-aux,P,avoid.
        F(P)  where 
        F(0)  =  0   
        F(pre.R)  =  G(pre)  where     
                              G(c<v>)  =  let  c1  =  if  name\_eq(c;x)  then  t  else  c  fi    in
                                                    let  v1  =  if  name\_eq(v;x)  then  t  else  v  fi    in
                                                    c1<v1>.pi-simple-subst-aux  R  avoid   
                              G(c?(v))  =  let  w  =  maybe-new(v;avoid)  in
                                                      let  c1  =  if  name\_eq(c;x)  then  t  else  c  fi    in
                                                      let  R1  =  pi-replace(w;v;R)  in
                                                      c1?(w).pi-simple-subst-aux  R1  [w  /  avoid]  where   
                                A  =  F(R)     
        F(P  +  Q)  =  (pi-simple-subst-aux  P  avoid  +  pi-simple-subst-aux  Q  avoid)  where   
                                A  =  F(P)   
                                B  =  F(Q)   
        F(P  |  Q)  =  (pi-simple-subst-aux  P  avoid  |  pi-simple-subst-aux  Q  avoid)  where   
                                A  =  F(P)   
                                B  =  F(Q)   
        F(!P)  =  !pi-simple-subst-aux  P  avoid  where   
                          A  =  F(P)   
        F(new  v.P)  =  let  w  =  maybe-new(v;avoid)  in
                                    let  P1  =  pi-replace(w;v;P)  in
                                    (new  w.  pi-simple-subst-aux  P1  [w  /  avoid])  where   
                                    A  =  F(P)) 
    P 
    avoid


Date html generated: 2010_08_27-PM-08_41_42
Last ObjectModification: 2010_05_03-PM-02_17_22

Home Index