Nuprl Definition : ler_non_decreasing_configuration
ler_non_decreasing_configuration(es) ==
e1,e2:E. epoch1,epoch2:
. i1,i2:Id.
(<epoch1, i1> 
ler_Config()(e1) 
<epoch2, i2> ler_Config()(e2) (e1 <loc e2) (epoch1 
epoch2))
Definitions occuring in Statement :
ler_Config: ler_Config(),
classrel: v X(e),
es-locl: (e <loc e'),
es-E: E,
Id: Id,
le: A B,
all: x:A. B[x],
implies: P Q,
pair: <a, b>,
product: x:A 
B[x],
int:
FDL editor aliases :
ler_non_decreasing_configuration
ler\_non\_decreasing\_configuration(es) ==
\mforall{}e1,e2:E. \mforall{}epoch1,epoch2:\mBbbZ{}. \mforall{}i1,i2:Id.
(<epoch1, i1> \mmember{} ler\_Config()(e1)
{}\mRightarrow{} <epoch2, i2> \mmember{} ler\_Config()(e2)
{}\mRightarrow{} (e1 <loc e2)
{}\mRightarrow{} (epoch1 \mleq{} epoch2))
Date html generated:
2012_02_20-PM-06_04_48
Last ObjectModification:
2012_02_02-PM-02_39_22
Home
Index