Nuprl Definition : pi-rep-trans

pi-rep-trans(l_loc;P;g) ==
  λl,serial,avoid. RecProcess(0;s,m.if (s =z 0) ∧b pDVfire?(m) then <1, make-lg([<l_loc, mk-tagged("msg";pDVloc(l))>])>
                  if (s =z 1) ∧b pDVloc_tag?(m)
                    then let l1 pDVloc_tag-id(m) in
                          let n1 pDVloc_tag-name(m) in
                          <0
                          lg-add(make-lg([<l1, mk-tagged("create";g l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>;\000C <l, mk-tagged("msg";pDVfire())>]);0;1)
                          >
                  else <s, make-lg([])>
                  fi )



Definitions occuring in Statement :  pDVfire?: pDVfire?(x) pDVloc_tag-name: pDVloc_tag-name(x) pDVloc_tag-id: pDVloc_tag-id(x) pDVloc_tag?: pDVloc_tag?(x) pDVfire: pDVfire() pDVloc: pDVloc(id) lg-add: lg-add(g;a;b) make-lg: make-lg(L) rec-process: RecProcess(s0;s,m.next[s; m]) cons: [a b] nil: [] band: p ∧b q ifthenelse: if then else fi  eq_int: (i =z j) let: let apply: a lambda: λx.A[x] pair: <a, b> natural_number: $n token: "$token" mk-tagged: mk-tagged(tg;x)
FDL editor aliases :  pi-rep-trans

Latex:
pi-rep-trans(l$_{loc}$;P;g)  ==
    \mlambda{}l,serial,avoid.  RecProcess(0;s,m.if  (s  =\msubz{}  0)  \mwedge{}\msubb{}  pDVfire?(m)
                                                                            then  ə,  make-lg([<l$_{loc}$,  mk-tagged("m\000Csg";pDVloc(l))>])>
                                    if  (s  =\msubz{}  1)  \mwedge{}\msubb{}  pDVloc\_tag?(m)
                                        then  let  l1  =  pDVloc\_tag-id(m)  in
                                                    let  n1  =  pDVloc\_tag-name(m)  in
                                                    ɘ
                                                    ,  lg-add(make-lg([<l1,  mk-tagged("create";g  P  l1  n1  avoid)>
                                                                                        <l1,  mk-tagged("msg";pDVfire())>
                                                                                        <l,  mk-tagged("msg";pDVfire())>]);0;1)
                                                    >
                                    else  <s,  make-lg([])>
                                    fi  )



Date html generated: 2015_07_23-AM-11_59_07
Last ObjectModification: 2012_08_30-PM-01_49_55

Home Index