A:ioa{i:l}(), de:sig(), rho:Decl, e:{[[de]] rho}. tc_ioa(A;de) 
ioa_mentions_trace(A) [[A]] rho de e 
sm{i:l}()
ds:Decl({ds}
Prop)({ds}(
da){ds}Prop)
is mentioned by
| Thm* A:ioa{i:l}(), de:sig(), rho:Decl, e:{[[de]] rho}. tc_ioa(A;de) ioa_mentions_trace(A) [[A]] rho de e sm{i:l}() | [ioa_mng_wf] |
In prior sections: mb state machine
Try larger context:
GenAutomata