is mentioned by

Thm* A:ioa{i:l}(), as:(LabelTerm) List, k:Label. ioa_mentions_trace(A) (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) subst_mentions_trace(as)	[effect_subst_mentions_trace]
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]
Thm* as:(LabelTerm) List. subst_mentions_trace(as) (i:||as||. mentions_trace(2of(as[i])))	[assert_subst_mentions_trace]
Def rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) == list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args)	[rel_mng_2]
Def [[r]] rho ds da de e s a tr == list_accum(x,t.x([[t]] 1of(e) s a tr);[[r.name]] rho 2of(e) ;r.args)	[rel_mng]
Def subst_mentions_trace(as) == reduce(a,b. mentions_trace(2of(a)) b;false;as)	[subst_mentions_trace]

In prior sections: core mb list 1 mb automata 1 prog 1 mb record mb automata 2 mb state machine

Try larger context: GenAutomata