Nuprl Lemma : send-once-no-prior-classrel
[Info,A:Type]. b:bag(A). es:EO+(Info). e:E. ((no Send(b) prior to e) 
(
first(e)) 
(bag-null(b)))
Proof not projected
Definitions occuring in Statement :
send-once-class: Send(b),
no-prior-classrel: (no X prior to e),
event-ordering+: EO+(Info),
es-first: first(e),
es-E: E,
assert: b,
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
or: P Q,
universe: Type,
bag-null: bag-null(bs),
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
no-prior-classrel: (no X prior to e),
or: P Q,
and: P 
Q,
implies: P Q,
rev_implies: P Q,
member: t 
T,
prop: 
,
alle-lt: e<e'.P[e],
not: 
A,
false: False,
assert: b,
btrue: tt,
guard: {T},
ifthenelse: if b then t else f fi ,
true: True,
cand: A c B,
squash: 
T,
decidable: Dec(P),
sq_type: SQType(T),
uimplies: b supposing a,
es-le: e 
loc e' ,
uiff: uiff(P;Q),
exists: 
x:A. B[x],
sq_stable: SqStable(P),
subtype: S 
T
Lemmas :
no-prior-classrel_wf,
send-once-class_wf,
classrel_wf,
es-locl_wf,
event-ordering+_inc,
es-E_wf,
assert_wf,
es-first_wf,
bag-null_wf,
event-ordering+_wf,
bag_wf,
es-init_wf,
decidable__assert,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_elim,
es-init-le,
es-first-init,
btrue_wf,
send-once-classrel,
bag-member_wf,
bag-member-not-bag-null,
sq_stable__assert,
btrue_neq_bfalse,
es-locl-first,
assert-bag-null,
bag-member-empty-iff
\mforall{}[Info,A:Type].
\mforall{}b:bag(A). \mforall{}es:EO+(Info). \mforall{}e:E. ((no Send(b) prior to e) \mLeftarrow{}{}\mRightarrow{} (\muparrow{}first(e)) \mvee{} (\muparrow{}bag-null(b)))
Date html generated:
2011_10_20-PM-03_23_01
Last ObjectModification:
2011_08_17-AM-11_32_08
Home
Index