Def		action_pre(a;ps)	[action_pre]
Def		mk_imp(hyp, concl)	[mk_imp]
Def		t.lbl	[qimp_lbl]
Def		mk_qimp(lbl, hyp, concl)	[mk_qimp]
Def		vc_imp(x)	[vc_imp]
Def		vc_qimp(x)	[vc_qimp]
Def		vc_hyp(v)	[vc_hyp]
Def		vc_concl(v)	[vc_concl]
Def		VCs	[vcs]
Def		< *v* >	[vcs_singleton]
Def		a +* b	[vcs_add]
Def		single_valued_decls(c)	[single_valued_decls]
Def		col_map_subst(x.f(x);c)	[col_map_subst]
Def		action_effect(a;es;fs)	[action_effect]
Def		[[l]] rho	[st_list_mng]
Def		[[d]] rho	[dec_mng]
Def		[[rn]] rho e	[relname_mng]
Def		rel_unprime(r)	[rel_unprime]
Def		pred_mentions(p;x)	[pred_mentions]
Def		covers_rel(A;r)	[covers_rel]
Def		smts_eff(ss;x)	[smts_eff]
Def			[bool]	bool 1
Def		c1 = c2	[col_equal]	mb collection
Def		P Q	[iff]	core
Def		ab	[arrow]	mb automata 1
Def		sig()	[sig]
Def		SQType(T)	[sq_type]	sqequal 1
Def		eq_relname(a;b)	[eq_relname]
Def		dec_lookup(ds;x)	[dec_lookup]
Def		c1 c2	[col_le]	mb collection
Def		[[t]] e s a tr	[term_mng]	mb automata 1
Def		[[sts]] rho	[sts_mng]
Def		[[s]] rho	[st_mng]
Def		st_lift(rho)	[st_lift]	mb automata 1
Def		x:y	[dbase]	mb declaration
Def		Top	[top]	core
Def		[[t]] e s s' a tr	[term_mng2]
Def		unzip(as)	[unzip]	mb list 1
Def		termlist_eq(a;b)	[termlist_eq]
Def		mentions_trace(t)	[mentions_trace]
Def		term_mentions_guard(g;t)	[term_mentions_guard]
Def		tc1(r;de)	[tc1]	mb automata 1
Def		rel_mentions(r;x)	[rel_mentions]
Def		covers_var(A;x)	[covers_var]
Def		(x l)	[l_member]	mb list 1
Def			[nat]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		st_app(c1;c2)	[st_app]
Def		tappend(tr;a)	[tappend]	mb automata 1
Def		tre.P	[tproj]	mb automata 1
Def		tr | P	[trace_projection]	mb events
Def		kind(a)	[kind]	mb record
Def		t.proj	[trace_env_proj]	mb automata 1
Def		affects_trace(e;k;t)	[affects_trace]
Def		trace_env(d)	[trace_env]	mb automata 1
Def		(d)	[sigma]	mb record
Def		Decl	[decl]	mb declaration
Def		rel_vars(r)	[rel_vars]
Def		term_primed_vars(t)	[term_primed_vars]
Def		closed_term(t)	[closed_term]
Def		(r)'	[rel_addprime]
Def		rel_free_vars(r)	[rel_free_vars]
Def		rel_subst(as;r)	[rel_subst]
Def		rel_subst2(as;r)	[rel_subst2]
Def		t.eff	[ioa_eff]	mb automata 1
Def		t.smt	[eff_smt]	mb automata 1
Def		t.lbl	[smt_lbl]	mb automata 1
Def		t.kind	[eff_kind]	mb automata 1
Def		eff()	[eff]
Def		t.acts	[frame_acts]	mb automata 1
Def		P Q	[implies]	core
Def		frame()	[frame]
Def		vc{i:l}()	[vc]
Def		qimp{i:l}()	[qimp]
Def		imp{i:l}()	[imp]
Def		Fmla	[pred]	mb automata 1
Def		rel()	[rel]
Def		dec()	[dec]
Def		smt_terms(c)	[smt_terms]
Def		smt()	[smt]
Def		st_app1(s1;s2)	[st_app1]
Def		relname()	[relname]
Def		SimpleType	[st]	mb automata 1
Def		Term	[term]	mb automata 1
Def		ts()	[ts]	mb automata 1
Def		Label	[lbl]	mb label
Def		x:A. B(x)	[all]	core
Def		t.frame	[ioa_frame]	mb automata 1
Def		t.var	[frame_var]	mb automata 1
Def		term_eq(a;b)	[term_eq]
Def		(a=b)	[ts_eq]	mb automata 1
Def		st_eq(s1;s2)	[st_eq]	mb automata 1
Def		term_subst(as;t)	[term_subst]
Def		term_subst2(as;t)	[term_subst2]
Def		apply_alist(as;l;d)	[apply_alist]	mb automata 1
Def		x ls	[lbls_member]	mb label
Def		l1 = l2	[eq_lbl]	mb basic
Def		b	[assert]	bool 1
Def		< x c | P(x) >	[col_filter]	mb collection
Def		< f(x) | x c >	[col_map]	mb collection
Def		a + b	[col_add]	mb collection
Def		(xc.f(x))	[col_accum]	mb collection
Def		x c	[col_member]	mb collection
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		t.rel	[pre_rel]	mb automata 1
Def		t.kind	[pre_kind]	mb automata 1
Def		t.hyp	[qimp_hyp]
Def		t.hyp	[imp_hyp]
Def		t.lbl	[dec_lbl]	mb automata 1
Def		t.term	[smt_term]	mb automata 1
Def		t.typ	[frame_typ]	mb automata 1
Def		t.name	[rel_name]	mb automata 1
Def		t.trace	[trace_env_trace]	mb automata 1
Def		1of(t)	[pi1]	core
Def		t.concl	[qimp_concl]
Def		t.concl	[imp_concl]
Def		t.typ	[dec_typ]	mb automata 1
Def		t.args	[rel_args]	mb automata 1
Def		t.rel	[sig_rel]	mb automata 1
Def		2of(t)	[pi2]	core
Def		Case vc_qimp(x) = > body(x) cont	[case_vc_qimp]
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]
Def		unprime(t)	[unprime]
Def		term_free_vars(t)	[term_free_vars]
Def		(t)'	[addprime]
Def		term_iterate(v; p; op; f; tr; a; t)	[term_iterate]	mb automata 1
Def		Case x = > body(x) cont	[case_relname_other]	mb automata 1
Def		l[i]	[select]	list 1
Def		ground_ptn(p)	[ground_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		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		nth_tl(n;as)	[nth_tl]	list 1
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		tl(l)	[tl]	list 1
Def		hd(l)	[hd]	list 1
Def		inr(x) = > body(x) cont	[case_inr]	prog 1
Def		False	[false]	core
Def		t_iterate(l;n;t)	[t_iterate]	mb tree
Def		Default = > body	[case_default]	prog 1
Def		Case vc_imp(x) = > body(x) cont	[case_vc_imp]
Def		Case(value) body	[case]	prog 1
Def		Collection(T)	[col]	mb collection
Def		< x >	[col_singleton]	mb collection
Def		r.l	[r_select]	mb record
Def		p q	[bor]	bool 1
Def		false	[bfalse]	bool 1
Def		True	[true]	core
Def		Case tree_leaf(x) = > body(x) cont	[case_tree_leaf]	mb tree
Def		pq	[band]	bool 1
Def		Case x;y = > body(x;y) cont	[case_node]	mb tree
Def		Y	[ycomb]	core
Def		< >	[col_none]	mb collection
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Case eq(x) = > body(x) cont	[case_relname_eq]	mb automata 1
Def		mk_dec(lbl, typ)	[mk_dec]	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		as @ bs	[append]	list 1
Def		(first x as s.t. P(x) else d)	[find]	mb list 1
Def		filter(P;l)	[filter]	mb list 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		||as||	[length]	list 1
Def		A & B	[cand]	core
Def		mk_smt(lbl, term, typ)	[mk_smt]	mb automata 1
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		map(f;as)	[map]	list 1
Def		mk_rel(name, args)	[mk_rel]	mb automata 1
Def		P Q	[rev_implies]	core
Def		tree_node( < x, y > )	[node]	mb tree
Def		mk_trace_env(trace, proj)	[mk_trace_env]	mb automata 1
Def		decl_type(d;x)	[decl_type]	mb declaration
Def		Pattern	[ptn]	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		i=j	[eq_int]	bool 1
Def		Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def		Tree(E)	[tree]	mb tree
Def		ts_trace(x)	[ts_trace]	mb automata 1
Def		tree_leaf(x)	[tree_leaf]	mb tree
Def		ts_fvar(x)	[ts_fvar]	mb automata 1
Def		ts_op(x)	[ts_op]	mb automata 1
Def		ts_var(x)	[ts_var]	mb automata 1
Def		ts_pvar(x)	[ts_pvar]	mb automata 1
Def		tree_node(x)	[tree_node]	mb tree
Def		ptn_con(T)	[ptn_con]	mb basic
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_con(E;T)	[tree_con]	mb tree
Def		i < j	[lt_int]	bool 1

About: