A,B:Dsys. A 
B 
(w:World. PossibleWorld(B;w) PossibleWorld(A;w))M1,M2:MsgA, k:Knd. M1 M2 (M2.da(k) r M1.da(k))V:(Id
Type), M1,M2:MsgA.
Thm* (
x:Id. V(x) r M2.ds(x))
Thm*
Thm* M1
M2 (x:Id, v:V(x). M2.init(x,v) M1.init(x,v))M1,M2:MsgA, x:Id. M1 M2 (M2.ds(x) r M1.ds(x))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))r B) (B r C) (A r C)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))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))M1,M2:MsgA.
Thm* M1
M2 (k:Knd, x:Id. M2.frame(k affects x) M1.frame(k affects x))M1,M2:MsgA.
Thm* M1
M2
Thm*
Thm* (
k:Knd, l:IdLnk, tg:Id.
Thm* (M2.sframe(k sends <l,tg>)
M1.sframe(k sends <l,tg>))M1,M2:MsgA. M1 M2 (a:Id. a declared in M1 a declared in M2)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))