Nuprl - Proof: s-sends-rule1 2 1

(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

1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. f : A

(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'

isrcv(e') & lnk(e') = l & sender(e') = e)
11. realizes es.& ((& (

e1,e2:E. e1 before e2

(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'

isrcv(e') & lnk(e') = l & sender(e') = e)
15. (& ((& (

e1,e2:E. e1 before e2

(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'

isrcv(e') & lnk(e') = l & sender(e') = e)
18. & ((& (

e1,e2:E. e1 before e2

(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'

isrcv(e') & lnk(e') = l & sender(e') = e)
20. & ((& (

e1,e2:E. e1 before e2

(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'

isrcv(e') & lnk(e') = l & sender(e') = e)
26. (& (

e1,e2:E. e1 before e2

(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)>]))

vartype(source(l);x)

r A

By:	InstHyp [x] -4 THEN Reduce -1

Generated subgoals:

None

About:

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