Nuprl Definition : list-eo

Given a single location, i, and a ⌈L ∈ Info List⌉, we can construct an event
ordering where the info associated with the events is exactly L.
The events are the indexes into L and both local and causal ordering are <.⋅

list-eo(L;i) ==
  mk-extended-eo(type: ℕ;
                 domain: λn.n <z ||L||;
                 loc: λe.i;
                 info: λn.if n <z ||L|| then L[n] else hd(L) fi ;
                 causal: λe1,e2. e1 < e2;
                 local: λe1,e2. e1 <z e2;
                 pred: λe.if (e =_z 0) then 0 else e - 1 fi ;
                 rank: λe.e)

Definitions occuring in Statement : mk-extended-eo: mk-extended-eo, select: L[n], hd: hd(l), length: ||as||, nat: ℕ, ifthenelse: if b then t else f fi , lt_int: i <z j, eq_int: (i =_z j), less_than: a < b, lambda: λx.A[x], subtract: n - m, natural_number: $n
FDL editor aliases : list-eo

Latex:
list-eo(L;i) == mk-extended-eo(type: \mBbbN{}; domain: \mlambda{}n.n <z ||L||; loc: \mlambda{}e.i; info: \mlambda{}n.if n <z ||L|| then L[n] else hd(L) fi ; causal: \mlambda{}e1,e2. e1 < e2; local: \mlambda{}e1,e2. e1 <z e2; pred: \mlambda{}e.if (e =\msubz{} 0) then 0 else e - 1 fi ; rank: \mlambda{}e.e) Date html generated: 2015_07_21-PM-04_28_50 Last ObjectModification: 2014_07_23-PM-00_02_38 Home Index