IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-causl-time111211111 1. the_w : World
2. FairFifo
3. e : E
4. e' : E
5. isrcv(kind(e'))
6. e = sender(e')
7. n : time(e')
8. match(lnk(kind(e'));n;time(e'))
9. match(lnk(kind(e'));mu(t.match(lnk(kind(e'));t;time(e')));time(e'))
10. i:.
10. i<mu(t.match(lnk(kind(e'));t;time(e'))) match(lnk(kind(e'));i;time(e'))
11. mu(t.match(lnk(kind(e'));t;time(e')))n n:. (t.match(lnk(kind(e'));t;time(e')))(n)
By:
Reduce 0 THEN InstConcl [n]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html