is mentioned by

Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, de:sig(), e:{[[de]] rho}, te:(LabelLabel). tc_ioa(A;de) ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;I) guarded_trace(A.da;te;I) tc_pred(I;A.ds; < > ;de) covers_pred(A;I) closed_pred(I) single_valued_decls(A.ds) let M = [[A]] rho de e in (s:M.state, tr:([[A.da]] rho) List. (M -tr- > s) [[VCs(A;I)]] rho A.ds A.da de e s mk_trace_env(tr, te)) (M |= always s,tr.[[I]] rho A.ds < > de e s mk_trace_env(tr, te))

[vc_trace_correctness]

In prior sections: mb state machine

Try larger context: GenAutomata