Def	pred_unprime(P)	[pred_unprime]
Def	tc_smt(s;ds;da;de)	[tc_smt]
Def	guarded_trace(da;e;I)	[guarded_trace]
Def	[[p]] rho ds da de e s a tr	[pred_mng]
Def	smts_eff_rel(ss;r)	[smts_eff_rel]
Def	pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr)	[pred_mng_2]
Def	wp2(A;a;Q)	[wp2]
Def	wp2_rel(A;a;r)	[wp2_rel]
Def	rel_eq(a;b)	[rel_eq]
Def	c1 = c2	[col_equal]	mb collection
Def	P Q	[iff]	core
Def	subst_mentions_trace(as)	[subst_mentions_trace]
Def	col_subst(c;r)	[col_subst]
Def	rel_subst(as;r)	[rel_subst]	mb automata 2
Def	term_subst(as;t)	[term_subst]	mb automata 2
Def	covers_rel(A;r)	[covers_rel]	mb automata 2
Def	covers_pred(A;p)	[covers_pred]
Def	covers_var(A;x)	[covers_var]	mb automata 2
Def	pred_mentions(p;x)	[pred_mentions]	mb automata 2
Def	rel_mentions(r;x)	[rel_mentions]	mb automata 2
Def	(x l)	[l_member]	mb list 1
Def	tc(r;ds;da;de)	[tc]
Def	trace_consistent_rel(rho;da;R;r)	[trace_consistent_rel]
Def	col_subst2(c;r)	[col_subst2]
Def	col_list_prod(l)	[col_list_prod]	mb collection
Def		[nat]	int 1
Def	{i..j}	[int_seg]	int 1
Def	i j < k	[lelt]	int 1
Def	AB	[le]	core
Def	A	[not]	core
Def	rel_subst2(as;r)	[rel_subst2]	mb automata 2
Def	term_subst2(as;t)	[term_subst2]	mb automata 2
Def	ioa{i:l}()	[ioa]
Def	(P)'	[pred_addprime]
Def	(r)'	[rel_addprime]	mb automata 2
Def	(t)'	[addprime]	mb automata 2
Def	[[sts]] rho	[sts_mng]	mb automata 2
Def	[[s]] rho	[sig_mng]
Def	[[l]] rho	[st_list_mng]	mb automata 2
Def	trace_consistent(rho;da;R;t)	[trace_consistent]
Def	[[ds]] rho	[decls_mng]
Def	[[d]] rho	[dec_mng]	mb automata 2
Def	[[r]] rho ds da de e s a tr	[rel_mng]
Def	rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)	[rel_mng_2]
Def	[[rn]] rho e	[relname_mng]	mb automata 2
Def	[[s]] rho	[st_mng]	mb automata 2
Def	st_lift(rho)	[st_lift]	mb automata 1
Def	x:y	[dbase]	mb declaration
Def	Top	[top]	core
Def	rel_unprime(r)	[rel_unprime]	mb automata 2
Def	unprime(t)	[unprime]	mb automata 2
Def	action_effect(a;es;fs)	[action_effect]	mb automata 2
Def	l	[tvar]	mb automata 1
Def	apply_alist(as;l;d)	[apply_alist]	mb automata 1
Def	sig()	[sig]	mb automata 2
Def	c1 c2	[col_le]	mb collection
Def	closed_term(t)	[closed_term]	mb automata 2
Def	rel_vars(r)	[rel_vars]	mb automata 2
Def	term_vars(t)	[term_vars]	mb automata 1
Def	term_types(ds;da;de;t)	[term_types]
Def	st_app(c1;c2)	[st_app]	mb automata 2
Def	st_app1(s1;s2)	[st_app1]	mb automata 2
Def	< >	[col_none]	mb collection
Def	Decl	[decl]	mb declaration
Def	{d}	[record]	mb record
Def	dec_lookup(ds;x)	[dec_lookup]	mb automata 2
Def	t.typ	[dec_typ]	mb automata 1
Def	niltrace()	[niltrace]	mb automata 1
Def	tappend(tr;a)	[tappend]	mb automata 1
Def	mk_trace_env(trace, proj)	[mk_trace_env]	mb automata 1
Def		[bool]	bool 1
Def	[[t]] e s a tr	[term_mng]	mb automata 1
Def	[[t]] e s s' a tr	[term_mng2]	mb automata 2
Def	tre.P	[tproj]	mb automata 1
Def	t.proj	[trace_env_proj]	mb automata 1
Def	trace_env(d)	[trace_env]	mb automata 1
Def	value(a)	[value]	mb record
Def	r.l	[r_select]	mb record
Def	Fmla	[pred]	mb automata 1
Def	unzip(as)	[unzip]	mb list 1
Def	Prop	[prop]	core
Def	trace(l)	[ttrace]	mb automata 1
Def	closed_pred(p)	[closed_pred]
Def	ioa_mentions_trace(A)	[ioa_mentions_trace]
Def	false	[bfalse]	bool 1
Def	closed_rel(r)	[closed_rel]
Def	rel_free_vars(r)	[rel_free_vars]	mb automata 2
Def	rel_primed_vars(r)	[rel_primed_vars]
Def	affects_trace_rel(e;k;r)	[affects_trace_rel]
Def	rel_mentions_trace(r)	[rel_mentions_trace]
Def	t.args	[rel_args]	mb automata 1
Def	t.rel	[sig_rel]	mb automata 1
Def	smts_eff(ss;x)	[smts_eff]	mb automata 2
Def	smt_terms(c)	[smt_terms]	mb automata 2
Def	t.term	[smt_term]	mb automata 1
Def	t.typ	[smt_typ]	mb automata 1
Def	t.init	[ioa_init]	mb automata 1
Def	t.rel	[pre_rel]	mb automata 1
Def	t.pre	[ioa_pre]	mb automata 1
Def	t.smt	[eff_smt]	mb automata 1
Def	t.eff	[ioa_eff]	mb automata 1
Def	t.frame	[ioa_frame]	mb automata 1
Def	t.acts	[frame_acts]	mb automata 1
Def	t.typ	[frame_typ]	mb automata 1
Def	2of(t)	[pi2]	core
Def	mentions_trace(t)	[mentions_trace]	mb automata 2
Def	affects_trace(e;k;t)	[affects_trace]	mb automata 2
Def	term_mentions_guard(g;t)	[term_mentions_guard]	mb automata 2
Def	x ls	[lbls_member]	mb label
Def	p q	[bor]	bool 1
Def	(first x as s.t. P(x) else d)	[find]	mb list 1
Def	tr | P	[trace_projection]	mb events
Def	filter(P;l)	[filter]	mb list 1
Def	reduce(f;k;as)	[reduce]	list 1
Def	termlist_eq(a;b)	[termlist_eq]	mb automata 2
Def	t.name	[rel_name]	mb automata 1
Def	eq_relname(a;b)	[eq_relname]	mb automata 2
Def	pre()	[pre]
Def	col_map_subst(x.f(x);c)	[col_map_subst]	mb automata 2
Def	rel()	[rel]	mb automata 2
Def	frame()	[frame]	mb automata 2
Def	eff()	[eff]	mb automata 2
Def	dec()	[dec]	mb automata 2
Def	relname()	[relname]	mb automata 2
Def	smt()	[smt]	mb automata 2
Def	SimpleType	[st]	mb automata 1
Def	Term	[term]	mb automata 1
Def	(d)	[sigma]	mb record
Def	ts()	[ts]	mb automata 1
Def	Label	[lbl]	mb label
Def	term_eq(a;b)	[term_eq]	mb automata 2
Def	st_eq(s1;s2)	[st_eq]	mb automata 1
Def	(a=b)	[ts_eq]	mb automata 1
Def	l1 = l2	[eq_lbl]	mb basic
Def	ground_ptn(p)	[ground_ptn]	mb basic
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	t.fun	[sig_fun]	mb automata 1
Def	< x >	[col_singleton]	mb collection
Def	term_primed_vars(t)	[term_primed_vars]	mb automata 2
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	< f(x) | x c >	[col_map]	mb collection
Def	(xc.f(x))	[col_accum]	mb collection
Def	< x c | P(x) >	[col_filter]	mb collection
Def	a + b	[col_add]	mb collection
Def	x c	[col_member]	mb collection
Def	D(i) for i I	[dall]	mb declaration
Def	kind(a)	[kind]	mb record
Def	t.lbl	[smt_lbl]	mb automata 1
Def	t.lbl	[dec_lbl]	mb automata 1
Def	t.trace	[trace_env_trace]	mb automata 1
Def	t.kind	[eff_kind]	mb automata 1
Def	t.var	[frame_var]	mb automata 1
Def	1of(t)	[pi1]	core
Def	list_accum(x,a.f(x;a);y;l)	[list_accum]	mb list 1
Def	term_free_vars(t)	[term_free_vars]	mb automata 2
Def	as @ bs	[append]	list 1
Def	P Q	[implies]	core
Def	x:A. B(x)	[all]	core
Def	zip(as;bs)	[zip]	mb list 1
Def	map(f;as)	[map]	list 1
Def	b	[assert]	bool 1
Def	False	[false]	core
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	Default = > body	[case_default]	prog 1
Def	Case x = > body(x) cont	[case_relname_other]	mb automata 1
Def	l[i]	[select]	list 1
Def	P & Q	[and]	core
Def	||as||	[length]	list 1
Def	A & B	[cand]	core
Def	Case eq(x) = > body(x) cont	[case_relname_eq]	mb automata 1
Def	Case(value) body	[case]	prog 1
Def	mk_dec(lbl, typ)	[mk_dec]	mb automata 1
Def	x:A. B(x)	[exists]	core
Def	P Q	[or]	core
Def	P Q	[rev_implies]	core
Def	t1 t2	[tapp]	mb automata 1
Def	l	[tfvar]	mb automata 1
Def	f	[topr]	mb automata 1
Def	l'	[tpvar]	mb automata 1
Def	ts_var(x)	[ts_var]	mb automata 1
Def	tree_leaf(x)	[tree_leaf]	mb tree
Def	decl_type(d;x)	[decl_type]	mb declaration
Def	ts_trace(x)	[ts_trace]	mb automata 1
Def	Pattern	[ptn]	mb basic
Def	ptn_atom(x)	[ptn_atom]	mb basic
Def	ptn_pr(x)	[ptn_pr]	mb basic
Def	Tree(E)	[tree]	mb tree
Def	Case lbl : typ = > body(lbl;typ)	[case_mk_dec]	mb automata 1
Def	mk_rel(name, args)	[mk_rel]	mb automata 1
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	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	hd(l)	[hd]	list 1
Def	nth_tl(n;as)	[nth_tl]	list 1
Def	tl(l)	[tl]	list 1
Def	inr(x) = > body(x) cont	[case_inr]	prog 1
Def	mk_smt(lbl, term, typ)	[mk_smt]	mb automata 1
Def	ij	[le_int]	bool 1
Def	b	[bnot]	bool 1
Def	tree_node( < x, y > )	[node]	mb tree
Def	ts_fvar(x)	[ts_fvar]	mb automata 1
Def	ts_op(x)	[ts_op]	mb automata 1
Def	ts_pvar(x)	[ts_pvar]	mb automata 1
Def	Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def	x=yAtom	[eq_atom]	bool 1
Def	i=j	[eq_int]	bool 1
Def	Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
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	ptn_con(T)	[ptn_con]	mb basic
Def	tree_con(E;T)	[tree_con]	mb tree
Def	tree_node(x)	[tree_node]	mb tree
Def	Case ts_var(x) = > body(x) cont	[case_ts_var]	mb automata 1
Def	inl(x) = > body(x) cont	[case_inl]	prog 1
Def	i < j	[lt_int]	bool 1

About: