i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type,
  f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
  source(l) = i
  
  @i: ma-single-sends(ds; da; k; l; f)  Dsys
  & (D:Dsys. 
  & (@i: ma-single-sends(ds; da; k; l; f)  D
  & (
  & (D 
  & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
  & (realizes es.& (e:E. 
  & (realizes es.& (isrcv(e)
  & (realizes es.& (
  & (realizes es.& (lnk(e) = l  IdLnk
  & (realizes es.& (
  & (realizes es.& ((valtype(e) r ma-valtype(da; kind(e))))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = k  Knd
  & (realizes es.& (
  & (realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
  & (realizes es.& (((e':E. 
  & (realizes es.& ((((e'  L)
  & (realizes es.& (((
  & (realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
  & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
  & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
  & (realizes es.& ((& =
  & (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
  & (realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List)))

By:

NewSpecializeEsLemmaOn Thm: better-sends-rule ma-single-sends(ds; da; k; l; f) THEN Try (Unfold `ma-valtype` 0 THEN Complete Auto) THEN Try (RevHypSubst' -2 0 THEN AllHyps (h.BackThru h THEN Complete Auto)) THEN Try (Analyze -1 THEN Unhide THEN ExRepD) THEN Subst' (rcv(l; tag(e')) = kind(e')) 0 THEN Try BackThruSomeHyp THEN RevHypSubst' -1 0 THEN MoveToConcl -2 THEN Unfolds [`es-isrcv`;`es-lnk`;`es-tag`] 0 THEN GenConclAtAddr [2;3] THEN Analyze -2 THEN Analyze -2 THEN Unfolds [`isrcv`;`lnk`;`tagof`] 0 THEN Reduce 0 THEN Fold `rcv` 0

None

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