mb
automata
4
Sections
GenAutomata
Doc
Def
smts_eff_pred(ss;p) == (
r
p.smts_eff_rel(ss;r))
is mentioned by
Thm*
A:ioa{i:l}(), I:Fmla, rho:Decl, te:(Label
Label
), a:dec().
ioa_mentions_trace(A)
trace_consistent_pred(rho;A.da;te;I)
a
A.da
trace_consistent_pred(rho;A.da;te;smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I))
[trace_consistent_action_effect]
Def
wp(A;a;Q) == smts_eff_pred(action_effect(a;A.eff;A.frame);Q)
[wp]
Def
ioa_trans(A;a;I) == vc_qimp(mk_qimp(a, I
action_pre(a;A.pre), smts_eff_pred(action_effect(a;A.eff;A.frame);I)))
[ioa_trans]
Try larger context:
GenAutomata
mb
automata
4
Sections
GenAutomata
Doc