(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
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
10. & (D:Dsys. 
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)>])  D
10. & (
10. & (D 
10. & (realizes es.(x@0:Id. vartype(source(l);x@0) r x : A(x@0)?Top)
10. & (realizes es.& (e:E. 
10. & (realizes es.& (loc(e) = source(l)
10. & (realizes es.& (
10. & (realizes es.& ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e)
10. & (realizes es.& ((valtype(e) r ma-valtype()))
10. & (realizes es.& (e:E. 
10. & (realizes es.& (isrcv(e)
10. & (realizes es.& (
10. & (realizes es.& (lnk(e) = l
10. & (realizes es.& (
10. & (realizes es.& ((valtype(e) r ma-valtype(k : B  rcv(l; tg) : T; kind(e)
10. & (realizes es.& ((valtype(e) r ma-valtype()))
10. & (realizes es.& (e:E. 
10. & (realizes es.& (loc(e) = source(l)
10. & (realizes es.& (
10. & (realizes es.& (kind(e) = k
10. & (realizes es.& (
10. & (realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
10. & (realizes es.& (((e':E. 
10. & (realizes es.& ((((e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
10. & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
10. & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
10. & (realizes es.& ((& =
10. & (realizes es.& ((& tagged-list-messages(z.
10. & (realizes es.& ((& (z when e);val(e);[<tg,s,v. f(s(x),v)>]))))
  @source(l): ma-single-sends(x : A;
  @source(l): ma-single-sends(k : B  rcv(l; tg) : T;
  @source(l): ma-single-sends(k;
  @source(l): ma-single-sends(l;
  @source(l): ma-single-sends([<tg,s,v. f(s(x),v)>])
   Dsys
  & (D:Dsys. 
  & (@source(l): ma-single-sends(x : A;
  & (@source(l): ma-single-sends(k : B  rcv(l; tg) : T;
  & (@source(l): ma-single-sends(k;
  & (@source(l): ma-single-sends(l;
  & (@source(l): ma-single-sends([<tg,s,v. f(s(x),v)>])  D
  & (
  & (D 
  & (realizes es.(vartype(source(l);x) r A)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = source(l)  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = k  Knd  (valtype(e) r B))
  & (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = source(l)  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = k  Knd
  & (realizes es.& (
  & (realizes es.& ((L:{e':E| kind(e') = rcv(l; tg)  Knd } List. 
  & (realizes es.& (((e':E. 
  & (realizes es.& ((((e'  L)
  & (realizes es.& (((
  & (realizes es.& (((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E)
  & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
  & (realizes es.& ((& map(e'.val(e');L) = f((x when e),val(e))  T List)))
By: ExRepD THEN Analyze 0 THEN Try Trivial THEN ParallelOp -2
THEN
RepeatFor 7 (ParallelOp -1)
THEN
ExRepD
THEN
BetterSplitAndConcl

Generated subgoals:

1 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)  Id
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  IdLnk
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)  Id
11. realizes es.& (
11. realizes es.& (kind(e) = k  Knd
11. realizes es.& (
11. realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
11. realizes es.& (((e':E. 
11. realizes es.& ((((e'  L)
11. realizes es.& (((
11. realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = 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)>])
11. realizes es.& ((&  (tg@0:Id
11. realizes es.& ((&  (ma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0)
11. realizes es.& ((&  (ma-valtype()) List))
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  Knd
15. (& (
15. (& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
15. (& (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
15. (& ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)))
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  Knd
18. & (
18. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
18. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
18. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
20. & (
20. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
20. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
20. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
26. 
26. (L:{e':E| isrcv(e') & lnk(e') = l } List. 
26. ((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
26. (&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)
  vartype(source(l);x) r A
1 step
2 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)  Id
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  IdLnk
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)  Id
11. realizes es.& (
11. realizes es.& (kind(e) = k  Knd
11. realizes es.& (
11. realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
11. realizes es.& (((e':E. 
11. realizes es.& ((((e'  L)
11. realizes es.& (((
11. realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = 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)>])
11. realizes es.& ((&  (tg@0:Id
11. realizes es.& ((&  (ma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0)
11. realizes es.& ((&  (ma-valtype()) List))
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  Knd
15. (& (
15. (& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
15. (& (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
15. (& ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)))
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  Knd
18. & (
18. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
18. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
18. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
20. & (
20. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
20. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
20. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
26. 
26. (L:{e':E| isrcv(e') & lnk(e') = l } List. 
26. ((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
26. (&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)
27. vartype(source(l);x) r A
  e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)
2 steps
3 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)  Id
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  IdLnk
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)  Id
11. realizes es.& (
11. realizes es.& (kind(e) = k  Knd
11. realizes es.& (
11. realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
11. realizes es.& (((e':E. 
11. realizes es.& ((((e'  L)
11. realizes es.& (((
11. realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = 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)>])
11. realizes es.& ((&  (tg@0:Id
11. realizes es.& ((&  (ma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0)
11. realizes es.& ((&  (ma-valtype()) List))
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  Knd
15. (& (
15. (& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
15. (& (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
15. (& ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)))
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  Knd
18. & (
18. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
18. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
18. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
20. & (
20. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
20. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
20. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
26. 
26. (L:{e':E| isrcv(e') & lnk(e') = l } List. 
26. ((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
26. (&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)
27. vartype(source(l);x) r A
28. e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)
  e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
10 steps
4 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)  Id
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  IdLnk
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)  Id
11. realizes es.& (
11. realizes es.& (kind(e) = k  Knd
11. realizes es.& (
11. realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
11. realizes es.& (((e':E. 
11. realizes es.& ((((e'  L)
11. realizes es.& (((
11. realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = 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)>])
11. realizes es.& ((&  (tg@0:Id
11. realizes es.& ((&  (ma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0)
11. realizes es.& ((&  (ma-valtype()) List))
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  Knd
15. (& (
15. (& ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
15. (& (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
15. (& ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)))
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  Knd
18. & (
18. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
18. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
18. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
20. & (
20. & ((L:{e':E| isrcv(e') & lnk(e') = l } List. 
20. & (((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
20. & ((&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List))
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  Knd
26. 
26. (L:{e':E| isrcv(e') & lnk(e') = l } List. 
26. ((e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = 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)>])
26. (&  (tg@0:Idma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0))) List)
27. (vartype(source(l);x) r A)
27. & (e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B))
27. & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
  e:E. 
  loc(e) = source(l)
  
  kind(e) = k  Knd
  
  (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)
51 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