(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
  the_w:World, t',t:, l:IdLnk.
  t'<t  ||snds(l;t')||+||onlnk(l;m(source(l);t'))||||snds(l;t)||
By: Auto
THEN
Subst
(||snds(l;t')||+||onlnk(l;m(source(l);t'))||
(=
(||snds(l;t') @ onlnk(l;m(source(l);t'))||)
0

Generated subgoals:

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'))||
   
2 steps
2 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)||
3 steps

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