(17steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-causl-time 1 1 1 2
1. the_w : World
2. FairFifo
3. e : E
4. z : E
5. isrcv(kind(z))
6. e = sender(z)
  time(e)<time(z)
By: RenameTo `e\'' `z' THEN HypSubst -1 0

Generated subgoal:

1 4. e' : E
5. isrcv(kind(e'))
6. e = sender(e')  E
  time(sender(e'))<time(e')
5 steps

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

(17steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc