is mentioned by

Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst2(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst2(as;r))	[member_col_subst2]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst(as;r))	[member_col_subst]
Def ioa_mentions_trace(A) == (e:eff(). e A.eff & mentions_trace(e.smt.term)) (p:pre(). p A.pre & rel_mentions_trace(p.rel)) (r:rel(). r A.init & rel_mentions_trace(r))	[ioa_mentions_trace]
Def guarded_trace(da;e;I) == r:rel(). r I (k:Label. affects_trace_rel(e;k;r) (t:dec(). t da & t.lbl = k))	[guarded_trace]
Def tc_smt(s;ds;da;de) == mk_dec(s.lbl, s.typ) ds & s.typ term_types(ds;da;de;s.term)	[tc_smt]
Def tc(r;ds;da;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 & Q term_types(ds;da;de;r.args[0]) & Q term_types(ds;da;de;r.args[1]) Case R = > ||de.rel(R)|| = ||r.args|| & (i:. i < ||r.args|| (de.rel(R))[i] term_types(ds;da;de;r.args[i])) Default = > False	[tc]

In prior sections: core int 1 bool 1 int 2 mb nat num thy 1 mb list 1 mb collection mb list 2 mb automata 2 mb state machine fun 1 rel 1

Try larger context: GenAutomata