Nuprl - Proof: send-once realizes

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: send-once realizes

T,A:Type, a:Id, f:(A

T), tg:Id, l:IdLnk, x:Id.

"done" = x

loc.

(send-once(loc;T;A;a;f;tg;l;x))

realizes es.(vartype(source(l);x)

r A)

realizes es.& (

e:E. kind(e) = rcv(l; tg)

Knd

(valtype(e)

r T))

realizes es.& (

e:E.

realizes es.& (kind(e) = rcv(l; tg)

Knd

realizes es.& (& val(e) = f((x when sender(e)))

realizes es.& (& & kind(sender(e)) = locl(a)

Knd

realizes es.& (& & (

e':E.

realizes es.& (& & (kind(e') = rcv(l; tg)

Knd

realizes es.& (& & (

realizes es.& (& & (kind(sender(e')) = locl(a)

Knd

e' = e

E))

By:	RealizerSetup THEN InstRealizerLemma `once` [a;source(l)]

Generated subgoal:

1 1. T : Type
2. A : Type
3. a : Id
4. f : AT
5. tg : Id
6. l : IdLnk
7. x : Id
8. "done" = x
9. A
10. T
11. (loc.(send-once(loc;T;A;a;f;tg;l;x)))  Dsys
12. D' : Dsys
13. loc.(send-once(loc;T;A;a;f;tg;l;x))  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. e@source(l).kind(e) = locl(a)
17. & e@source(l).e'@source(l).kind(e) = locl(a)
17. & e@source(l).e'@source(l).
17. & kind(e') = locl(a)  Knd  e = e'  E
  (vartype(source(l);x) r A)
  & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
  & (e:E.
  & (kind(e) = rcv(l; tg)
  & (& val(e) = f((x when sender(e)))  T
  & (& & kind(sender(e)) = locl(a)
  & (& & (e':E.
  & (& & (kind(e') = rcv(l; tg)  kind(sender(e')) = locl(a)  e' = e))
7 steps

About:

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

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