the_es:ES.
Thm* (Trans e,e':E. (e <loc e'))
Thm* & SWellFounded((e <loc e'))
Thm* & (
e,e':E. loc(e) = loc(e') 
Id 
(e <loc e') 
e = e' (e' <loc e))
Thm* & (
e:E. first(e) (e':E. 
(e' <loc e)))
Thm* & (
e:E.
Thm* & (
first(e)
Thm* & (
Thm* & ((pred(e) <loc e) & (
e':E. ((pred(e) <loc e') & (e' <loc e))))
Thm* & (
e:E.
Thm* & (
first(e)
Thm* & (
Thm* & ((
x:Id. (x when e) = (x after pred(e)) vartype(loc(e);x)))
Thm* & (Trans e,e':E. (e < e'))
Thm* & SWellFounded((e < e'))
Thm* & (
e:E.
Thm* & (isrcv(e)
Thm* & (
Thm* & (sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))
Msg)
Thm* & (
e,e':E. (e <loc e') (e < e'))
Thm* & (
e:E. isrcv(e) (sender(e) < e))
Thm* & (
e,e':E.
Thm* & ((e < e')
Thm* & (
Thm* & (
first(e') & (e < pred(e')) e = pred(e') E
Thm* & (
isrcv(e') & (e < sender(e')) e = sender(e') E)
Thm* & (
e:E. isrcv(e) loc(e) = destination(lnk(e)))
Thm* & (
e:E, l:IdLnk.
Thm* & (
loc(e) = source(l) sends(l;e) = nil (Msg on l) List)
Thm* & (
e,e':E.
Thm* & (isrcv(e)
Thm* & (
Thm* & (isrcv(e')
Thm* & (
Thm* & (lnk(e) = lnk(e')
Thm* & (
Thm* & (((e <loc e')
Thm* & ((
Thm* & (((sender(e) <loc sender(e'))
Thm* & ((
sender(e) = sender(e') E & index(e)<index(e')))
Thm* & (
e:E, l:IdLnk, n:
||sends(l;e)||.
Thm* & (
e':E. isrcv(e') & lnk(e') = l & sender(e') = e E & index(e') = n 
)