(70steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s-sends-rule1 2 4 1
1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. f : AB(T List)
9. rcv(l; tg) = k  T = B
10. @source(l): ma-single-sends(x : A;
10. @source(l): ma-single-sends(k : B  rcv(l; tg) : T;
10. @source(l): ma-single-sends(k;
10. @source(l): ma-single-sends(l;
10. @source(l): ma-single-sends([<tg,s,v. f(s(x),v)>])
10.  Dsys
11. D:Dsys. 
11. @source(l): ma-single-sends(x : A;
11. @source(l): ma-single-sends(k : B  rcv(l; tg) : T;
11. @source(l): ma-single-sends(k;
11. @source(l): ma-single-sends(l;
11. @source(l): ma-single-sends([<tg,s,v. f(s(x),v)>])  D
11. 
11. D 
11. realizes es.(x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
11. realizes es.& (e:E. 
11. realizes es.& (loc(e) = source(l)
11. realizes es.& (
11. realizes es.& ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
11. realizes es.& (e:E. 
11. realizes es.& (isrcv(e)
11. realizes es.& (
11. realizes es.& (lnk(e) = l
11. realizes es.& (
11. realizes es.& ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
11. realizes es.& (e:E. 
11. realizes es.& (loc(e) = source(l)
11. realizes es.& (
11. realizes es.& (kind(e) = k
11. realizes es.& (
11. realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
11. realizes es.& (((e':E. 
11. realizes es.& ((((e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
11. realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
11. realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
11. realizes es.& ((& =
11. realizes es.& ((& tagged-list-messages(z.(z when e);val(e);[<tg
11. realizes es.& ((& tagged-list-messages(z.(z when e);val(e);[,s,v. f
11. realizes es.& ((& tagged-list-messages(z.(z when e);val(e);[,s,v. (s(x)
11. realizes es.& ((& tagged-list-messages(z.(z when e);val(e);[,s,v. ,v)>])))
12. @source(l): ma-single-sends(x : A;
12. @source(l): ma-single-sends(k : B  rcv(l; tg) : T;
12. @source(l): ma-single-sends(k;
12. @source(l): ma-single-sends(l;
12. @source(l): ma-single-sends([<tg,s,v. f(s(x),v)>])
12.  Dsys
13. D : Dsys
14. @source(l): ma-single-sends(x : A;
14. @source(l): ma-single-sends(k : B  rcv(l; tg) : T;
14. @source(l): ma-single-sends(k;
14. @source(l): ma-single-sends(l;
14. @source(l): ma-single-sends([<tg,s,v. f(s(x),v)>])  D
15. D':Dsys. 
15. D  D'
15. 
15. (w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (
15. ((x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
15. (& (e:E. 
15. (& (loc(e) = source(l)
15. (& (
15. (& ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
15. (& (e:E. 
15. (& (isrcv(e)
15. (& (
15. (& (lnk(e) = l
15. (& (
15. (& ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
15. (& (e:E. 
15. (& (loc(e) = source(l)
15. (& (
15. (& (kind(e) = k
15. (& (
15. (& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
15. (& (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
15. (& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
15. (& ((& map(e'.<tag(e'),val(e')>;L)
15. (& ((& =
15. (& ((& tagged-list-messages(z.(z when e);val(e);[<tg,s,v. f(s(x),v)>]))))
16. D' : Dsys
17. D  D'
18. w:World, p:FairFifo.
18. PossibleWorld(D';w)
18. 
18. (x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
18. & (e:E. 
18. & (loc(e) = source(l)
18. & (
18. & ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
18. & (e:E. 
18. & (isrcv(e)
18. & (
18. & (lnk(e) = l
18. & (
18. & ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
18. & (e:E. 
18. & (loc(e) = source(l)
18. & (
18. & (kind(e) = k
18. & (
18. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
18. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
18. & ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
18. & ((& map(e'.<tag(e'),val(e')>;L)
18. & ((& =
18. & ((& tagged-list-messages(z.(z when e);val(e);[<tg,s,v. f(s(x),v)>])))
19. w : World
20. p:FairFifo. 
20. PossibleWorld(D';w)
20. 
20. (x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
20. & (e:E. 
20. & (loc(e) = source(l)
20. & (
20. & ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
20. & (e:E. 
20. & (isrcv(e)
20. & (
20. & (lnk(e) = l
20. & (
20. & ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e))))
20. & (e:E. 
20. & (loc(e) = source(l)
20. & (
20. & (kind(e) = k
20. & (
20. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
20. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
20. & ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
20. & ((& map(e'.<tag(e'),val(e')>;L)
20. & ((& =
20. & ((& tagged-list-messages(z.(z when e);val(e);[<tg,s,v. f(s(x),v)>])))
21. p : FairFifo
22. PossibleWorld(D';w)
23. x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top
24. e:E. 
24. loc(e) = source(l)
24. 
24. (valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e)))
25. e:E. 
25. isrcv(e)
25. 
25. lnk(e) = l  (valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e)))
26. e:E. 
26. loc(e) = source(l)
26. 
26. kind(e) = k
26. 
26. (L:{e':E| isrcv(e') & lnk(e') = l } List. 
26. ((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
26. (& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
26. (& map(e'.<tag(e'),val(e')>;L)
26. (& =
26. (& tagged-list-messages(z.(z when e);val(e);[<tg,s,v. f(s(x),v)>]))
27. (vartype(source(l);x) r A)
27. & (e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B))
27. & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
28. e : E
29. loc(e) = source(l)
30. kind(e) = k
31. L:{e':E| isrcv(e') & lnk(e') = l } List. 
31. (e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
31. & (e1,e2:E. e1 before e2  L  (e1 <loc e2))
31. & map(e'.<tag(e'),val(e')>;L)
31. & =
31. & tagged-list-messages(z.(z when e);val(e);[<tg,s,v. f(s(x),v)>])
  L:{e':E| kind(e') = rcv(l; tg) } List. 
  (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e  E)
  & (e1,e2:E. e1 before e2  L  (e1 <loc e2))
  & map(e'.val(e');L) = f((x when e),val(e))  T List
By: ExRepD

Generated subgoal:

1 27. vartype(source(l);x) r A
28. e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)
29. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
30. e : E
31. loc(e) = source(l)
32. kind(e) = k  Knd
33. L : {e':E| isrcv(e') & lnk(e') = l } List
34. e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e  E
35. e1,e2:E. e1 before e2  L  (e1 <loc e2)
36. map(e'.<tag(e'),val(e')>;L)
36. =
36. tagged-list-messages(z.(z when e);val(e);[<tg,s,v. f(s(x),v)>])
36.  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List
  L:{e':E| kind(e') = rcv(l; tg) } List. 
  (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e  E)
  & (e1,e2:E. e1 before e2  L  (e1 <loc e2))
  & map(e'.val(e');L) = f((x when e),val(e))  T List
49 steps

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

(70steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc