Nuprl Definition : eventually-one-leader

eventually ldr is the only leader ==

b:

. ((

((leader b) = ldr))

leader b eventually retires)

Definitions : all:

x:A. B[x], nat:

, implies: P

Q, not:

A, equal: s = t, Id: Id, leader-eventually-retires: l eventually retires, apply: f a
FDL editor aliases : eventually-one-leader

eventually ldr is the only leader == \mforall{}b:\mBbbN{}. ((\mneg{}((leader b) = ldr)) {}\mRightarrow{} leader b eventually retires) Date html generated: 2010_08_28-PM-01_01_02 Last ObjectModification: 2009_12_23-PM-05_28_15 Home Index