At:
ioa all mng state
1
1.
I: Type
2.
A: I
ioa{i:l}()
3.
rho: Decl
4.
de: sig()
5.
e: {[[de]] rho}
6.
s: {[[ioa_all(I; i.A(i)).ds]] rho}
7.
i: I
s 
[[A(i)]] rho de e.state
By:
Unfolds [`ioa_mng`] 0
THEN
Reduce 0
Generated subgoal:
| 1 | s {[[A(i).ds]] rho} |
About:
