is mentioned by

Thm* ds1,ds2:Collection(dec()), x,y:Label, rho:Decl , v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1) v [[ds2]] rho(y)	[decls_mng_rename_member]
Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x)	[decls_mng_member]
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]

In prior sections: mb automata 2

Try larger context: GenAutomata