BA

BAA

BAA

BAA

BA(B List)

A

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)

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; } ;H(j,u);N(j,u)) {s:A| M(s)M(H(j,u)) }

1

18. z: B List 19. 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;z) {s:A| M(s)M(a) }

6 steps

About: