Def [[A]] rho de e == mk_sm([[A.da]] rho, [[A.ds]] rho, s.[[A.init]] rho A.ds < > de e s niltrace(), s1,a,s2. ( p:pre(). p A.pre  p.kind = kind(a)  [[p.rel]] rho A.ds dec_lookup(A.da;kind(a)) de e s1 value(a) niltrace()) & ( ef:eff(). ef A.eff  ef.kind = kind(a)  s2.ef.smt.lbl = [[ef.smt.term]] 1of(e) s1 value(a) niltrace() [[ef.smt.typ]] rho) & ( fr:frame(). fr A.frame  (kind(a) fr.acts)  s2.fr.var = s1.fr.var [[fr.typ]] rho)) | [ioa_mng] |