A:ioa{i:l}(), rho:Decl, de:sig(), act:(
[[A.da]] rho), r,r0:rel(). tc_ioa(A;de) 
r 
smts_eff_rel(action_effect(kind(act);A.eff;A.frame);r0) 
rel_eq(rel_unprime(r);rel_unprime(r0)) (
t:dec(). t A.da & t.lbl = kind(act))
t.unprime(t);r.args))
is mentioned by
| Thm* A:ioa{i:l}(), rho:Decl, de:sig(), act:([[A.da]] rho), r,r0:rel(). tc_ioa(A;de) r smts_eff_rel(action_effect(kind(act);A.eff;A.frame);r0) rel_eq(rel_unprime(r);rel_unprime(r0)) (t:dec(). t A.da & t.lbl = kind(act)) | [rel_effect_lemma] |
In prior sections: mb automata 3
Try larger context:
GenAutomata