Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, de:sig(), e:{[[de]] rho}, te:(Label Label  ). 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] |
Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, te:(Label Label  ). ioa_mentions_trace(A)  trace_consistent_pred(rho;A.da;te;I)  ( v VCs(A;I).trace_consistent_vc(rho;A.da;te;v)) | [trace_consistent_ioa_inv_vc] |
Thm* A:ioa{i:l}(), I:Fmla, de:sig(). tc_ioa(A;de)  tc_pred(I;A.ds; < > ;de)  covers_pred(A;I)  closed_pred(I)  single_valued_decls(A.ds)  tc_vcs{i}(VCs(A;I);A.ds;A.da;de) | [tc_ioa_inv_vc] |