M1,M2:MsgA.
Thm* M1
M2
Thm*
Thm* (
k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id
Thm* (
k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(
if source(l) = i
Thm* (
k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg))
Thm* (
k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List.
Thm* (M2.send(k;l;s;v;ms;i)
M1.send(k;l;s;v;ms;i))eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top)