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