(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 1 1 1 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
28. e:E. loc(e) = source(l)  kind(e) = k  (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
33. L : {e':E| isrcv(e') & lnk(e') = l } List
34. e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e
35. e1,e2:E. e1 before e2  L  (e1 <loc e2)
36. map(e'.<tag(e'),val(e')>;L) = map(x@0.<tg,x@0>;f((x when e),val(e)))
37. e' : E
38. (e'  L)  (isrcv(e') & lnk(e') = l & sender(e') = e)
39. (e'  L)
40. isrcv(e')
41. lnk(e') = l
42. sender(e') = e
43. f((x when e),val(e))  T List
  tag(e') = tg
By: Analyze -5 THEN ExRepD
THEN
AssertBY
(map(e'.<tag(e'),val(e')>;L)[i] = map(x@0.<tg,x@0>;f((x when e),val(e)))[i])
(Analyze THEN RWO Thm* f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L|| 0)
THEN
RWO Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i])) -1
THEN
Reduce -1

Generated subgoals:

1 39. i : 
40. i<||L||
41. e' = L[i]
42. isrcv(e')
43. lnk(e') = l
44. sender(e') = e  E
45. f((x when e),val(e))  T List
46. map(e'.<tag(e'),val(e')>;L)[i]
46. =
46. map(x@0.<tg,x@0>;f((x when e),val(e)))[i]
46.  tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))
  i<||f((x when e),val(e))||
1 step
2 39. i : 
40. i<||L||
41. e' = L[i]
42. isrcv(e')
43. lnk(e') = l
44. sender(e') = e  E
45. f((x when e),val(e))  T List
46. <tag(L[i]),val(L[i])>
46. =
46. <tg,(f((x when e),val(e)))[i]>
46.  tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))
  tag(e') = tg
2 steps

About:
pairproductlistconsnilassertnatural_numberless_than
setlambdaapplyfunctionuniverseequalmember
sqequaltopsubtype_relimpliesandallexists
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