Nuprl Lemma : mu_ex_v5_send-single
[es:EO']. [m1,m2,init,p1,p2,i:Id]. [e:E]. [m:Message].
(<i, m> 
mu_ex_v5_main(init;m1;m2;p1;p2)(e) 
({<i, m>} = (mu_ex_v5_main(init;m1;m2;p1;p2) es e)))
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_main: mu_ex_v5_main(initial_token;m1;m2;proc1;proc2),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
implies: P Q,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
equal: s = t,
single-bag: {x},
bag: bag(T)
Definitions :
ge: i 
j ,
rev_implies: P 
Q,
iff: P Q,
true: True,
and: P 
Q,
squash: 
T,
bag-only: only(bs),
false: False,
implies: P Q,
not: 
A,
le: A 
B,
member: t T,
prop: 
,
exists: 
x:A. B[x],
nat: 
,
all: x:A. B[x],
bag-size: bag-size(bs),
uimplies: b supposing a,
bag-member: x bs,
es-sv-class: es-sv-class(es;X),
uall: [x:A]. B[x],
classrel: v X(e),
subtype: S 
T,
eclass: EClass(A[eo; e])
Lemmas :
single-bag_wf,
and_wf,
bag_wf,
equal_wf,
bag-only_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
classrel_wf,
member_null,
hd_member,
hd_wf,
length-one-member,
nat_wf,
true_wf,
squash_wf,
bag-size-one,
bag-size_wf,
mu_ex_v5_main_wf,
Message_wf,
Id_wf,
bag-member-size,
mu_ex_v5_send-at-most-one
\mforall{}[es:EO']. \mforall{}[m1,m2,init,p1,p2,i:Id]. \mforall{}[e:E]. \mforall{}[m:Message].
(<i, m> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e)
{}\mRightarrow{} (\{<i, m>\} = (mu\_ex\_v5\_main(init;m1;m2;p1;p2) es e)))
Date html generated:
2012_02_20-PM-07_04_35
Last ObjectModification:
2012_02_02-PM-03_03_25
Home
Index