Nuprl - Proof: world-event-system 10

(248steps 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: world-event-system 10

1. the_w : World
2. FairFifo
3.

e,e':E. loc(e) = loc(e')

e <c e'

e = e'

e' <c e
4.

e:E. first(e)

(

e':E. loc(e') = loc(e)

e' <c e)
5.

e:E.
5.

first(e)
5.

5. loc(pred(e)) = loc(e) & pred(e) <c e
5. & (

e':E. loc(e') = loc(e)

(pred(e) <c e' & e' <c e))
6.

e:E.

first(e)

(

x:Id. (x when e) = (x after pred(e)))
7. Trans e,e':E. e <c e'
8. SWellFounded(e <c e')
9.

e:E.
9. isrcv(kind(e))
9.

9. sends(lnk(kind(e));sender(e))[index(e)]
9. =
9. msg(lnk(kind(e));tag(kind(e));val(e))
10.

e:E. isrcv(kind(e))

sender(e) <c e
11.

e,e':E.
11. e <c e'
11.

11.

first(e') & e <c pred(e')

e = pred(e')
11.

isrcv(kind(e')) & e <c sender(e')

e = sender(e')

e:E. isrcv(kind(e))

loc(e) = destination(lnk(kind(e)))

By:	Unfold `fair-fifo` 2 THEN ExRepD THEN Analyze -2 THEN Analyze -3 THEN All (Unfolds [`w-loc`;`w-time`;`w-ekind`]) THEN All Reduce THEN All (Unfold `w-act`) THEN All Reduce

Generated subgoal:

1 2. i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List
3. i:Id, t:.
3. isnull(a(i;t))
3.
3. (x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List
4. i:Id, t:, l:IdLnk.
4. isrcv(l;a(i;t))
4.
4. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg
5. l:IdLnk, t:.
5. t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List
6. e,e':E. 1of(e) = 1of(e')  e <c e'  e = e'  e' <c e
7. e:E. first(e)  (e':E. 1of(e') = 1of(e)  e' <c e)
8. e:E.
8. first(e)
8.
8. 1of(pred(e)) = 1of(e) & pred(e) <c e
8. & (e':E. 1of(e') = 1of(e)  (pred(e) <c e' & e' <c e))
9. e:E.
9. first(e)  (x:Id. (x when e) = (x after pred(e))  vartype(1of(e);x))
10. Trans e,e':E. e <c e'
11. SWellFounded(e <c e')
12. e:E.
12. isrcv(kind(a(1of(e);2of(e))))
12.
12. sends(lnk(kind(a(1of(e);2of(e))));sender(e))[index(e)]
12. =
12. msg(lnk(kind(a(1of(e);2of(e))));tag(kind(a(1of(e);2of(e))));val(e))
12.  Msg(the_w.M)
13. e:E. isrcv(kind(a(1of(e);2of(e))))  sender(e) <c e
14. e,e':E.
14. e <c e'
14.
14. first(e') & e <c pred(e')  e = pred(e')  E
14.  isrcv(kind(a(1of(e');2of(e')))) & e <c sender(e')  e = sender(e')  E
15. e1 : Id
16. e2 :
17. isnull(a(e1;e2))
18. isrcv(kind(a(e1;e2)))
  e1 = destination(lnk(kind(a(e1;e2))))
3 steps

About:

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

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