Nuprl - mb_hybrid LEMMAs for P_no_dup

Rank	Theorem	Name
3	Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E)	[P_no_dup_composable]
cites
2	Thm* E:EventStruct. EquivRel(\|E\|)(_1 =msg=(E) _2)	[event_msg_eq_equiv]
0	Thm* as,bs:T List. \|\|as @ bs\|\| = \|\|as\|\|+\|\|bs\|\|	[length_append]
1	Thm* as,bs:T List, i:\|\|as\|\|. (as @ bs)[i] = as[i]	[select_append_front]
0	Thm* L:T List, i:\|\|L\|\|. (L[i] L)	[select_member]
1	Thm* as,bs:T List, i:{\|\|as\|\|..(\|\|as\|\|+\|\|bs\|\|)}. (as @ bs)[i] = bs[(i-\|\|as\|\|)]	[select_append_back]