Nuprl - Proof: es-loc-rcv 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: es-loc-rcv 2

1. es : ES
2. e : E
3. l : IdLnk
4. tg : Id
5. kind(e) = rcv(l; tg)
6. isrcv(e)

loc(e) = destination(l) & loc(sender(e)) = source(l)

By:	Unfold `guard` 0 THEN Analyze 0 THEN SupposeNot

Generated subgoals:

1 7. loc(e) = destination(l)
loc(e) = destination(l)
1 step

2 7. loc(sender(e)) = source(l)
loc(sender(e)) = source(l)
4 steps

About:

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

1	7. loc(e) = destination(l) loc(e) = destination(l)	1 step
2	7. loc(sender(e)) = source(l) loc(sender(e)) = source(l)	4 steps