Def		switch_inv(E; tr)	[switch_inv2001_03_15_DASH_PM_DASH_12_53_21]	mb hybrid
Def		x R_del(E) y	[R_del]	mb hybrid
Def		tTop	[st_top]	mb automata 1
Def		relname_eq(x)	[relname_eq]	mb automata 1
Def		relname_other(x)	[relname_other]	mb automata 1
Def		outl(x)	[outl]	union
Def		outr(x)	[outr]	union
Def		fappend(f;n;x)	[fappend]	mb nat
Def		...	[hide]	mb basic
Def		ptn_int(x)	[ptn_int]	mb basic
Def		ptn_var(x)	[ptn_var]	mb basic
Def		const_ptn(l)	[const_ptn]	mb basic
Def		int_ptn(l)	[int_ptn]	mb basic
Def		var_ptn(l)	[var_ptn]	mb basic
Def		left_ptn(l)	[left_ptn]	mb basic
Def		right_ptn(l)	[right_ptn]	mb basic
Def		StAntiSym(T;x,y.R(x;y))	[st_anti_sym]	rel 1
Def		Irrefl(T;x,y.E(x;y))	[irrefl]	rel 1
Def		left_child(t)	[left_child]	mb tree
Def		right_child(t)	[right_child]	mb tree
Def		leaf_value(t)	[leaf_value]	mb tree
Def		Default = > body EndSwitch	[switch_default]	prog 1
Def		< x,y > = > body(x;y)	[case_pair]	prog 1
Def		x::y = > body(x;y) cont	[case_cons]	prog 1
Def		[] = > body cont	[case_nil]	prog 1
Def		= > body	[case_it]	prog 1
Def		x:body	[case_bind]	prog 1
Def		< < "a", b > , c, 1 > = > body(b;c) cont	[case_pattern1]	prog 1
Def		< a, inl < < "a", b > , c, 1 > > = > body(a;b;c) cont	[case_pattern2]	prog 1
Def		< a, inl < < "a", b > , c, 1 > >	[pattern2]	prog 1
Def		union1()	[union1]	prog 1
Def		union1_term1(x) = > body(x) cont	[case_union1_term1]	prog 1
Def		union1_term1(x)	[union1_term1]	prog 1
Def		union1_term2(x) = > body(x) cont	[case_union1_term2]	prog 1
Def		union1_term2(x)	[union1_term2]	prog 1
Def		union1_term3(x) = > body(x) cont	[case_union1_term3]	prog 1
Def		union1_term3(x)	[union1_term3]	prog 1
Def		enum1_switch(value;el1;el2;el3)	[enum1_switch]	prog 1
Def		enum1_el1 = > body cont	[case_enum1_el1]	prog 1
Def		enum1_el2 = > body cont	[case_enum1_el2]	prog 1
Def		enum1_el3 = > body cont	[case_enum1_el3]	prog 1
Def		module1_type(prop)	[module1_type]	prog 1
Def		t.tag	[module1_tag]	prog 1
Def		t.data	[module1_data]	prog 1
Def		module1(tag, data) = > body(tag;data)	[case_module1]	prog 1
Def		module1(tag, data)	[module1]	prog 1
Def		For{T,op,id} x as. f(x)	[for]	list 1
Def		ForHdTl{A,f,k} h::t as. g(h;t)	[for_hdtl]	list 1
Def		mapc(f)	[mapc]	list 1
Def		pq	[bxor]	bool 1
Def		pq	[rev_bimplies]	bool 1
Def		i j k	[lele]	int 1
Def		S T	[suptype]	int 1
Def		t ...$L	[label]	core
Def		???	[error]	core
Def		I	[icomb]	core
Def		K	[kcomb]	core
Def		S	[scomb]	core
Def		let x,y,z = a in t(x;y;z)	[spread3]	core
Def		let w,x,y,z = a in t(w;x;y;z)	[spread4]	core
Def		let a,b,c,d,e = u in v(a;b;c;d;e)	[spread5]	core
Def		let a,b,c,d,e,f = u in v(a;b;c;d;e;f)	[spread6]	core
Def		let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g)	[spread7]	core
Def		XM	[xmiddle]	core
Def		[x]{T}	[type_inj]	core
Def		rel_arg_typ(rn;i;de)	[rel_arg_typ]	mb automata 1
Def		trace_env(d)	[trace_env]	mb automata 1
Def		[[s]] rho	[sig_mng]	mb automata 3
Def		sig()	[sig]	mb automata 2
Def		subst_mentions_trace(as)	[subst_mentions_trace]	mb automata 3
Def		{p}	[record_pair]	mb record
Def		r	[pred_rel]	mb automata 1
Def		closed_pred(p)	[closed_pred]	mb automata 3
Def		c1 = c2	[col_equal]	mb collection
Def		(P)'	[pred_addprime]	mb automata 3
Def		pred_unprime(P)	[pred_unprime]	mb automata 3
Def		c1 c2	[col_le]	mb collection
Def		[[A]] rho de e	[ioa_mng]	mb automata 4
Def		ioa_all(I; i.A(i))	[ioa_all]	mb automata 1
Def		ioa{i:l}()	[ioa]	mb automata 3
Def		ioa_mentions_trace(A)	[ioa_mentions_trace]	mb automata 3
Def		wp_rel(A;a;r)	[wp_rel]	mb automata 4
Def		wp2_rel(A;a;r)	[wp2_rel]	mb automata 3
Def		pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr)	[pred_mng_2]	mb automata 3
Def		wp2(A;a;Q)	[wp2]	mb automata 3
Def		tc_ioa(A;de)	[tc_ioa]	mb automata 4
Def		single_valued_decls(c)	[single_valued_decls]	mb automata 2
Def		rel_eq(a;b)	[rel_eq]	mb automata 3
Def		sm{i:l}()	[sm]	mb state machine
Def		covers_rel(A;r)	[covers_rel]	mb automata 2
Def		wp(A;a;Q)	[wp]	mb automata 4
Def		trace_consistent_vc(rho;da;R;v)	[trace_consistent_vc]	mb automata 4
Def		covers_pred(A;p)	[covers_pred]	mb automata 3
Def		tc_vcs{i}(vs;ds;da;de)	[tc_vcs]	mb automata 4
Def		VCs	[vcs]	mb automata 2
Def		[[vs]] rho ds da de e s tr	[vcs_mng]	mb automata 4
Def		VCs(A;I)	[ioa_inv_vc]	mb automata 4
Def		guarded_trace(da;e;I)	[guarded_trace]	mb automata 3
Def		(M |= always s,t.P(s;t))	[trace_inv]	mb state machine
Def		let x = a in b(x)	[let]	core
Def		closed_term(t)	[closed_term]	mb automata 2
Def		unzip(as)	[unzip]	mb list 1
Def		ab	[arrow]	mb automata 1
Def		SQType(T)	[sq_type]	sqequal 1
Def		tc1(r;de)	[tc1]	mb automata 1
Def		No-dup-send(E)	[no_duplicate_send]	mb structures
Def		EventStruct	[event_str]	mb structures
Def		(L -msg(a;b) L1)	[remove_msgs]	mb hybrid
Def		(xL.P(x))	[l_exists]	mb list 2
Def		Tag-by-msg(E)	[P_tag_by_msg]	mb hybrid
Def		TaggedEventStruct	[tagged_event_str]	mb structures
Def		PTrue	[PTrue]	mb hybrid
Def		I fuses P	[fusion_condition]	mb hybrid
Def		R_ad_normal(tr)	[R_ad_normal]	mb hybrid
Def		R_strong_safety(E)	[R_strong_safety]	mb hybrid
Def		P Q	[prop_and]	mb nat
Def		Structure	[struct]	mb structures
Def		TraceProperty(E)	[trace_property]	mb hybrid
Def		tag_splitable(E;R)	[tag_splitable]	mb structures
Def		totalorder(E)	[totalorder]	mb hybrid
Def		single-tag-decomposable(E)	[single_tag_decomposable]	mb hybrid
Def		switch-decomposable(E)	[switch_decomposable]	mb hybrid
Def		AD-normal(E)	[switch_normal]	mb hybrid
Def		MCS(E)	[memoryless_composable_safety]	mb hybrid
Def		R_permutation(E)	[R_permutation]	mb hybrid
Def		R^-1	[rel_inverse]	mb nat
Def		switchR(tr)	[switch_inv_rel]	mb hybrid
Def		local_deliver_property(E;P)	[local_deliver_property]	mb hybrid
Def		switchable0(E)	[switchable0]	mb hybrid
Def		switchable(E)	[b_switchable]	mb hybrid
Def		adR(E)	[R_ad]	mb hybrid
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]	mb hybrid
Def		interleaving(T;L1;L2;L)	[interleaving]	mb list 2
Def		null(as)	[null]	list 1
Def		last(L)	[last_RENAMED]	mb list 1
Def		compose_flips(L)	[compose_flips]	mb list 2
Def		x before y l	[l_before]	mb list 1
Def		guarded_permutation(T;P)	[guarded_permutation]	mb list 2
Def		Bij(A; B; f)	[biject]	fun 1
Def		count(x < y in L | P(x;y))	[count_pairs]	mb list 1
Def		i:I M(i)	[sm_all]	mb state machine
Def		(f o M)	[sm_a_rename]	mb state machine
Def		(M |= initially x,tr.P(x;tr))	[initially]	mb state machine
Def		(M |= x,tr.P(x;tr) while Q(x;tr))	[while]	mb state machine
Def		{i...j}	[int_iseg]	int 1
Def		ij	[ge]	core
Def		A List	[listp]	mb list 1
Def		sublist_occurence(T;L1;L2;f)	[sublist_occurence]	mb list 1
Def		interleaving_occurence(T;L1;L2;L;f1;f2)	[interleaving_occurence]	mb list 1
Def			[nat_plus]	int 1
Def		i = j	[pm_equal]	int 2
Def		|i|	[absval]	int 2
Def		Preorder(T;x,y.R(x;y))	[preorder]	rel 1
Def		gcd(a;b)	[gcd]	num thy 1
Def		x:A. B(x)	[sq_exists]	core
Def		CoPrime(a,b)	[coprime]	num thy 1
Def		SqStable(P)	[sq_stable]	core
Def		atomic(a)	[atomic]	num thy 1
Def		prime(a)	[prime]	num thy 1
Def		a = b mod m	[eqmod]	num thy 1
Def		fib(n)	[fib]	num thy 1
Def		isl(x)	[isl]	union
Def		nondecreasing(f;k)	[nondecreasing]	mb nat
Def		fadd(f;g)	[fadd]	mb nat
Def		R1 = > R2	[rel_implies]	mb nat
Def		f^n	[fun_exp]	mb nat
Def		search(k;P)	[search]	mb nat
Def		dec2bool(d)	[dec2bool]	mb basic
Def		Decision	[decision]	mb basic
Def		Symmetrize(x,y.R(x;y);a;b)	[symmetrize]	rel 1
Def		IsEqFun(T;eq)	[eqfun_p]	rel 1
Def		strict_part(x,y.R(x;y);a;b)	[strict_part]	rel 1
Def		Linorder(T;x,y.R(x;y))	[linorder]	rel 1
Def		is_leaf(t)	[is_leaf]	mb tree
Def		enum1()	[enum1]	prog 1
Def		rev(as)	[reverse]	list 1
Def		as[m..n]	[segment]	list 1
Def		as\[i]	[reject]	list 1
Def		f{m..n}	[listify]	list 1
Def		A List(n)	[list_n]	list 1
Def		i > j	[gt]	core
Def		{...i}	[int_lower]	int 1
Def		imin(a;b)	[imin]	int 2
Def		a -- b	[ndiff]	int 2
Def		Rem(a;n;r)	[rem_nrel]	int 2
Def		a mod n	[modulus]	int 2
Def		a n	[div_floor]	int 2
Def		WellFnd{i}(A;x,y.R(x;y))	[wellfounded]	well fnd
Def		{i...}	[int_upper]	int 1
Def		b2i(b)	[b2i]	bool 1
Def		p=q	[eq_bool]	bool 1
Def		A ~~ B	[one_one_corr]	fun 1
Def		Stable{P}	[stable]	core
Def		{a:T}	[singleton]	core
Def		{!x:T | P(x)}	[unique_set]	core
Def		a = !x:T. Q(x)	[uni_sat]	core
Def		tc_vc(v;ds;da;de)	[tc_vc]	mb automata 4
Def		tc_pred(P;ds;da;de)	[tc_pred]	mb automata 4
Def		tc(r;ds;da;de)	[tc]	mb automata 3
Def		tc_eff(ef;ds;de)	[tc_eff]	mb automata 4
Def		tc_smt(s;ds;da;de)	[tc_smt]	mb automata 3
Def		vc_mng(v;rho;ds;da;de;e;s;tr)	[vc_mng]	mb automata 4
Def		term_types(ds;da;de;t)	[term_types]	mb automata 3
Def		dec_lookup(ds;x)	[dec_lookup]	mb automata 2
Def		[[p]] rho ds da de e s a tr	[pred_mng]	mb automata 3
Def		trace_consistent_pred(rho;da;R;p)	[trace_consistent_pred]	mb automata 4
Def		trace_consistent_rel(rho;da;R;r)	[trace_consistent_rel]	mb automata 3
Def		trace_consistent(rho;da;R;t)	[trace_consistent]	mb automata 3
Def		[[ds]] rho	[decls_mng]	mb automata 3
Def		ioa_trans_all{i}(A;I)	[ioa_trans_all]	mb automata 4
Def		ioa_trans(A;a;I)	[ioa_trans]	mb automata 4
Def		smts_eff_pred(ss;p)	[smts_eff_pred]	mb automata 4
Def		smts_eff_rel(ss;r)	[smts_eff_rel]	mb automata 3
Def		st_app(c1;c2)	[st_app]	mb automata 2
Def		(xc.f(x))	[col_accum]	mb collection
Def		[[sts]] rho	[sts_mng]	mb automata 2
Def		action_effect(a;es;fs)	[action_effect]	mb automata 2
Def		(xc.P(x))	[col_all]	mb collection
Def		action_pre(a;ps)	[action_pre]	mb automata 2
Def		P Q	[pred_and]	mb automata 1
Def		col_subst(c;r)	[col_subst]	mb automata 3
Def		col_subst2(c;r)	[col_subst2]	mb automata 3
Def		col_map_subst(x.f(x);c)	[col_map_subst]	mb automata 2
Def		smts_eff(ss;x)	[smts_eff]	mb automata 2
Def		smt_terms(c)	[smt_terms]	mb automata 2
Def		< f(x) | x c >	[col_map]	mb collection
Def		a +* b	[vcs_add]	mb automata 2
Def		covers_var(A;x)	[covers_var]	mb automata 2
Def		pred_mentions(p;x)	[pred_mentions]	mb automata 2
Def		col_list_prod(l)	[col_list_prod]	mb collection
Def		< x c | P(x) >	[col_filter]	mb collection
Def		a + b	[col_add]	mb collection
Def		i:I. C(i)	[col_union]	mb collection
Def		x c	[col_member]	mb collection
Def		P Q	[implies]	core
Def		pre()	[pre]	mb automata 3
Def		< *v* >	[vcs_singleton]	mb automata 2
Def		vc{i:l}()	[vc]	mb automata 2
Def		qimp{i:l}()	[qimp]	mb automata 2
Def		imp{i:l}()	[imp]	mb automata 2
Def		Fmla	[pred]	mb automata 1
Def		rel()	[rel]	mb automata 2
Def		x:A. B(x)	[all]	core
Def		t.typ	[eff_typ]	mb automata 1
Def		frame()	[frame]	mb automata 2
Def		eff()	[eff]	mb automata 2
Def		dec()	[dec]	mb automata 2
Def		smt()	[smt]	mb automata 2
Def		st_app1(s1;s2)	[st_app1]	mb automata 2
Def		relname()	[relname]	mb automata 2
Def		SimpleType	[st]	mb automata 1
Def		< x >	[col_singleton]	mb collection
Def		t.smt	[eff_smt]	mb automata 1
Def		t.var	[frame_var]	mb automata 1
Def		t.typ	[frame_typ]	mb automata 1
Def		t.acts	[frame_acts]	mb automata 1
Def		rel_mentions(r;x)	[rel_mentions]	mb automata 2
Def		composableR(E)	[R_composable]	mb hybrid
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		layerR(E)	[layer_rel]	mb hybrid
Def		R(tg)	[tag_rel]	mb hybrid
Def		R^*	[rel_star]	mb nat
Def			[nat]	int 1
Def		sublist(T;L1;L2)	[sublist]	mb list 1
Def		delayableR(E)	[R_delayable]	mb hybrid
Def		asyncR(E)	[R_async]	mb hybrid
Def		swap adjacent[P(x;y)]	[swap_adjacent]	mb list 2
Def		C(Q)	[message_closure]	mb hybrid
Def		x somewhere delivered before y	[delivered_before_somewhere]	mb hybrid
Def		No-dup-deliver(E)	[P_no_dup]	mb hybrid
Def		Causal(E)	[P_causal]	mb hybrid
Def		switch_inv(E)	[switch_inv]	mb hybrid
Def		disjoint_sublists(T;L1;L2;L)	[disjoint_sublists]	mb list 1
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def		Div(a;n;q)	[div_nrel]	int 2
Def		i j < k	[lelt]	int 1
Def		AB	[le]	core
Def		is-deliver(E)(x)	[event_is_deliver]	mb structures
Def		x delivered at time k	[delivered_at]	mb hybrid
Def		Dec(P)	[decidable]	core
Def		reducible(a)	[reducible]	num thy 1
Def			[int_nzero]	int 1
Def		a b	[nequal]	core
Def		A	[not]	core
Def		t.frame	[ioa_frame]	mb automata 1
Def		t.term	[smt_term]	mb automata 1
Def		[[r]] rho ds da de e s a tr	[rel_mng]	mb automata 3
Def		[[t]] e s a tr	[term_mng]	mb automata 1
Def		t.lbl	[smt_lbl]	mb automata 1
Def		t.kind	[eff_kind]	mb automata 1
Def		t.eff	[ioa_eff]	mb automata 1
Def		rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)	[rel_mng_2]	mb automata 3
Def		[[t]] e s s' a tr	[term_mng2]	mb automata 2
Def		tre.P	[tproj]	mb automata 1
Def		tr | P	[trace_projection]	mb events
Def		kind(a)	[kind]	mb record
Def		t.kind	[pre_kind]	mb automata 1
Def		t.pre	[ioa_pre]	mb automata 1
Def		t.init	[ioa_init]	mb automata 1
Def		t.ds	[ioa_ds]	mb automata 1
Def		t.da	[ioa_da]	mb automata 1
Def		tappend(tr;a)	[tappend]	mb automata 1
Def		vc_hyp(v)	[vc_hyp]	mb automata 2
Def		t.hyp	[qimp_hyp]	mb automata 2
Def		t.lbl	[qimp_lbl]	mb automata 2
Def		t.hyp	[imp_hyp]	mb automata 2
Def		t.lbl	[dec_lbl]	mb automata 1
Def		rel_unprime(r)	[rel_unprime]	mb automata 2
Def		rel_subst(as;r)	[rel_subst]	mb automata 2
Def		(r)'	[rel_addprime]	mb automata 2
Def		rel_subst2(as;r)	[rel_subst2]	mb automata 2
Def		t.name	[rel_name]	mb automata 1
Def		t.fun	[sig_fun]	mb automata 1
Def		term_subst(as;t)	[term_subst]	mb automata 2
Def		term_subst2(as;t)	[term_subst2]	mb automata 2
Def		apply_alist(as;l;d)	[apply_alist]	mb automata 1
Def		tr delivered at p	[deliveries_at]	mb hybrid
Def		< A,evt,tg > (E)	[induced_tagged_event_str]	mb structures
Def		loc(E)	[event_loc]	mb structures
Def		memorylessR(E)	[R_memoryless]	mb hybrid
Def		=msg=(E)	[event_msg_eq]	mb structures
Def		< tr > _tg	[tag_sublist]	mb structures
Def		tag(E)	[event_tag]	mb structures
Def		send-enabledR(E)	[R_send_enabled]	mb hybrid
Def		is-send(E)	[event_is_snd]	mb structures
Def		Trace(E)	[str_trace]	mb structures
Def		safetyR(E)	[R_safety]	mb hybrid
Def		P refines Q	[tr_refines]	mb hybrid
Def		MessageStruct	[message_str]	mb structures
Def		|S|	[carrier]	mb structures
Def		msg(E)	[event_msg]	mb structures
Def		MS(E)	[event_msg_str]	mb structures
Def		t.trace	[trace_env_trace]	mb automata 1
Def		=(M)	[msg_eq]	mb structures
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		(M |= x,x',tr,tr'.R(x;x';tr;tr'))	[tla]	mb state machine
Def		(M -tr- > s)	[reachable_via]	mb state machine
Def		trace_reachable(M;s;l;s')	[trace_reachable]	mb state machine
Def		M.state	[sm_state]	mb state machine
Def		t.ds	[sm_ds]	mb state machine
Def		M.action	[sm_action]	mb state machine
Def		t.da	[sm_da]	mb state machine
Def		t.init	[sm_init]	mb state machine
Def		1of(t)	[pi1]	core
Def		[[rn]] rho e	[relname_mng]	mb automata 2
Def		r.l	[r_select]	mb record
Def		t.typ	[smt_typ]	mb automata 1
Def		[[l]] rho	[st_list_mng]	mb automata 2
Def		[[d]] rho	[dec_mng]	mb automata 2
Def		[[s]] rho	[st_mng]	mb automata 2
Def		value(a)	[value]	mb record
Def		t.rel	[pre_rel]	mb automata 1
Def		Term	[term]	mb automata 1
Def		(d)	[sigma]	mb record
Def		closed_rel(r)	[closed_rel]	mb automata 3
Def		ts()	[ts]	mb automata 1
Def		{d}	[record]	mb record
Def		Decl	[decl]	mb declaration
Def		d o f	[rename_decl]	mb declaration
Def		Label	[lbl]	mb label
Def		P & Q	[and]	core
Def		niltrace()	[niltrace]	mb automata 1
Def			[it]	core
Def		< >	[col_none]	mb collection
Def		mk_sm(da, ds, init, trans)	[mk_sm]	mb state machine
Def		False	[false]	core
Def		vc_concl(v)	[vc_concl]	mb automata 2
Def		rel_mentions_trace(r)	[rel_mentions_trace]	mb automata 3
Def		mentions_trace(t)	[mentions_trace]	mb automata 2
Def		termlist_eq(a;b)	[termlist_eq]	mb automata 2
Def		eq_relname(a;b)	[eq_relname]	mb automata 2
Def		rel_primed_vars(r)	[rel_primed_vars]	mb automata 3
Def		term_primed_vars(t)	[term_primed_vars]	mb automata 2
Def		affects_trace_rel(e;k;r)	[affects_trace_rel]	mb automata 3
Def		affects_trace(e;k;t)	[affects_trace]	mb automata 2
Def		rel_vars(r)	[rel_vars]	mb automata 2
Def		term_vars(t)	[term_vars]	mb automata 1
Def		iterate(statevar x- > v(x) statevar x''- > v'(x') funsymbol op- > opr(op) freevar f- > fvar(f) trace(tr)- > trace(tr) a(b)- > comb(a;b) over t)	[term_iter]	mb automata 2
Def		rel_free_vars(r)	[rel_free_vars]	mb automata 2
Def		term_mentions_guard(g;t)	[term_mentions_guard]	mb automata 2
Def		term_eq(a;b)	[term_eq]	mb automata 2
Def		(a=b)	[ts_eq]	mb automata 1
Def		st_eq(s1;s2)	[st_eq]	mb automata 1
Def		x ls	[lbls_member]	mb label
Def		x:y	[dbase]	mb declaration
Def		l1 = l2	[eq_lbl]	mb basic
Def		unprime(t)	[unprime]	mb automata 2
Def		term_free_vars(t)	[term_free_vars]	mb automata 2
Def		(t)'	[addprime]	mb automata 2
Def		term_iterate(v; p; op; f; tr; a; t)	[term_iterate]	mb automata 1
Def		t_iterate(l;n;t)	[t_iterate]	mb tree
Def		ts_case(x) var(a)= > v(a) var'(b)= > p(b) opr(f)= > op(f) fvar(x)= > f(x) trace(P)= > t(P) end_ts_case	[ts_case]	mb automata 1
Def		ground_ptn(p)	[ground_ptn]	mb basic
Def		Default = > body	[case_default]	prog 1
Def		t.concl	[qimp_concl]	mb automata 2
Def		Case vc_qimp(x) = > body(x) cont	[case_vc_qimp]	mb automata 2
Def		t.concl	[imp_concl]	mb automata 2
Def		t.proj	[trace_env_proj]	mb automata 1
Def		mk_trace_env(trace, proj)	[mk_trace_env]	mb automata 1
Def		Case vc_imp(x) = > body(x) cont	[case_vc_imp]	mb automata 2
Def		Case(value) body	[case]	prog 1
Def		mk_dec(lbl, typ)	[mk_dec]	mb automata 1
Def		mk_qimp(lbl, hyp, concl)	[mk_qimp]	mb automata 2
Def		vc_qimp(x)	[vc_qimp]	mb automata 2
Def		mk_imp(hyp, concl)	[mk_imp]	mb automata 2
Def		vc_imp(x)	[vc_imp]	mb automata 2
Def		false	[bfalse]	bool 1
Def		t.args	[rel_args]	mb automata 1
Def		t.rel	[sig_rel]	mb automata 1
Def		t.typ	[dec_typ]	mb automata 1
Def		t.trans	[sm_trans]	mb state machine
Def		2of(t)	[pi2]	core
Def		pq	[bimplies]	bool 1
Def		p q	[bor]	bool 1
Def		(first x as s.t. P(x) else d)	[find]	mb list 1
Def		filter(P;l)	[filter]	mb list 1
Def		compose_list(L)	[compose_list]	mb list 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		pq	[band]	bool 1
Def		Collection(T)	[col]	mb collection
Def		$x	[clbl]	mb basic
Def		lbl_pr( < x, y > )	[lbl_pair]	mb basic
Def		t	[typ]	mb automata 1
Def		D(i) for i I	[dall]	mb declaration
Def		list_accum(x,a.f(x;a);y;l)	[list_accum]	mb list 1
Def		l1 l2	[iseg]	mb list 1
Def		swap(L;i;j)	[swap]	mb list 2
Def		(L o f)	[permute_list]	mb list 2
Def		mklist(n;f)	[mklist]	mb list 1
Def		as @ bs	[append]	list 1
Def		zip(as;bs)	[zip]	mb list 1
Def		map(f;as)	[map]	list 1
Def		DecidableEquiv	[dequiv]	mb structures
Def		b	[assert]	bool 1
Def		Case x = > body(x) cont	[case_relname_other]	mb automata 1
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		A & B	[cand]	core
Def		Case eq(x) = > body(x) cont	[case_relname_eq]	mb automata 1
Def		x:A. B(x)	[exists]	core
Def		P Q	[or]	core
Def		Case ts_trace(x) = > body(x) cont	[case_ts_trace]	mb automata 1
Def		Case ts_fvar(x) = > body(x) cont	[case_ts_fvar]	mb automata 1
Def		Case ts_op(x) = > body(x) cont	[case_ts_op]	mb automata 1
Def		Case ts_pvar(x) = > body(x) cont	[case_ts_pvar]	mb automata 1
Def		Case ptn_int(x) = > body(x) cont	[case_ptn_int]	mb basic
Def		Case ptn_var(x) = > body(x) cont	[case_ptn_var]	mb basic
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		tl(l)	[tl]	list 1
Def		hd(l)	[hd]	list 1
Def		inr(x) = > body(x) cont	[case_inr]	prog 1
Def		True	[true]	core
Def		Case tree_leaf(x) = > body(x) cont	[case_tree_leaf]	mb tree
Def		Case x;y = > body(x;y) cont	[case_node]	mb tree
Def		Y	[ycomb]	core
Def		if b t else f fi	[ifthenelse]	bool 1
Def		st_lift(rho)	[st_lift]	mb automata 1
Def		t1 t2	[tapp]	mb automata 1
Def		trace(l)	[ttrace]	mb automata 1
Def		l	[tfvar]	mb automata 1
Def		f	[topr]	mb automata 1
Def		l	[tvar]	mb automata 1
Def		l'	[tpvar]	mb automata 1
Def		mk_smt(lbl, term, typ)	[mk_smt]	mb automata 1
Def		imax(a;b)	[imax]	int 2
Def		ij	[le_int]	bool 1
Def		b	[bnot]	bool 1
Def		true	[btrue]	bool 1
Def		Prop	[prop]	core
Def		Case lbl : typ = > body(lbl;typ)	[case_mk_dec]	mb automata 1
Def		mk_rel(name, args)	[mk_rel]	mb automata 1
Def		x f y	[infix_ap]	core
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		inl(x) = > body(x) cont	[case_inl]	prog 1
Def		Case ts_var(x) = > body(x) cont	[case_ts_var]	mb automata 1
Def		Tree(E)	[tree]	mb tree
Def		ts_var(x)	[ts_var]	mb automata 1
Def		tree_leaf(x)	[tree_leaf]	mb tree
Def		ts_fvar(x)	[ts_fvar]	mb automata 1
Def		ts_trace(x)	[ts_trace]	mb automata 1
Def		ts_pvar(x)	[ts_pvar]	mb automata 1
Def		ts_op(x)	[ts_op]	mb automata 1
Def		tree_node( < x, y > )	[node]	mb tree
Def		Unit	[unit]	core
Def		mk_ioa(ds, da, init, pre, eff, frame)	[mk_ioa]	mb automata 1
Def			[bool]	bool 1
Def		Top	[top]	core
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		(i, j)	[flip]	mb nat
Def		sum(f(x;y) | x < n; y < m)	[double_sum]	mb nat
Def		sum(f(x) | x < k)	[sum]	mb nat
Def		primrec(n;b;c)	[primrec]	mb nat
Def		R^n	[rel_exp]	mb nat
Def		Case v = > case cont	[switch_case]	prog 1
Def		i=j	[eq_int]	bool 1
Def		InvFuns(A; B; f; g)	[inv_funs]	fun 1
Def		f o g	[compose]	fun 1
Def		decl_type(d;x)	[decl_type]	mb declaration
Def		Pattern	[ptn]	mb basic
Def		firstn(n;as)	[firstn]	list 1
Def		i < j	[lt_int]	bool 1
Def		GCD(a;b;y)	[gcd_p]	num thy 1
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def		ptn_con(T)	[ptn_con]	mb basic
Def		Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def		Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def		x=yAtom	[eq_atom]	bool 1
Def		ptn_atom(x)	[ptn_atom]	mb basic
Def		ptn_pr(x)	[ptn_pr]	mb basic
Def		Order(T;x,y.R(x;y))	[order]	rel 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		P Q	[iff]	core
Def		AntiSym(T;x,y.R(x;y))	[anti_sym]	rel 1
Def		Connex(T;x,y.R(x;y))	[connex]	rel 1
Def		tree_con(E;T)	[tree_con]	mb tree
Def		tree_node(x)	[tree_node]	mb tree
Def		< < "a", b > , c, 1 >	[pattern1]	prog 1
Def		EndSwitch	[switch_done]	prog 1
Def		enum1_el3	[enum1_el3]	prog 1
Def		enum1_el2	[enum1_el2]	prog 1
Def		enum1_el1	[enum1_el1]	prog 1
Def		Switch(t) b	[switch]	prog 1
Def		{T}	[guard]	core
Def		x:T. b(x)	[tlambda]	fun 1
Def		mapcons(f;as)	[mapcons]	list 1
Def		S T	[subtype]	core
Def		Id	[tidentity]	fun 1
Def		Id	[identity]	fun 1
Def		Surj(A; B; f)	[surject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		P Q	[rev_implies]	core
Def		T	[squash]	core

About: