Thm* 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)) | [ma-send-sub] |
Thm* M1,M2:MsgA.
Thm* M1 M2
Thm* 
Thm* ( k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x).
Thm* (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w)) | [ma-ef-sub] |
Thm* M1,M2:MsgA.
Thm* M1 M2
Thm* 
Thm* ( a:Id, s:M2.state.
Thm* (a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s)) | [ma-npre-sub] |
Thm* M1,M2:MsgA.
Thm* M1 M2
Thm* 
Thm* ( a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v)) | [ma-pre-sub] |
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:( if source(l) = i
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:( if M.da(rcv
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:( if (l; tg))
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:( else Top fi) List.
Thm* M.send(k;l;s;v;ms;i) Prop | [ma-send_wf] |
Thm* M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x).
Thm* M.ef(k,x,s,v,w) Prop | [ma-ef_wf] |
Thm* M:MsgA, a:Id, s:M.state, v:M.da(locl(a)). M.pre(a,s,v) Prop | [ma-pre_wf] |
Thm* M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s) Prop | [ma-npre_wf] |