Nuprl - mb_event_system_7 LEMMAs for s_DASH_unconditional_DASH_send1_DASH_rule

mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
9	Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. Thm* (rcv(l; tg) = k T = B) Thm* Thm* (f:(ABT). Thm* (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))])) Thm* ( Dsys Thm* (& (D:Dsys. Thm* (& (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]) Thm* (& (@source(l): ma-single-sends1() D Thm* (& ( Thm* (& (D Thm* (& (realizes es.(vartype(source(l);x) r A) Thm* (& (realizes es.& (e:E. Thm* (& (realizes es.& (loc(e) = source(l) Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k Knd (valtype(e) r B)) Thm* (& (realizes es.& (e:E. kind(e) = rcv(l; tg) Knd (valtype(e) r T)) Thm* (& (realizes es.& (e:E. Thm* (& (realizes es.& (loc(e) = source(l) Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k Knd Thm* (& (realizes es.& ( Thm* (& (realizes es.& ((e':E. Thm* (& (realizes es.& ((kind(e') = rcv(l; tg) Knd Thm* (& (realizes es.& ((& sender(e') = e E Thm* (& (realizes es.& ((& & (e'':E. Thm* (& (realizes es.& ((& & (kind(e'') = rcv(l; tg) Knd Thm* (& (realizes es.& ((& & ( Thm* (& (realizes es.& ((& & (sender(e'') = e E e'' = e' E) Thm* (& (realizes es.& ((& & val(e') = f((x when e),val(e)) T))))	[s-unconditional-send1-rule]
cites the following:
8	Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(T List)). Thm* (rcv(l; tg) = k T = B) Thm* Thm* @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f) Dsys Thm* & (D:Dsys. Thm* & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f) D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(source(l);x) r A) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = source(l) Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k Knd (valtype(e) r B)) Thm* & (realizes es.& (e:E. kind(e) = rcv(l; tg) Knd (valtype(e) r T)) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = source(l) Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((L:{e':E\| kind(e') = rcv(l; tg) Knd } List. Thm* & (realizes es.& (((e':E. Thm* & (realizes es.& ((((e' L) Thm* & (realizes es.& ((( Thm* & (realizes es.& (((kind(e') = rcv(l; tg) Knd & sender(e') = e E) Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2 L (e1 <loc e2)) Thm* & (realizes es.& ((& map(e'.val(e');L) = f((x when e),val(e)) T List)))	[s-sends-rule1]
0	Thm* f:Top, T:Type, L:T List. \|\|map(f;L)\|\| ~ \|\|L\|\|	[length-map]
0	Thm* a,x:T. (x [a]) x = a	[member_singleton]
1	Thm* es:ES, l:IdLnk, tg:Id, e:E. Thm* kind(e) = rcv(l; tg) Thm* Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)	[es-kind-rcv]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 7 Sections EventSystems Doc