Nuprl Definition : pi-bar-trans

pi-bar-trans(l_loc;P;Q;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
                          <2
                          , lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>;\000C <l_loc, mk-tagged("msg";pDVloc(l))>]);0;1)
                          >
                  if (s =z 2) ∧b pDVloc_tag?(m)
                    then let l2 = pDVloc_tag-id(m) in
                          let n2 = pDVloc_tag-name(m) in
                          <3
                          , lg-add(make-lg([<l2, mk-tagged("create";g Q l2 n2 avoid)>; <l2, mk-tagged("msg";pDVfire())>]\000C);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 b then t else f fi ,  eq_int: (i =z j),  let: let,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  natural_number: $n,  token: "$token",  mk-tagged: mk-tagged(tg;x)
FDL editor aliases :  pi-bar-trans
Latex:
pi-bar-trans(l$_{loc}$;P;Q;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$_{loc}$,  mk-tagged("msg";pDVloc(l\000C))>]);0;1)
                                                    >
                                    if  (s  =\msubz{}  2)  \mwedge{}\msubb{}  pDVloc\_tag?(m)
                                        then  let  l2  =  pDVloc\_tag-id(m)  in
                                                    let  n2  =  pDVloc\_tag-name(m)  in
                                                    ɛ
                                                    ,  lg-add(make-lg([<l2,  mk-tagged("create";g  Q  l2  n2  avoid)>
                                                                                        <l2,  mk-tagged("msg";pDVfire())>]);0;1)
                                                    >
                                    else  <s,  make-lg([])>
                                    fi  )


Date html generated: 2015_07_23-AM-11_59_01
Last ObjectModification: 2012_08_30-PM-01_49_49

Home Index