es:ES, l:IdLnk, tg:Id, e:E.
Thm* kind(e) = rcv(l; tg)
Thm*
Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)
a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a) False| Theorem | Name |
| es:ES, l:IdLnk, tg:Id, e:E.
Thm* kind(e) = rcv(l; tg) Thm*
Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l) | [es-kind-rcv] |
| cites the following: | |
| a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a) False | [not_rcv_locl] |