is mentioned by

Def VCs(A;I) == < *vc_imp(mk_imp(A.init, I))* > +* ioa_trans_all{i}(A;I)

[ioa_inv_vc]

Try larger context: GenAutomata