(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 2
1. the_w : World
2. FairFifo
3. e,z:E. e <loc z  isrcv(kind(z)) & e = sender(z)  time(e)<time(z)
  n:, e,e':E.
  (e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n e')
  
  time(e)<time(e')
By: InductionOnNat THEN RecUnfold `rel_exp` 0 THEN Reduce 0

Generated subgoals:

1 4. n : 
5. 0<n
6. 0<n-1
6. 
6. (e,e':E.
6. ((e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n-1 e')
6. (
6. (time(e)<time(e'))
7. n = 1
  0<1
  
  (e,e':E.
  ((z:E. 
  ((e <loc z  isrcv(kind(z)) & e = sender(z)  E
  ((& (z e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^0 e'))
  (
  (time(e)<time(e'))
1 step
2 4. n : 
5. 0<n
6. 0<n-1
6. 
6. (e,e':E.
6. ((e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n-1 e')
6. (
6. (time(e)<time(e'))
7. n = 1
  0<n
  
  (e,e':E.
  ((e 
  ((if n=0 x,y. x = y  E
  ((else x,y. z:E. 
  ((else x <loc z  isrcv(kind(z)) & x = sender(z)  E
  ((else & (z 
  ((else & (e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n
  ((else & (-1 y) fi e')
  (
  (time(e)<time(e'))
3 steps

About:
ifthenelseassertnatural_numbersubtractless_thanlambda
equalimpliesandorallexists
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