At:
ioa all mng action
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:Label
decl_type([[ioa_all(I; i.A(i)).da]] rho;l)
7.
i: I
8.
l: Label
9.
x: [[ioa_all(I; i.A(i)).da]] rho(l)
10.
d: dec()
11.
d
A(i).da
12.
d.lbl = l
d
i:I. A(i).da
By:
RWW "member_col_union" 0
THEN
AutoInstConcl []
Generated subgoals:
None
About: