Nuprl - Proof: w-causl-time 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-causl-time 1 1 1

1. the_w : World
2. FairFifo

e,z:E. e <loc z

isrcv(kind(z)) & e = sender(z)

time(e)<time(z)

By:	Auto THEN Analyze -1 THEN ExRepD

Generated subgoals:

1 3. e : E
4. z : E
5. e <loc z
  time(e)<time(z)
1 step

2 3. e : E
4. z : E
5. isrcv(kind(z))
6. e = sender(z)  E
  time(e)<time(z)
6 steps

About:

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

1	3. e : E 4. z : E 5. e <loc z time(e)<time(z)	1 step
2	3. e : E 4. z : E 5. isrcv(kind(z)) 6. e = sender(z) E time(e)<time(z)	6 steps