A
AA
AA
AA
A(B List)
i:B, s:A. P(i,s) 
M(F(i,s))
M(s)
i:B, s:A. M(G(i,s))M(s)
i:B, s:A. 
P(i,s) M(H(i,s)) < M(s)
m1:.
m1 < m
(u:A.
M(u) = m1
(j:B.
process u j where
process s i ==
if P(i,s) then F(i,s)
else G(i,s) where
xs := N(i,s);
s:= H(i,s);
while not null xs {
s := process s (hd xs);
xs := tl xs;
}
{s:A| M(s)M(u) }))
P(j,u)
a:{s:A| M(s)M(H(j,u)) }.
list_accum(s',i'.process s' i' where
process s i ==
if P(i,s) then F(i,s)
else G(i,s) where
xs := N(i,s);
s:= H(i,s);
while not null xs {
s := process s (hd xs);
xs := tl xs;
} ;a;v)
{s:A| M(s)M(a) }
M(H(j,u)) }
M(a) }
M(s') < m
None
About:
| | | | | | | | | | |