Nuprl Definition : leader-eventually-retires

l eventually retires ==

b:

.

r:E(Reserve). (((leader Reserve(r)) = l)

(Reserve(r)

b))

Definitions : exists:

x:A. B[x], nat:

, all:

x:A. B[x], es-E-interface: E(X), implies: P

Q, equal: s = t, Id: Id, apply: f a, le: A

B, eclass-val: X(e)
FDL editor aliases : leader-eventually-retires

l eventually retires == \mexists{}b:\mBbbN{}. \mforall{}r:E(Reserve). (((leader Reserve(r)) = l) {}\mRightarrow{} (Reserve(r) \mleq{} b)) Date html generated: 2010_08_28-PM-01_00_55 Last ObjectModification: 2010_04_17-PM-05_47_25 Home Index