A:(I
ioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:{[[ioa_all(I; i.A(i)).ds]] rho}, i:I. s 
[[A(i)]] rho de e.stateds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 
d.lbl = x d ds1) v [[ds2]] rho(x)| Theorem | Name | ||
| Thm* A:(Iioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:{[[ioa_all(I; i.A(i)).ds]] rho}, i:I. s [[A(i)]] rho de e.state | [ioa_all_mng_state] | ||
| cites | |||
| Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x) | [decls_mng_member] |