Nuprl Lemma : ler_inc_Config
[es:EO']. [nodes:bag(Id)].
((e1,e2:E. epoch1,epoch2:
. i1,i2:Id.
(<epoch1, i1> 
ler_Config()(e1) 
<epoch2, i2> ler_Config()(e2) (e1 <loc e2) (epoch1 
epoch2)))
(e:E. epoch:. i:Id. (<epoch, i> ler_Config()(e) (epoch > 0)))
([e1,e2:E]. [epoch1,epoch2:]. [i1,i2:Id].
(<epoch2, i2> ler_Config()(e2) <epoch1, i1> ler_Nbr()(e1) (e1 <loc e2) (epoch1 epoch2))))
Proof not projected
Definitions occuring in Statement :
ler_Nbr: ler_Nbr(),
ler_Config: ler_Config(),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
gt: i > j,
le: A B,
all: x:A. B[x],
implies: P Q,
pair: <a, b>,
product: x:A 
B[x],
natural_number: $n,
int: ,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
implies: P Q,
all: x:A. B[x],
le: A B,
gt: i > j,
ler_Nbr: ler_Nbr(),
member: t T,
nat: 
,
ge: i 
j ,
not: 
A,
false: False,
prop: 
,
squash: 
T,
true: True,
let: let,
top: Top,
so_lambda: 
x.t[x],
subtype: S 
T,
ler_dumEpoch: ler_dumEpoch(),
strongwellfounded: SWellFounded(R[x; y]),
exists: 
x:A. B[x],
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
sq_stable: SqStable(P),
or: P 
Q,
btrue: tt,
bfalse: ff,
sq_type: SQType(T),
guard: {T},
pi2: snd(t),
so_apply: x[s],
pi1: fst(t),
es-p-local-pred: es-p-local-pred(es;P),
es-locl: (e <loc e')
Lemmas :
es-causl-swellfnd,
nat_properties,
ge_wf,
nat_wf,
le_wf,
es-causl_wf,
rec-combined-loc-class-opt-1-classrel,
simple-loc-comb-2-concat-classrel,
ifthenelse_wf,
lt_int_wf,
bag_wf,
single-bag_wf,
primed-class-opt_wf,
ler_dumEpoch_wf,
sq_stable_from_decidable,
decidable__le,
bool_cases,
subtype_base_sq,
bool_wf,
bool_subtype_base,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_lt_int,
bag-member-single,
Error :pi2_wf,
pi1_wf_top,
primed-class-opt-classrel,
le_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
es-locl_wf,
classrel_wf,
ler_Nbr_wf,
ler_Config_wf,
Id_wf,
gt_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
event-ordering+_wf,
es-loc_wf,
int_subtype_base
\mforall{}[es:EO']. \mforall{}[nodes:bag(Id)].
((\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)))
{}\mRightarrow{} (\mforall{}e:E. \mforall{}epoch:\mBbbZ{}. \mforall{}i:Id. (<epoch, i> \mmember{} ler\_Config()(e) {}\mRightarrow{} (epoch > 0)))
{}\mRightarrow{} (\mforall{}[e1,e2:E]. \mforall{}[epoch1,epoch2:\mBbbZ{}]. \mforall{}[i1,i2:Id].
(<epoch2, i2> \mmember{} ler\_Config()(e2)
{}\mRightarrow{} <epoch1, i1> \mmember{} ler\_Nbr()(e1)
{}\mRightarrow{} (e1 <loc e2)
{}\mRightarrow{} (epoch1 \mleq{} epoch2))))
Date html generated:
2012_02_20-PM-06_07_39
Last ObjectModification:
2012_02_02-PM-02_40_22
Home
Index