Nuprl Lemma : send-once-loc-classrel
[Info,A:Type]. [b:Id 
bag(A)].
es:EO+(Info). e:E. v:A. (v 
send-once-loc-class(b)(e) 
bag-member(A;v;b loc(e)) 
(
first(e)))
Proof not projected
Definitions occuring in Statement :
send-once-loc-class: send-once-loc-class(b),
classrel: v X(e),
event-ordering+: EO+(Info),
es-first: first(e),
es-loc: loc(e),
es-E: E,
Id: Id,
assert: b,
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
universe: Type,
bag-member: bag-member(T;x;bs),
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
classrel: v X(e),
send-once-loc-class: send-once-loc-class(b),
and: P Q,
member: t T,
prop: 
,
eclass: EClass(A[eo; e]),
no-prior-classrel: (no X prior to e),
implies: P Q,
rev_implies: P Q,
alle-lt: e<e'.P[e],
not: 
A,
false: False,
uimplies: b supposing a,
decidable: Dec(P),
or: P 
Q,
subtype: S 
T
Lemmas :
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
Id_wf,
bag_wf,
classrel_wf,
once-class_wf,
es-loc_wf,
bag-member_wf,
assert_wf,
es-first_wf,
assert_witness,
no-prior-classrel_wf,
btrue_neq_bfalse,
es-locl_wf,
es-locl-first,
assert_elim,
iff_functionality_wrt_iff,
iff_weakening_uiff,
once-classrel,
decidable__assert,
es-pred_wf,
es-pred-locl,
es-loc-pred
\mforall{}[Info,A:Type]. \mforall{}[b:Id {}\mrightarrow{} bag(A)].
\mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}v:A.
(v \mmember{} send-once-loc-class(b)(e) \mLeftarrow{}{}\mRightarrow{} bag-member(A;v;b loc(e)) \mwedge{} (\muparrow{}first(e)))
Date html generated:
2011_10_20-PM-03_22_52
Last ObjectModification:
2011_08_25-PM-06_24_00
Home
Index