(248steps 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: world-event-system 12 1 1 1 2 2 2 2 1 1 1 1 1 1 1 2 2 2 1 1 1 1
1. the_w : World
2. t' : 
3. t : 
4. l : IdLnk
5. t'<t
  ||snds(l;t')||+||onlnk(l;m(source(l);t'))||
  =
  ||snds(l;t') @ onlnk(l;m(source(l);t'))||
   
By: RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   0
THEN
Try
(Fold `member` 0
(THEN
(BackThru Thm* w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||  )

Generated subgoal:

1 6. m(source(l);t')
6. =
6. m(source(l);t')
6.  {m:Msg(the_w.M)| source(mlnk(m)) = source(l) } List
7. {m:Msg(the_w.M)| source(mlnk(m)) = source(l) } List
8. {m:Msg(the_w.M)| source(mlnk(m)) = source(l) } List
9. u : {m:Msg(the_w.M)| source(mlnk(m)) = source(l) }
  u  Msg
1 step

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

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