Nuprl - Proof: sends-rule 2 1

(148steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sends-rule 2 1

1. i : Id
2. k : Knd
3. l : IdLnk
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : (tg:Id

State(ds)

ma-valtype(da; k)

(da(rcv(l; tg))?Void List)) List
7. source(l) = i
8. w : World
9. p : FairFifo
10. FairFifo
11.

i@0,x:Id.
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)

11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if <ds
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,da
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,<[<k,l>],

x.f>
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,

>
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(else fi)))

11. vartype(i@0;x)

r if 2of(1of(if eqof(IdDeq)(i@0,i)

11. vartype(i@0;x)

r if 2of(1of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
11. vartype(i@0;x)

r if 2of(1of(else fi))
11. vartype(i@0;x)

r if (x)
11. vartype(i@0;x)

r else Top fi
12.

i@0:Id, a:Action(i@0).
12.

isnull(a)
12.

12. (valtype(i@0;a)

r if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
12. (valtype(i@0;a)

r else fi.da(kind(a)))
13.

l@0:IdLnk, tg:Id.
13. (w.M(l@0,tg))

r if eqof(IdDeq)(source(l@0),i)

13. (w.M(l@0,tg))

r if <ds,da,,,,<[<k,l>],

x.f>,,,

>
13. (w.M(l@0,tg))

r else fi.da(rcv(l@0; tg))
14.

i@0,x:Id.
14. deq-member(IdDeq;x;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)

14. deq-member(IdDeq;x;1of(1of(2of(2of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
14. deq-member(IdDeq;x;1of(1of(2of(2of(else fi)))))
14.

14. s(i@0;0).x
14. =
14. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
14. 2of(1of(2of(2of(else fi))))
14. (x)
15.

i@0:Id, t:

.
15.

isnull(a(i@0;t))
15.

15. (islocal(kind(a(i@0;t)))
15. (

15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq)
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i)

15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <ds
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,da
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[<k,l>],

x.f>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,

>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else fi))))))
15. (

15. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
15. (2of(1of(2of(2of(2of(else fi)))))
15. ((act(kind(a(i@0;t)))
15. (,

x.s(i@0;t).x
15. (,val(a(i@0;t))))
15. & (

x:Id.
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t))
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(2of(2of(2of(2of(
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if (i@0
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,i)

15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if <ds
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,da
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,<[<k,l>]
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,,

x.f>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,

>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(else fi)))))))
15. & (

15. & (s(i@0;t+1).x
15. & (=
15. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i)

15. & (2of(1of(2of(2of(2of(2of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
15. & (2of(1of(2of(2of(2of(2of(else fi))))))
15. & ((<kind(a(i@0;t)),x>
15. & (,

x.s(i@0;t).x
15. & (,val(a(i@0;t))))
15. & (

l@0:IdLnk.
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if (i@0
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,i)

15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if <ds
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,da
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[<k
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[,l>]
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,

x.
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,f>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,

>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;else fi))))))))
15. & (

15. & (withlnk(l@0;m(i@0;t))
15. & (=
15. & (if source(l@0) = i@0

15. & (if concat(map(

tgf.map(

x.
15. & (if <1of(tgf),x>;2of(tgf)
15. & (if <1of(tgf),x>;((

x.s(i@0;t).x)
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of(
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i)

15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else fi)))))))
15. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l@0>)))
15. & (else nil fi)
15. & (

x:Id.
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq)
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,i)

15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if <ds
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,da
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[<k,l>],

x.f>
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,

>
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(else fi)))))))))
15. & (

(

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],

x.f>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,

>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(else fi))))))))
15. & (

(deq-member(KindDeq;kind(a(i@0;t));(x)))
15. & (

15. & (s(i@0;t).x = s(i@0;t+1).x)
15. & (

l@0:IdLnk, tg:Id.
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of(
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of(
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq)
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i)

15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <ds
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,da
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[<k,l>],

x.f>
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,

>
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else fi))))))))))
15. & (

(

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of(
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],

x.f>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,

>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(else fi)))))))))
15. & (

(deq-member(KindDeq;kind(a(i@0;t));(<l@0,tg>)))
15. & (

15. & (w-tagged(tg; onlnk(l@0;m(i@0;t))) = nil)
16.

i@0,a:Id, t:

.
16.

t':

.
16. t

t'
16. &

isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a)
16. &

a declared in if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
16. &

a declared in else fi
16. &

unsolvable if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
16. &

unsolvable else fi.pre(a,

x.s(i@0;t').x)

(

x:Id. vartype(i;x)

r ds(x)?Top)

& (

e:E. loc(e) = i

(valtype(e)

r ma-valtype(da; kind(e))))

& (

e:E. isrcv(e)

lnk(e) = l

(valtype(e)

r ma-valtype(da; kind(e))))

& ({m:Msg| source(mlnk(m)) = i }

r Msg((

l,tg. da(rcv(l; tg))?Top)))

By:	RepeatFor 3 (Thin -1) THEN AllHyps (h. (InstHyp [i] h THENA Complete Auto THEN Thin h (THEN (Subst ((eqof(IdDeq)(i,i)) ~ true) -1 (THEN (Try (Unfolds [`ma-da`;`ma-din`] -1) (THEN (Reduce -1 (THEN (Try (BackThru Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true)) THEN SplitAndConcl

Generated subgoals:

1 4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : (tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List
7. source(l) = i
8. w : World
9. FairFifo
10. FairFifo
11. l@0:IdLnk, tg:Id.
11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
11. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
12. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
13. x:Id.
13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
  x:Id. vartype(i;x) r ds(x)?Top
4 steps

2 11. l@0:IdLnk, tg:Id.
11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
11. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
12. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
13. x:Id.
13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
  e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e)))
15 steps

3 11. l@0:IdLnk, tg:Id.
11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
11. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
12. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
13. x:Id.
13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
  e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e)))
6 steps

4 11. l@0:IdLnk, tg:Id.
11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
11. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
12. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
13. x:Id.
13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
  {m:Msg| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top))
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(148steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc

1	4. ds : x:Id fp-> Type 5. da : a:Knd fp-> Type 6. f : (tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List 7. source(l) = i 8. w : World 9. FairFifo 10. FairFifo 11. l@0:IdLnk, tg:Id. 11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i) 11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,> 11. (w.M(l@0,tg)) r else fi.da(rcv(l@0; tg)) 12. a:Action(i). isnull(a) (valtype(i;a) r da(kind(a))?Top) 13. x:Id. 13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi x:Id. vartype(i;x) r ds(x)?Top	4 steps
2	11. l@0:IdLnk, tg:Id. 11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i) 11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,> 11. (w.M(l@0,tg)) r else fi.da(rcv(l@0; tg)) 12. a:Action(i). isnull(a) (valtype(i;a) r da(kind(a))?Top) 13. x:Id. 13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi e:E. loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))	15 steps
3	11. l@0:IdLnk, tg:Id. 11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i) 11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,> 11. (w.M(l@0,tg)) r else fi.da(rcv(l@0; tg)) 12. a:Action(i). isnull(a) (valtype(i;a) r da(kind(a))?Top) 13. x:Id. 13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi e:E. isrcv(e) lnk(e) = l (valtype(e) r ma-valtype(da; kind(e)))	6 steps
4	11. l@0:IdLnk, tg:Id. 11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i) 11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,> 11. (w.M(l@0,tg)) r else fi.da(rcv(l@0; tg)) 12. a:Action(i). isnull(a) (valtype(i;a) r da(kind(a))?Top) 13. x:Id. 13. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi {m:Msg\| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top))	3 steps