(12steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-match-unique 1 1 1 1
1. the_w : World
2. e : E
3. t : 
4. t' : 
5. FairFifo
6. isrcv(kind(e))
7. t<t'
  ||snds(lnk(kind(e));t)||
  +||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))||||snds(lnk(kind(e));t')||
By: Unfold `w-snds` 0 THEN Unfold `w-ml` 0
THEN
GenConcl ((t1.onlnk(lnk(kind(e));m(source(lnk(kind(e)));t1))) = f)
THENA
(Auto THEN Unfold `w-Msg` 0)
THEN
Subst (onlnk(lnk(kind(e));m(source(lnk(kind(e)));t)) = f(t)) 0

Generated subgoals:

1 8. f : (Msg List)
9. (t1.onlnk(lnk(kind(e));m(source(lnk(kind(e)));t1))) = f
  onlnk(lnk(kind(e));m(source(lnk(kind(e)));t)) = f(t)  Msg List
1 step
2 8. f : (Msg List)
9. (t1.onlnk(lnk(kind(e));m(source(lnk(kind(e)));t1))) = f
  ||concat(map(f;upto(t)))||+||f(t)||||concat(map(f;upto(t')))||
2 steps

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

(12steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc