Nuprl Definition : ler2_non_dummy_configuration
ler2_non_dummy_configuration(es;nodes) ==
e:E. epoch:
. i:Id. (<epoch, i> 
ler2_config'base()(e) 
((epoch > 0) 
i 
nodes (
(i = loc(e)))))
Definitions occuring in Statement :
ler2_config'base: ler2_config'base(),
classrel: v X(e),
es-loc: loc(e),
es-E: E,
Id: Id,
gt: i > j,
all: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
pair: <a, b>,
product: x:A 
B[x],
natural_number: $n,
int: ,
equal: s = t,
bag-member: x bs
FDL editor aliases :
ler2_non_dummy_configuration
ler2\_non\_dummy\_configuration(es;nodes) ==
\mforall{}e:E. \mforall{}epoch:\mBbbZ{}. \mforall{}i:Id.
(<epoch, i> \mmember{} ler2\_config'base()(e) {}\mRightarrow{} ((epoch > 0) \mwedge{} i \mdownarrow{}\mmember{} nodes \mwedge{} (\mneg{}(i = loc(e)))))
Date html generated:
2012_02_20-PM-06_17_04
Last ObjectModification:
2012_02_02-PM-02_44_05
Home
Index