E:Type, eq:EqDecider(E), T,V:(IdIdType), M:(IdLnkIdType),
  loc:(EId), k:(EKnd), v:(e:Eeventtype(k;loc;V;M;e)),
  w,a:(x:Ide:ET(loc(e),x)), snds:(l:IdLnkE(Msg_sub(l; M) List)),
  sndr:({e:E| isrcv(k(e)) }E), i:(e:{e:E| isrcv(k(e)) }||snds
  sndr:({e:E| isrcv(k(e)) }E), i:(e:{e:E| isrcv(k(e)) }||(lnk(k(e))
  sndr:({e:E| isrcv(k(e)) }E), i:(e:{e:E| isrcv(k(e)) }||,sndr(e))||),
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms{i:l}
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(E;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(T;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(M;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(loc;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(k;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(v;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(w;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(a;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(snds;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(sndr;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(i;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(f;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(prd;
  f:(E), prd:({e':E| f(e') }E), cl:(EEProp), p:ESAxioms(cl).
  mk-es(E; eq; T; V; M; loc; k; v; w; a; snds; sndr; i; f; prd; cl; p)  ES

By:	let tacs let  [Trivial;Reduce 0;Auto THEN Analyze -1 THEN Unhide THEN Complete Auto] in Auto THEN Try (Analyze -1 THEN Unhide THEN Complete Auto) THEN Unfolds [`mk-es`;`event_system`] 0 THEN Analyze THEN All (Unfold `event_system_typename`) THENL tacs THEN Repeat (Analyze THENL tacs)

1

1. E : Type 2. EqDecider(E) 3. T : IdIdType 4. V : IdIdType 5. M : IdLnkIdType 6. loc : EId 7. k : EKnd 8. v : e:Eeventtype(k;loc;V;M;e) 9. w : x:Ide:ET(loc(e),x) 10. a : x:Ide:ET(loc(e),x) 11. snds : l:IdLnkE(Msg_sub(l; M) List) 12. sndr : {e:E| isrcv(k(e)) }E 13. i : e:{e:E| isrcv(k(e)) }||snds(lnk(k(e)),sndr(e))|| 14. f : E 15. prd : {e':E| f(e') }E 16. cl : EEProp 17. ESAxioms{i:l} 17. ESAxioms(E; T; M; loc; k; v; w; a; snds; sndr; i; f; prd; cl)     Top

Auto

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