is mentioned by

Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, te:(LabelLabel). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;I) (vVCs(A;I).trace_consistent_vc(rho;A.da;te;v))	[trace_consistent_ioa_inv_vc]
Thm* vs:VCs{i}, ds,da:Collection{i}(dec()), de:sig(), rho:Decl{i}, e:{sig_mng{i:l}(de; rho)}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vcs{i}(vs;ds;da;de) (vvs.trace_consistent_vc(rho;da;tr.proj;v)) [[vs]] rho ds da de e s tr Prop{i'}	[vcs_mng_wf]
Thm* v:vc{i:l}(), ds,da:Collection(dec()), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vc(v;ds;da;de) trace_consistent_vc(rho;da;tr.proj;v) vc_mng(v;rho;ds;da;de;e;s;tr) Prop	[vc_mng_wf]
Thm* v:vc{i:l}(), ds,da:Collection(dec()), de:sig(). tc_vc(v;ds;da;de) Prop	[tc_vc_wf]
Def ioa_trans_all{i}(A;I) == < ioa_trans(A;a.lbl;I) | a A.da >	[ioa_trans_all]
Def tc_vcs{i}(vs;ds;da;de) == v:vc{i:l}(). v vs tc_vc(v;ds;da;de)	[tc_vcs]
Def [[vs]] rho ds da de e s tr == v:vc{i:l}(). v vs vc_mng(v;rho;ds;da;de;e;s;tr)	[vcs_mng]

In prior sections: mb automata 2

Try larger context: GenAutomata