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) guarded_trace(A.da;te;I) ![](FONT/eq.png) tc_pred(I;A.ds; < > ;de) ![](FONT/eq.png) covers_pred(A;I) ![](FONT/eq.png) closed_pred(I) ![](FONT/eq.png) single_valued_decls(A.ds) ![](FONT/eq.png) let M = [[A]] rho de e in ( s:M.state, tr:( [[A.da]] rho) List. (M -tr- > s) ![](FONT/eq.png) [[VCs(A;I)]] rho A.ds A.da de e s mk_trace_env(tr, te)) ![](FONT/eq.png) (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![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;te;I) ![](FONT/eq.png) ( v VCs(A;I).trace_consistent_vc(rho;A.da;te;v)) | [trace_consistent_ioa_inv_vc] |
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] |
Thm* A:ioa{i:l}(), Q:Fmla, rho:Decl, R:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ), k:Label. ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;R;Q) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;R;wp(A;k;Q)) | [trace_consistent_wp] |
Thm* A:ioa{i:l}(), Q:Fmla, rho:Decl, R:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ), k:Label. ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;R;Q) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;R;wp2(A;k;Q)) | [trace_consistent_wp2] |
Thm* da:Collection(dec()), P:Fmla, rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). trace_consistent_pred(rho;da;te;P) ![](FONT/eq.png) trace_consistent_pred(rho;da;te;(P)') | [trace_consistent_pred_addprime] |
Thm* da:Collection(dec()), P:Fmla, rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). trace_consistent_pred(rho;da;te;P) ![](FONT/eq.png) trace_consistent_pred(rho;da;te;pred_unprime(P)) | [trace_consistent_pred_unprime] |
Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ), a:dec(). ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;te;I) ![](FONT/eq.png) a A.da ![](FONT/eq.png) trace_consistent_pred(rho;A.da;te;smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I)) | [trace_consistent_action_effect] |
Thm* A:ioa{i:l}(), rho:Decl, r:rel(), R:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ), k:Label. ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_rel(rho;A.da;R;r) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r)) | [trace_consistent_wp2_rel] |
Thm* A:ioa{i:l}(), rho:Decl, r:rel(), R:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ), k:Label. ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_rel(rho;A.da;R;r) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r)) | [trace_consistent_wp_rel] |
Thm* A:ioa{i:l}(), rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;te;A.init) | [trace_consistent_init] |
Thm* A:ioa{i:l}(), rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ), k:Label. ioa_mentions_trace(A) ![](FONT/eq.png) trace_consistent_pred(rho;A.da;te;action_pre(k;A.pre)) | [trace_consistent_action_pre] |
Thm* p,q:Fmla, rho:Decl, da:Collection(dec()), R:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). trace_consistent_pred(rho;da;R;p q) ![](FONT/if_big.png) trace_consistent_pred(rho;da;R;p) & trace_consistent_pred(rho;da;R;q) | [trace_consistent_pred_and] |
Thm* p:Fmla, rho:Decl, da:Collection(dec()), R:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). trace_consistent_pred(rho;da;R;p) Prop | [trace_consistent_pred_wf] |
Thm* r:rel(), as:(Label Term) List, daa:Collection(dec()), rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). trace_consistent_rel(rho;daa;te;r) ![](FONT/eq.png) subst_mentions_trace(as) ![](FONT/eq.png) trace_consistent_rel(rho;daa;te;rel_subst2(as;r)) | [trace_consistent_rel_subst2] |
Thm* r:rel(), as:(Label Term) List, daa:Collection(dec()), rho:Decl, te:(Label![](FONT/dash.png) Label![](FONT/dash.png) ![](FONT/then_med.png) ). trace_consistent_rel(rho;daa;te;r) ![](FONT/eq.png) subst_mentions_trace(as) ![](FONT/eq.png) trace_consistent_rel(rho;daa;te;rel_subst(as;r)) | [trace_consistent_rel_subst] |