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) <z 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 <z j
, 
btrue: tt
, 
less_than: a < b
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
int_eq: if a=b  then c  else d
, 
apply: f a
, 
lambda: λx.A[x]
, 
pair: <a, b>
, 
product: x:A × B[x]
, 
subtract: n - 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