Nuprl - mb_event_system_6 LEMMAs for ma_DASH_join_DASH_list_DASH

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
9	Thm* L:MsgA List. (A,BL.A \|\|+ B) (AL.Feasible(A)) Feasible((L))	[ma-join-list-feasible]
cites the following:
0	Thm* Feasible()	[ma-empty-feasible]
2	Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))	[l_all_cons]
1	Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y)) (x,yL.P(x,y)) & (yL.P(x,y))	[pairwise-cons]
8	Thm* L:MsgA List. Thm* (A,BL.A \|\|+ B) (L) MsgA & (M:MsgA. (BL.M \|\|+ B) M \|\|+ (L))	[ma-join-list-property]
6	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]

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html