Def M.send(k;l;s;v;ms;i)
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> =
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf.
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x.
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf)
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List

is mentioned by

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]

Def PossibleWorld(D;w) Def == FairFifo Def == & (i,x:Id. vartype(i;x) r M(i).ds(x)) Def == & & (i:Id, a:Action(i). Def == & & (isnull(a)  (valtype(i;a) r M(i).da(kind(a)))) Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))) Def == & & (i,x:Id. M(i).init(x,s(i;0).x)) Def == & & (i:Id, t:. Def == & & (isnull(a(i;t)) Def == & & ( Def == & & ((islocal(kind(a(i;t))) Def == & & (( Def == & & ((M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))) Def == & & (& (x:Id.  Def == & & (& (M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)) Def == & & (& (l:IdLnk.  Def == & & (& (M(i).send(kind(a(i;t));l;x. Def == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)) Def == & & (& (x:Id.  Def == & & (& (M(i).frame(kind(a(i;t)) affects x) Def == & & (& ( Def == & & (& (s(i;t).x = s(i;t+1).x  M(i).ds(x)) Def == & & (& (l:IdLnk, tg:Id. Def == & & (& (M(i).sframe(kind(a(i;t)) sends <l,tg>) Def == & & (& ( Def == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)) Def == & & (i,a:Id, t:. Def == & & (t':.  Def == & & (tt' Def == & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a) Def == & & (&  a declared in M(i) Def == & & (&  unsolvable M(i).pre(a,x.s(i;t').x))

[possible-world]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html