is mentioned by

Def tc_ioa(A;de) == tc_pred(A.init;A.ds; < > ;de) & (p:pre(). p A.pre tc(p.rel;A.ds;dec_lookup(A.da;p.kind);de)) & (ef:eff(). ef A.eff mk_dec(ef.kind, ef.typ) A.da & tc_eff(ef;A.ds;de)) & (f:frame(). f A.frame mk_dec(f.var, f.typ) A.ds)	[tc_ioa]
Def tc_eff(ef;ds;de) == tc_smt(ef.smt;ds; < ef.typ > ;de)	[tc_eff]

Try larger context: GenAutomata