Def		rel_arg_typ(rn;i;de)	[rel_arg_typ]	mb automata 1
Def		[[A]] rho de e	[ioa_mng]
Def		wp_rel(A;a;r)	[wp_rel]
Def		wp2_rel(A;a;r)	[wp2_rel]	mb automata 3
Def		wp2(A;a;Q)	[wp2]	mb automata 3
Def		tc_ioa(A;de)	[tc_ioa]
Def		covers_rel(A;r)	[covers_rel]	mb automata 2
Def		wp(A;a;Q)	[wp]
Def		trace_consistent_vc(rho;da;R;v)	[trace_consistent_vc]
Def		covers_pred(A;p)	[covers_pred]	mb automata 3
Def		tc_vcs{i}(vs;ds;da;de)	[tc_vcs]
Def		VCs(A;I)	[ioa_inv_vc]
Def		tc_vc(v;ds;da;de)	[tc_vc]
Def		tc_pred(P;ds;da;de)	[tc_pred]
Def		tc(r;ds;da;de)	[tc]	mb automata 3
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		ioa_trans_all{i}(A;I)	[ioa_trans_all]
Def		ioa_trans(A;a;I)	[ioa_trans]
Def		smts_eff_pred(ss;p)	[smts_eff_pred]
Def		smts_eff_rel(ss;r)	[smts_eff_rel]	mb automata 3
Def		trace_consistent_pred(rho;da;R;p)	[trace_consistent_pred]
Def		trace_consistent_rel(rho;da;R;r)	[trace_consistent_rel]	mb automata 3
Def		col_subst2(c;r)	[col_subst2]	mb automata 3
Def		col_subst(c;r)	[col_subst]	mb automata 3
Def		col_list_prod(l)	[col_list_prod]	mb collection
Def		l[i]	[select]	list 1
Def		pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr)	[pred_mng_2]	mb automata 3
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		rel_subst(as;r)	[rel_subst]	mb automata 2
Def		rel_subst2(as;r)	[rel_subst2]	mb automata 2
Def		(P)'	[pred_addprime]	mb automata 3
Def		pred_unprime(P)	[pred_unprime]	mb automata 3
Def		rel_unprime(r)	[rel_unprime]	mb automata 2
Def		rel_eq(a;b)	[rel_eq]	mb automata 3
Def		[[vs]] rho ds da de e s tr	[vcs_mng]
Def		vc_mng(v;rho;ds;da;de;e;s;tr)	[vc_mng]
Def		[[p]] rho ds da de e s a tr	[pred_mng]	mb automata 3
Def		[[r]] rho ds da de e s a tr	[rel_mng]	mb automata 3
Def		(r)'	[rel_addprime]	mb automata 2
Def		t.name	[rel_name]	mb automata 1
Def		closed_pred(p)	[closed_pred]	mb automata 3
Def		closed_rel(r)	[closed_rel]	mb automata 3
Def		rel_primed_vars(r)	[rel_primed_vars]	mb automata 3
Def		ioa_mentions_trace(A)	[ioa_mentions_trace]	mb automata 3
Def		guarded_trace(da;e;I)	[guarded_trace]	mb automata 3
Def		rel_free_vars(r)	[rel_free_vars]	mb automata 2
Def		rel_mentions_trace(r)	[rel_mentions_trace]	mb automata 3
Def		affects_trace_rel(e;k;r)	[affects_trace_rel]	mb automata 3
Def		rel_vars(r)	[rel_vars]	mb automata 2
Def		t.args	[rel_args]	mb automata 1
Def		||as||	[length]	list 1
Def		trace_env(d)	[trace_env]	mb automata 1
Def		[[s]] rho	[sig_mng]	mb automata 3
Def		{p}	[record_pair]	mb record
Def		(M |= always s,t.P(s;t))	[trace_inv]	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		sm{i:l}()	[sm]	mb state machine
Def		{d}	[record]	mb record
Def		Decl	[decl]	mb declaration
Def		sig()	[sig]	mb automata 2
Def		VCs	[vcs]	mb automata 2
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		ioa{i:l}()	[ioa]	mb automata 3
Def		Collection(T)	[col]	mb collection
Def			[nat]	int 1
Def		subst_mentions_trace(as)	[subst_mentions_trace]	mb automata 3
Def		r	[pred_rel]	mb automata 1
Def		smts_eff(ss;x)	[smts_eff]	mb automata 2
Def		action_effect(a;es;fs)	[action_effect]	mb automata 2
Def		eff()	[eff]	mb automata 2
Def		smt_terms(c)	[smt_terms]	mb automata 2
Def		smt()	[smt]	mb automata 2
Def		action_pre(a;ps)	[action_pre]	mb automata 2
Def		pre()	[pre]	mb automata 3
Def		col_map_subst(x.f(x);c)	[col_map_subst]	mb automata 2
Def		rel()	[rel]	mb automata 2
Def		Term	[term]	mb automata 1
Def		relname()	[relname]	mb automata 2
Def		M.action	[sm_action]	mb state machine
Def		trace_consistent(rho;da;R;t)	[trace_consistent]	mb automata 3
Def		(d)	[sigma]	mb record
Def		tc_eff(ef;ds;de)	[tc_eff]
Def		tc_smt(s;ds;da;de)	[tc_smt]	mb automata 3
Def		term_types(ds;da;de;t)	[term_types]	mb automata 3
Def		single_valued_decls(c)	[single_valued_decls]	mb automata 2
Def		frame()	[frame]	mb automata 2
Def		dec_lookup(ds;x)	[dec_lookup]	mb automata 2
Def		[[ds]] rho	[decls_mng]	mb automata 3
Def		[[sts]] rho	[sts_mng]	mb automata 2
Def		dec()	[dec]	mb automata 2
Def		st_app(c1;c2)	[st_app]	mb automata 2
Def		st_app1(s1;s2)	[st_app1]	mb automata 2
Def		SimpleType	[st]	mb automata 1
Def		ts()	[ts]	mb automata 1
Def		Label	[lbl]	mb label
Def		b	[assert]	bool 1
Def			[bool]	bool 1
Def		Prop	[prop]	core
Def		c1 = c2	[col_equal]	mb collection
Def		P Q	[iff]	core
Def		[[l]] rho	[st_list_mng]	mb automata 2
Def		[[rn]] rho e	[relname_mng]	mb automata 2
Def		[[d]] rho	[dec_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		c1 c2	[col_le]	mb collection
Def		ioa_all(I; i.A(i))	[ioa_all]	mb automata 1
Def		term_subst(as;t)	[term_subst]	mb automata 2
Def		term_subst2(as;t)	[term_subst2]	mb automata 2
Def		unprime(t)	[unprime]	mb automata 2
Def		l	[tvar]	mb automata 1
Def		apply_alist(as;l;d)	[apply_alist]	mb automata 1
Def		A & B	[cand]	core
Def		t.trans	[sm_trans]	mb state machine
Def		t.init	[sm_init]	mb state machine
Def		t.typ	[eff_typ]	mb automata 1
Def		t.smt	[eff_smt]	mb automata 1
Def		t.typ	[frame_typ]	mb automata 1
Def		t.acts	[frame_acts]	mb automata 1
Def		t.frame	[ioa_frame]	mb automata 1
Def		t.term	[smt_term]	mb automata 1
Def		[[t]] e s a tr	[term_mng]	mb automata 1
Def		t.typ	[smt_typ]	mb automata 1
Def		t.eff	[ioa_eff]	mb automata 1
Def		value(a)	[value]	mb record
Def		t.rel	[pre_rel]	mb automata 1
Def		t.pre	[ioa_pre]	mb automata 1
Def		t.init	[ioa_init]	mb automata 1
Def		t.da	[ioa_da]	mb automata 1
Def		tappend(tr;a)	[tappend]	mb automata 1
Def		vc_concl(v)	[vc_concl]	mb automata 2
Def		t.concl	[qimp_concl]	mb automata 2
Def		vc_hyp(v)	[vc_hyp]	mb automata 2
Def		t.hyp	[qimp_hyp]	mb automata 2
Def		t.concl	[imp_concl]	mb automata 2
Def		tre.P	[tproj]	mb automata 1
Def		t.proj	[trace_env_proj]	mb automata 1
Def		t.rel	[sig_rel]	mb automata 1
Def		t.ds	[sm_ds]	mb state machine
Def		t.typ	[dec_typ]	mb automata 1
Def		2of(t)	[pi2]	core
Def		x:A. B(x)	[exists]	core
Def		t.trace	[trace_env_trace]	mb automata 1
Def		let x = a in b(x)	[let]	core
Def		(xc.f(x))	[col_accum]	mb collection
Def		(xc.P(x))	[col_all]	mb collection
Def		P Q	[pred_and]	mb automata 1
Def		< f(x) | x c >	[col_map]	mb collection
Def		a +* b	[vcs_add]	mb automata 2
Def		i:I. C(i)	[col_union]	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		P Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		< x >	[col_singleton]	mb collection
Def		t.var	[frame_var]	mb automata 1
Def		{i..j}	[int_seg]	int 1
Def		i j < k	[lelt]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		t.lbl	[smt_lbl]	mb automata 1
Def		t.kind	[eff_kind]	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.ds	[ioa_ds]	mb automata 1
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		t.fun	[sig_fun]	mb automata 1
Def		t.da	[sm_da]	mb state machine
Def		1of(t)	[pi1]	core
Def		r.l	[r_select]	mb record
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		mentions_trace(t)	[mentions_trace]	mb automata 2
Def		term_primed_vars(t)	[term_primed_vars]	mb automata 2
Def		term_vars(t)	[term_vars]	mb automata 1
Def		affects_trace(e;k;t)	[affects_trace]	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		termlist_eq(a;b)	[termlist_eq]	mb automata 2
Def		eq_relname(a;b)	[eq_relname]	mb automata 2
Def		x ls	[lbls_member]	mb label
Def		term_eq(a;b)	[term_eq]	mb automata 2
Def		st_eq(s1;s2)	[st_eq]	mb automata 1
Def		term_mentions_guard(g;t)	[term_mentions_guard]	mb automata 2
Def		(a=b)	[ts_eq]	mb automata 1
Def		l1 = l2	[eq_lbl]	mb basic
Def		(t)'	[addprime]	mb automata 2
Def		term_free_vars(t)	[term_free_vars]	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		ground_ptn(p)	[ground_ptn]	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		Default = > body	[case_default]	prog 1
Def		Case vc_qimp(x) = > body(x) cont	[case_vc_qimp]	mb automata 2
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		nth_tl(n;as)	[nth_tl]	list 1
Def		Case x = > body(x) cont	[case_relname_other]	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		Case eq(x) = > body(x) cont	[case_relname_eq]	mb automata 1
Def		decl_type(d;x)	[decl_type]	mb declaration
Def		map(f;as)	[map]	list 1
Def		mk_rel(name, args)	[mk_rel]	mb automata 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		reduce(f;k;as)	[reduce]	list 1
Def		Tree(E)	[tree]	mb tree
Def		list_accum(x,a.f(x;a);y;l)	[list_accum]	mb list 1
Def		P Q	[rev_implies]	core
Def		mk_ioa(ds, da, init, pre, eff, frame)	[mk_ioa]	mb automata 1
Def		ts_var(x)	[ts_var]	mb automata 1
Def		t	[typ]	mb automata 1
Def		trace(l)	[ttrace]	mb automata 1
Def		l	[tfvar]	mb automata 1
Def		f	[topr]	mb automata 1
Def		l'	[tpvar]	mb automata 1
Def		tree_leaf(x)	[tree_leaf]	mb tree
Def		$x	[clbl]	mb basic
Def		lbl_pr( < x, y > )	[lbl_pair]	mb basic
Def		as @ bs	[append]	list 1
Def		pq	[band]	bool 1
Def		Pattern	[ptn]	mb basic
Def		D(i) for i I	[dall]	mb declaration
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		t1 t2	[tapp]	mb automata 1
Def		tree_con(E;T)	[tree_con]	mb tree
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		ptn_atom(x)	[ptn_atom]	mb basic
Def		ptn_pr(x)	[ptn_pr]	mb basic
Def		zip(as;bs)	[zip]	mb list 1
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		Case lbl : typ = > body(lbl;typ)	[case_mk_dec]	mb automata 1
Def		i < j	[lt_int]	bool 1
Def		tree_node( < x, y > )	[node]	mb tree
Def		ts_trace(x)	[ts_trace]	mb automata 1
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		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_node(x)	[tree_node]	mb tree

About: