Nuprl Definition : ler2_consistent_configuration
ler2_consistent_configuration(es) ==
e1,e2:E. epoch:
. i1,i2:Id.
(<epoch, i1> 
ler2_config'base()(e1) 
<epoch, i2> ler2_config'base()(e2) (loc(e1) = loc(e2)) (i1 = i2))
Definitions occuring in Statement :
ler2_config'base: ler2_config'base(),
classrel: v X(e),
es-loc: loc(e),
es-E: E,
Id: Id,
all: x:A. B[x],
implies: P Q,
pair: <a, b>,
product: x:A 
B[x],
int: ,
equal: s = t
FDL editor aliases :
ler2_consistent_configuration
ler2\_consistent\_configuration(es) ==
\mforall{}e1,e2:E. \mforall{}epoch:\mBbbZ{}. \mforall{}i1,i2:Id.
(<epoch, i1> \mmember{} ler2\_config'base()(e1)
{}\mRightarrow{} <epoch, i2> \mmember{} ler2\_config'base()(e2)
{}\mRightarrow{} (loc(e1) = loc(e2))
{}\mRightarrow{} (i1 = i2))
Date html generated:
2012_02_20-PM-06_16_52
Last ObjectModification:
2012_02_02-PM-02_43_58
Home
Index