Nuprl Definition : ranked-eo

ordering multiple locations

ranked-eo(L;rk) ==
  mk-extended-eo(type: i:Id × ℕ||L i||;
                 domain: λp.tt;
                 loc: λp.(fst(p));
                 info: λp.L (fst(p))[snd(p)];
                 causal: λe1,e2. rk e1 < rk e2;
                 local: λe1,e2. snd(e1) <snd(e2);
                 pred: λp.if snd(p)=0  then p  else <fst(p), (snd(p)) 1>;
                 rank: rk)



Definitions occuring in Statement :  mk-extended-eo: mk-extended-eo Id: Id select: L[n] length: ||as|| int_seg: {i..j-} lt_int: i <j btrue: tt less_than: a < b pi1: fst(t) pi2: snd(t) int_eq: if a=b  then c  else d apply: a lambda: λx.A[x] pair: <a, b> product: x:A × B[x] subtract: m natural_number: $n
FDL editor aliases :  ranked-eo

Latex:
ranked-eo(L;rk)  ==
    mk-extended-eo(type:  i:Id  \mtimes{}  \mBbbN{}||L  i||;
                                  domain:  \mlambda{}p.tt;
                                  loc:  \mlambda{}p.(fst(p));
                                  info:  \mlambda{}p.L  (fst(p))[snd(p)];
                                  causal:  \mlambda{}e1,e2.  rk  e1  <  rk  e2;
                                  local:  \mlambda{}e1,e2.  snd(e1)  <z  snd(e2);
                                  pred:  \mlambda{}p.if  snd(p)=0    then  p    else  <fst(p),  (snd(p))  -  1>
                                  rank:  rk)



Date html generated: 2015_07_21-PM-04_41_38
Last ObjectModification: 2014_07_23-PM-00_09_17

Home Index