---

pi-new-trans(x;P;g) ==
  Y 
  (pi-new-trans,l,serial,avoid,m.
    if pDVfire?(m)
    then let n = maybe-new-local(serial;x;avoid) in
          let P' = pi-simple-subst(n;x;P) in
          <g P' l serial l-union(NameDeq;avoid;pi-names(P))
          , make-lg([<l, mk-tagged("msg";pDVfire())>])
          >
    else <pi-new-trans l serial avoid, make-lg([])>
    fi )

---

Definitions :  ycomb: Y,  lambda: x.A[x],  ifthenelse: if b then t else f fi ,  pDVfire?: pDVfire?(x),  maybe-new-local: maybe-new-local(me;s;avoid),  let: let,  pi-simple-subst: pi-simple-subst(t;x;P),  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-new-trans

---

pi-new-trans(x;P;g)  ==
    Y 
    (\mlambda{}pi-new-trans,l,serial,avoid,m.
        if  pDVfire?(m)
        then  let  n  =  maybe-new-local(serial;x;avoid)  in
                    let  P'  =  pi-simple-subst(n;x;P)  in
                    <g  P'  l  serial  l-union(NameDeq;avoid;pi-names(P))
                    ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                    >
        else  <pi-new-trans  l  serial  avoid,  make-lg([])>
        fi  )


Date html generated: 2010_08_27-PM-09_43_03
Last ObjectModification: 2010_05_13-PM-01_30_52

Home Index