---

pi-guarded-aux(compList;g) ==
  Y 
  (pi-guarded-aux,l,serial,avoid,m.
    if pDVmsg?(m)
    then let val = pDVmsg-val(m) in
          let i = pDVmsg-index(m) in
          if i <z ||compList||
          then let pre_i,P_i = compList[i] in
                 let P' = if pircv?(pre_i)
                          then pi-simple-subst(val;pircv-var(pre_i);P_i)
                          else P_i
                          fi  in
                     <g P' l serial l-union(NameDeq;avoid;pi-names(P'))
                     , make-lg([<l, mk-tagged("msg";pDVfire())>])
                     >
          else <pi-guarded-aux l serial avoid, make-lg([])>
          fi 
    else <pi-guarded-aux l serial avoid, make-lg([])>
    fi )

---

Definitions :  ycomb: Y,  lambda: x.A[x],  pDVmsg?: pDVmsg?(x),  pDVmsg-val: pDVmsg-val(x),  pDVmsg-index: pDVmsg-index(x),  lt_int: i <z j,  length: ||as||,  spread: spread def,  select: l[i],  let: let,  ifthenelse: if b then t else f fi ,  pircv?: pircv?(x),  pi-simple-subst: pi-simple-subst(t;x;P),  pircv-var: pircv-var(x),  l-union: l-union(eq;as;bs),  name-deq: NameDeq,  pi-names: pi-names(p),  cons: [car / cdr],  mk-tagged: mk-tagged(tg;x),  token: "$token",  pDVfire: pDVfire(),  pair: <a, b>,  apply: f a,  make-lg: make-lg(L),  nil: []
FDL editor aliases :  pi-guarded-aux

---

pi-guarded-aux(compList;g)  ==
    Y 
    (\mlambda{}pi-guarded-aux,l,serial,avoid,m.
        if  pDVmsg?(m)
        then  let  val  =  pDVmsg-val(m)  in
                    let  i  =  pDVmsg-index(m)  in
                    if  i  <z  ||compList||
                    then  let  pre$_{i}$,P$_{i}$  =  compList[i]  in
                                  ...
                    else  <pi-guarded-aux  l  serial  avoid,  make-lg([])>
                    fi 
        else  <pi-guarded-aux  l  serial  avoid,  make-lg([])>
        fi  )


Date html generated: 2010_08_27-PM-09_43_26
Last ObjectModification: 2010_05_11-PM-04_07_06

Home Index