(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 3 1 2 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
THENA
(Auto
(THEN
(Try (BackThru Thm* w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||  ))

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))||
   
1 step
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_thanequalmemberimpliesall
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