Def	sm{i:l}()	[sm]
Def	(f o M)	[sm_a_rename]
Def	(M |= always s,t.P(s;t))	[trace_inv]
Def	(M |= initially x,tr.P(x;tr))	[initially]
Def	(M |= x,tr.P(x;tr) while Q(x;tr))	[while]
Def	(M |= x,x',tr,tr'.R(x;x';tr;tr'))	[tla]
Def	(M -tr- > s)	[reachable_via]
Def	trace_reachable(M;s;l;s')	[trace_reachable]
Def	M.state	[sm_state]
Def	{d}	[record]	mb record
Def	M.action	[sm_action]
Def	(d)	[sigma]	mb record
Def	Decl	[decl]	mb declaration
Def	d o f	[rename_decl]	mb declaration
Def	Label	[lbl]	mb label
Def	Pattern	[ptn]	mb basic
Def	i:I M(i)	[sm_all]
Def	P Q	[iff]	core
Def	True	[true]	core
Def	t.ds	[sm_ds]
Def	t.da	[sm_da]
Def	Prop	[prop]	core
Def	t.init	[sm_init]
Def	kind(a)	[kind]	mb record
Def	1of(t)	[pi1]	core
Def	t.trans	[sm_trans]
Def	value(a)	[value]	mb record
Def	2of(t)	[pi2]	core
Def	x:A. B(x)	[all]	core
Def	D(i) for i I	[dall]	mb declaration
Def	mk_sm(da, ds, init, trans)	[mk_sm]
Def	A & B	[cand]	core
Def	x:A. B(x)	[exists]	core
Def	P & Q	[and]	core
Def	Y	[ycomb]	core
Def	P Q	[implies]	core
Def	as @ bs	[append]	list 1
Def	ptn_con(T)	[ptn_con]	mb basic
Def	P Q	[rev_implies]	core
Def	decl_type(d;x)	[decl_type]	mb declaration
Def	ground_ptn(p)	[ground_ptn]	mb basic
Def	b	[assert]	bool 1
Def	Top	[top]	core
Def	l1 = l2	[eq_lbl]	mb basic
Def	Default = > body	[case_default]	prog 1
Def	pq	[band]	bool 1
Def	Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def	Case ptn_var(x) = > body(x) cont	[case_ptn_var]	mb basic
Def	Case(value) body	[case]	prog 1
Def	x=yAtom	[eq_atom]	bool 1
Def	i=j	[eq_int]	bool 1
Def	Case ptn_int(x) = > body(x) cont	[case_ptn_int]	mb basic
Def	Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def	hd(l)	[hd]	list 1
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

About: