Def	switch_inv(E; tr)	[switch_inv2001_03_15_DASH_PM_DASH_12_53_21]
Def	x R_del(E) y	[R_del]
Def	No-dup-send(E)	[no_duplicate_send]	mb structures
Def	EventStruct	[event_str]	mb structures
Def	(L -msg(a;b) L1)	[remove_msgs]
Def	TaggedEventStruct	[tagged_event_str]	mb structures
Def	MessageStruct	[message_str]	mb structures
Def	DecidableEquiv	[dequiv]	mb structures
Def	EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def	Refl(T;x,y.E(x;y))	[refl]	rel 1
Def	(xL.P(x))	[l_exists]	mb list 2
Def	totalorder(E)	[totalorder]
Def	single-tag-decomposable(E)	[single_tag_decomposable]
Def	MCS(E)	[memoryless_composable_safety]
Def	switchable0(E)	[switchable0]
Def	switchable(E)	[b_switchable]
Def	composableR(E)	[R_composable]
Def	(xL.P(x))	[l_all]	mb list 2
Def	agree_on_common(T;as;bs)	[agree_on_common]	mb list 1
Def	(x l)	[l_member]	mb list 1
Def		[bool]	bool 1
Def	P Q	[iff]	core
Def	Tag-by-msg(E)	[P_tag_by_msg]
Def	PTrue	[PTrue]
Def	I fuses P	[fusion_condition]
Def	R_ad_normal(tr)	[R_ad_normal]
Def	R_strong_safety(E)	[R_strong_safety]
Def	P Q	[prop_and]	mb nat
Def	Structure	[struct]	mb structures
Def	TraceProperty(E)	[trace_property]
Def	tag_splitable(E;R)	[tag_splitable]	mb structures
Def	switch-decomposable(E)	[switch_decomposable]
Def	AD-normal(E)	[switch_normal]
Def	R_permutation(E)	[R_permutation]
Def	R^-1	[rel_inverse]	mb nat
Def	switchR(tr)	[switch_inv_rel]
Def	local_deliver_property(E;P)	[local_deliver_property]
Def	adR(E)	[R_ad]
Def	P o evt	[compose_map]	mb structures
Def	induced_event_str(E;A;f)	[induced_event_str]	mb structures
Def	full_switch_inv(E;A;evt;tg;tr_u;tr_l)	[full_switch_inv]
Def	true	[btrue]	bool 1
Def	sublist(T;L1;L2)	[sublist]	mb list 1
Def	layerR(E)	[layer_rel]
Def	delayableR(E)	[R_delayable]
Def	asyncR(E)	[R_async]
Def	R(tg)	[tag_rel]
Def	swap adjacent[P(x;y)]	[swap_adjacent]	mb list 2
Def	swap(L;i;j)	[swap]	mb list 2
Def	x somewhere delivered before y	[delivered_before_somewhere]
Def	switch_inv(E)	[switch_inv]
Def	x delivered at time k	[delivered_at]
Def	C(Q)	[message_closure]
Def	No-dup-deliver(E)	[P_no_dup]
Def	Causal(E)	[P_causal]
Def	(L o f)	[permute_list]	mb list 2
Def	l[i]	[select]	list 1
Def	tr delivered at p	[deliveries_at]
Def	memorylessR(E)	[R_memoryless]
Def	nth_tl(n;as)	[nth_tl]	list 1
Def	ij	[le_int]	bool 1
Def	b	[bnot]	bool 1
Def	=msg=(E)	[event_msg_eq]	mb structures
Def	Label	[lbl]	mb label
Def	< tr > _tg	[tag_sublist]	mb structures
Def	=(M)	[msg_eq]	mb structures
Def	l1 = l2	[eq_lbl]	mb basic
Def	ground_ptn(p)	[ground_ptn]	mb basic
Def	pq	[band]	bool 1
Def	filter(P;l)	[filter]	mb list 1
Def	reduce(f;k;as)	[reduce]	list 1
Def	< A,evt,tg > (E)	[induced_tagged_event_str]	mb structures
Def	loc(E)	[event_loc]	mb structures
Def	P & Q	[and]	core
Def	x:A. B(x)	[exists]	core
Def	x f y	[infix_ap]	core
Def	tag(E)	[event_tag]	mb structures
Def	increasing(f;k)	[increasing]	mb basic
Def	{i..j}	[int_seg]	int 1
Def	R^*	[rel_star]	mb nat
Def		[nat]	int 1
Def	i j < k	[lelt]	int 1
Def	AB	[le]	core
Def	is-deliver(E)(x)	[event_is_deliver]	mb structures
Def	Dec(P)	[decidable]	core
Def	A	[not]	core
Def	send-enabledR(E)	[R_send_enabled]
Def	is-send(E)	[event_is_snd]	mb structures
Def	b	[assert]	bool 1
Def	P Q	[implies]	core
Def	||as||	[length]	list 1
Def	x:A. B(x)	[all]	core
Def	True	[true]	core
Def	safetyR(E)	[R_safety]
Def	l1 l2	[iseg]	mb list 1
Def	mklist(n;f)	[mklist]	mb list 1
Def	as @ bs	[append]	list 1
Def	Trace(E)	[str_trace]	mb structures
Def	P refines Q	[tr_refines]
Def	|S|	[carrier]	mb structures
Def	P Q	[or]	core
Def	Prop	[prop]	core
Def	msg(E)	[event_msg]	mb structures
Def	map(f;as)	[map]	list 1
Def	MS(E)	[event_msg_str]	mb structures
Def	(ternary) R preserves P	[preserved_by2]	mb nat
Def	R preserves P	[preserved_by]	mb nat
Def	R1 R2	[rel_or]	mb nat
Def	Top	[top]	core
Def	P Q	[rev_implies]	core
Def	f o g	[compose]	fun 1
Def	uid(MS)	[msg_id]	mb structures
Def	sender(MS)	[msg_sender]	mb structures
Def	content(MS)	[msg_content]	mb structures
Def	cEQ(MS)	[msg_content_eq]	mb structures
Def	=(DE)	[eq_dequiv]	mb structures
Def	2of(t)	[pi2]	core
Def	1of(t)	[pi1]	core
Def	Pattern	[ptn]	mb basic
Def	Case ptn_var(x) = > body(x) cont	[case_ptn_var]	mb basic
Def	Case ptn_int(x) = > body(x) cont	[case_ptn_int]	mb basic
Def	hd(l)	[hd]	list 1
Def	Default = > body	[case_default]	prog 1
Def	Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def	Case(value) body	[case]	prog 1
Def	x=yAtom	[eq_atom]	bool 1
Def	(i, j)	[flip]	mb nat
Def	R^n	[rel_exp]	mb nat
Def	primrec(n;b;c)	[primrec]	mb nat
Def	i=j	[eq_int]	bool 1
Def	Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def	ptn_con(T)	[ptn_con]	mb basic
Def	tl(l)	[tl]	list 1
Def	inl(x) = > body(x) cont	[case_inl]	prog 1
Def	inr(x) = > body(x) cont	[case_inr]	prog 1
Def	i < j	[lt_int]	bool 1
Def	Trans x,y:T. E(x;y)	[trans]	rel 1
Def	Sym x,y:T. E(x;y)	[sym]	rel 1

About: