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