At:
ioa all mng state
1
1
1
1
1
1
1.
I: Type
2.
A: I
ioa{i:l}()
3.
rho: Decl
4.
de: sig()
5.
e: {[[de]] rho}
6.
s: l:Labeldecl_type([[ioa_all(I; i.A(i)).ds]] rho;l)
7.
i: I
8.
x1: Label
9.
x: [[ioa_all(I; i.A(i)).ds]] rho(x1)
10.
d: dec()
11.
d 
A(i).ds
12.
d.lbl = x1
d 
i:I. A(i).ds
By:
RWW "member_col_union" 0
THEN
AutoInstConcl []
Generated subgoals:
None
About:
