Nuprl Lemma : base-noloc-classrel
[T:Type]. [es:EO']. [e:E]. [v:T]. [hdr:Name].
uiff(v 
Base(hdr;T)(e);
(es-header(es;e) = hdr) 
(
msg-type(info(e)) == T) (v = msg-body(info(e))))
Proof not projected
Definitions occuring in Statement :
base-headers-msg-val: Base(hdr;typ),
es-header: es-header(es;e),
msg-type: msg-type(msg),
msg-body: msg-body(msg),
Message: Message,
classrel: v X(e),
es-info: info(e),
event-ordering+: EO+(Info),
es-E: E,
name: Name,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
squash: T,
and: P Q,
universe: Type,
equal: s = t,
eq_term: a == b
Definitions :
msg-has-type: msg-has-type(m;T),
implies: P 
Q,
all: x:A. B[x],
cand: A c B,
bag-member: x bs,
prop: 
,
true: True,
uimplies: b supposing a,
member: t T,
pi1: fst(t),
es-header: es-header(es;e),
and: P Q,
squash: T,
classrel: v X(e),
uiff: uiff(P;Q),
uall: [x:A]. B[x],
guard: {T},
has-valueall: has-valueall(a),
bfalse: ff,
btrue: tt,
band: p 
q,
ifthenelse: if b then t else f fi ,
cond-msg-body: cond-msg-body(hdr;typ;m),
assert: b,
base-headers-msg-val: Base(hdr;typ),
pMsg: pMsg(P.M[P]),
Message: Message,
false: False,
unit: Unit,
bool: 
,
not: 
A,
sq_stable: SqStable(P),
subtype: S 
T,
it: 
Lemmas :
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
msg-body_wf2,
type-valueall-type,
msg-type_wf,
eq_term_wf,
assert_wf,
es-info_wf,
name_wf,
squash_wf,
base-headers-msg-val_wf,
Message_wf,
classrel_wf,
name_eq_wf,
uiff_wf,
empty-bag_wf,
not_functionality_wrt_uiff,
bag-member-empty,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
single-bag_wf,
bag-member_wf,
bag-member-single,
assert-eq_term,
eqtt_to_assert,
equal_wf,
uiff_transitivity,
bool_wf,
assert-name_eq,
sq_stable__bag-member
\mforall{}[T:Type]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[v:T]. \mforall{}[hdr:Name].
uiff(v \mmember{} Base(hdr;T)(e);\mdownarrow{}(es-header(es;e) = hdr)
\mwedge{} (\muparrow{}msg-type(info(e)) == T)
\mwedge{} (v = msg-body(info(e))))
Date html generated:
2012_01_23-PM-12_53_17
Last ObjectModification:
2011_12_11-PM-09_48_03
Home
Index