(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
  x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(T List)).
  (rcv(l; tg) = k  T = B)
  
  @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  Dsys
  & (D:Dsys. 
  & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  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: UnivCD THEN Unfold `ma-single-sends1` 0
THEN
Inst Thm: s-sends-rule
[source(l);k;l;x : A;k : B  rcv(l; tg) : T;[<tg,s,v. f(s(x),v)>]]
THENA
Try (Complete Auto)

Generated subgoals:

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
  [<tg,s,v. f(s(x),v)>]
   (tg@0:Id
   (State(x : A)ma-valtype(k : B  rcv(l; tg) : T; k)
   ((k : B  rcv(l; tg) : T(rcv(l; tg@0))?Void List)) List
4 steps
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)  Id
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  IdLnk
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)  Id
10. & (realizes es.& (
10. & (realizes es.& (kind(e) = k  Knd
10. & (realizes es.& (
10. & (realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
10. & (realizes es.& (((e':E. 
10. & (realizes es.& ((((e'  L)
10. & (realizes es.& (((
10. & (realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = 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)>])
10. & (realizes es.& ((&  (tg@0:Id
10. & (realizes es.& ((&  (ma-valtype(k : B  rcv(l; tg) : T; rcv(l; tg@0)
10. & (realizes es.& ((&  (ma-valtype()) List)))
  @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)))
65 steps

About:
pairproductlistconsnilassertvoidsetlambdaapply
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