Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, de:sig(), e:{[[de]] rho}, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). tc_ioa(A;de) ![](FONT/eq.png) ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;te;I) ![](FONT/eq.png) tc_pred(I;A.ds; < > ;de) ![](FONT/eq.png) covers_pred(A;I) ![](FONT/eq.png) guarded_trace(A.da;te;I) ![](FONT/eq.png) closed_pred(I) ![](FONT/eq.png) single_valued_decls(A.ds) ![](FONT/eq.png) ( s0,x:[[A]] rho de e.state, act:[[A]] rho de e.action, x':[[A]] rho de e.state, tr:( [[A.da]] rho) List. [[A]] rho de e.init(s0) ![](FONT/eq.png) trace_reachable([[A]] rho de e;s0;mk_trace_env(tr, te).trace;x) ![](FONT/eq.png) [[I]] rho A.ds < > de e x mk_trace_env(tr, te) ![](FONT/eq.png) [[A]] rho de e.trans(x,act,x') ![](FONT/eq.png) (( t:dec(). t A.da & t.lbl = kind(act)) ![](FONT/eq.png) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)) ![](FONT/eq.png) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)) | [vc_trace_correct_action_decl_lemma] |