es:ES, e:E, l:IdLnk, tg:Id.
Thm* kind(e) = rcv(l; tg)
Thm*
Thm* loc(e) = destination(l) & loc(sender(e)) = source(l)
the_es:ES, e:E. isrcv(e) index(e) 
||sends(lnk(e);sender(e))||| Theorem | Name |
| es:ES, e:E, l:IdLnk, tg:Id.
Thm* kind(e) = rcv(l; tg) Thm*
Thm* loc(e) = destination(l) & loc(sender(e)) = source(l) | [es-loc-rcv] |
| cites the following: | |
| the_es:ES, e:E. isrcv(e) index(e) ||sends(lnk(e);sender(e))|| | [es-index_wf] |