Def MsgA
Def == ds:x:Id fp-> Type
Def == da:a:Knd fp-> Type
Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
Def == kl:KndIdLnk fp-> (tg:Id
Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop

is mentioned by

Thm* i:Id, M:{M:MsgA| Feasible(M) }. @i: M  System	[m-sys-at_wf]
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* L:MsgA List. ma-is-empty((L))  reduce(M,x. ma-is-empty(M) & x;True;L)	[assert-ma-join-list-is-empty]
Thm* L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)	[ma-join-list-is-empty]
Thm* L:MsgA List. ma-is-empty((L))	[ma-is-empty_wf_join]
Thm* L:MsgA List. (L)  MsgAForm	[msg-form-join-list]
Thm* MsgA r MsgAForm	[msga-sub-msg-form]
Thm* L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.B ||+ M)  (L) ||+ M)	[ma-join-list-compat2]
Thm* L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-compat]
Thm* L:MsgA List. (A,BL.A ||+ B)  (AL.Feasible(A))  Feasible((L))	[ma-join-list-feasible]
Thm* L:MsgA List, M:MsgA. (A,BL.A ||+ B)  (M  L)  M  (L)	[ma-sub-join-list]
Thm* L:MsgA List. (A,BL.A ||+ B)  (L)  MsgA	[ma-join-list_wf]
Thm* L:MsgA List.  Thm* (A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-property]
Thm* A,B,C:MsgA. A ||+ B  C ||+ A  C ||+ B  C ||+ A  B	[ma-compat-join]
Thm* A,B:MsgA. Thm* A || B Thm*  Thm* ma-frame-compatible(A; B) Thm*  Thm* ma-sframe-compatible(A; B)  Feasible(A)  Feasible(B)  Feasible(A  B)	[ma-join-feasible]
Thm* A:MsgA. A ||+	[ma-empty-compat-right]
Thm* A:MsgA.  ||+ A	[ma-empty-compat-left]
Thm* A,B:MsgA. A ||+ B  B ||+ A	[ma-compat-symmetry]
Thm* A,B,C:MsgA. Thm* A || B Thm*  Thm* ma-frame-compatible(A; B) Thm*  Thm* ma-sframe-compatible(A; B) Thm*  Thm* C || A Thm*  Thm* ma-frame-compatible(C; A) Thm*  Thm* ma-sframe-compatible(C; A) Thm*  Thm* C || B Thm*  Thm* ma-frame-compatible(C; B) Thm*  Thm* ma-sframe-compatible(C; B) Thm*  Thm* C || A  B & ma-frame-compatible(C; A  B) & ma-sframe-compatible(C; A  B)	[ma-compatible-join]
Thm* A:MsgA. ma-sframe-compatible(; A)	[ma-empty-sframe-compatible-left]
Thm* A:MsgA. ma-frame-compatible(A; )	[ma-empty-frame-compatible-right]
Thm* A:MsgA. ma-sframe-compatible(A; )	[ma-empty-sframe-compatible-right]
Thm* A:MsgA. ma-frame-compatible(; A)	[ma-empty-frame-compatible-left]
Thm* A,B:MsgA. ma-sframe-compatible(A; B)  Prop	[ma-sframe-compatible_wf]
Thm* A,B:MsgA. ma-frame-compatible(A; B)  Prop	[ma-frame-compatible_wf]
Thm* M:MsgA. Feasible(M)  Prop{i'}	[ma-feasible_wf]
Thm* T,T':Type, x:Id, c:T, a:Id, P:(TT'Prop). Thm* ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v))  MsgA	[ma-single-pre-init1_wf]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp), Thm* init:x:Id fp-> ds(x)?Void. Thm* (with ds: ds init: initaction a:T precondition a(v) is P)  MsgA	[ma-single-pre-init_wf]
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]
Thm* i:Id, A,B:MsgA. @i: A  @i: B  A  B	[s-at-sub-s-at]
Def System == {M:(IdMsgA)| loc:Id. Feasible(M(loc)) }	[msystem]

In prior sections: mb event system 5

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