Def IdLnk == IdId

is mentioned by

Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* source(l) = i Thm*  Thm* @i: ma-single-sends(ds; da; k; l; f)  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-sends(ds; da; k; l; f)  D Thm* & ( Thm* & (D  Thm* & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (isrcv(e) Thm* & (realizes es.& ( Thm* & (realizes es.& (lnk(e) = l  IdLnk Thm* & (realizes es.& ( Thm* & (realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k  Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.  Thm* & (realizes es.& (((e':E.  Thm* & (realizes es.& ((((e'  L) Thm* & (realizes es.& ((( Thm* & (realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E) Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2)) Thm* & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L) Thm* & (realizes es.& ((& = Thm* & (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f) Thm* & (realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List)))	[s-sends-rule]
Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* source(l) = i Thm*  Thm* d-single-sends(i; ds; da; k; l; f)  Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& (e:E.  Thm* realizes es.& (isrcv(e) Thm* realizes es.& ( Thm* realizes es.& (lnk(e) = l  IdLnk Thm* realizes es.& ( Thm* realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id Thm* realizes es.& ( Thm* realizes es.& (kind(e) = k  Knd Thm* realizes es.& ( Thm* realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.  Thm* realizes es.& (((e':E.  Thm* realizes es.& ((((e'  L) Thm* realizes es.& ((( Thm* realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E) Thm* realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2)) Thm* realizes es.& ((& map(e'.<tag(e'),val(e')>;L) Thm* realizes es.& ((& = Thm* realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f) Thm* realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List))	[better-sends-rule]
Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* source(l) = i Thm*  Thm* d-single-sends(i; ds; da; k; l; f)  Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& (e:E.  Thm* realizes es.& (isrcv(e) Thm* realizes es.& ( Thm* realizes es.& (lnk(e) = l  IdLnk Thm* realizes es.& ( Thm* realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& ({m:Msg| source(mlnk(m)) = i } r Msg Thm* realizes es.& (((l,tg. da(rcv(l; tg))?Top))) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id Thm* realizes es.& ( Thm* realizes es.& (kind(e) = k  Knd Thm* realizes es.& ( Thm* realizes es.& (sends(l;e) Thm* realizes es.& (= Thm* realizes es.& (tagged-messages(l;z.(z when e);val(e);f) Thm* realizes es.& ( Msg((l,tg. da(rcv(l; tg))?Top)) List)	[sends-rule]
Thm* i:Id, L:Knd List, l:IdLnk, tg:Id. Thm* @i: only L sends on (l with tg)  Thm* realizes es.e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L)	[sframe-rule]
Thm* D:Dsys, L:Id List. Thm* (i:Id. (i  L)  ma-is-empty(M(i))) Thm*  Thm* (i:Id. Feasible(M(i))) Thm*  Thm* (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L) Thm* (iL.(ltgma-outlinks(M(i);i). Thm* interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg))))) Thm*  Thm* d-feasible(D)	[finite-support-feasible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* xdom(ds). A=ds(x)   A Thm*  Thm* kdom(da). A=da(k)   A  Feasible(ma-single-sends(ds; da; k; l; f))	[ma-single-sends-feasible]
Thm* l:IdLnk, tg:Id, L:MsgA List. Thm* (ML.T r M.din(l,tg))  (T r (L).din(l,tg))	[sub-join-list-din]
Thm* L:MsgA List, P:(IdLnkIdTypeProp), i:Id. Thm* (ML.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks((L);i).P(ltg))	[ma-outlinks-join-list]
Thm* A,B:MsgAForm, ltg:(IdLnkIdType), i:Id. Thm* (ltg  ma-outlinks(A  B;i)) Thm*  Thm* (ltg  ma-outlinks(A;i))  (ltg  ma-outlinks(B;i))	[ma-outlinks-join]
Thm* M:MsgAForm, i:Id. ma-outlinks(M;i)  (IdLnkIdType) List	[ma-outlinks-wf2]
Thm* A,B,T:Type, x:Id, a:Knd, tg:Id, l:IdLnk, f:(AB(T List)). Thm* (a = rcv(l; tg)  T = B) Thm*  Thm* ma-single-sends1(A; B; T; x; a; l; tg; f)  MsgA	[ma-single-sends1_wf]

In prior sections: mb event system 1 mb event system 2 mb event system 3 mb event system 4 mb event system 5

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html