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)
is mentioned
In prior sections:
mb automata 4