is mentioned by

Thm* t:ioa{i:l}(). t.frame Collection(frame())	[ioa_frame_wf]
Def ioa{i:l}() == Collection(dec())Collection(dec())Collection(rel())Collection(pre())Collection(eff()) Collection(frame())	[ioa]

Try larger context: GenAutomata