Nuprl - Proof: world-event-system 12 1 1 1 2 2 2 2 1 1 1 1 1 1 1 2 2 2 1 1 1 2

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 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)||

By:	Subst ((snds(l;t') @ onlnk(l;m(source(l);t'))) ~ snds(l;t'+1)) 0

Generated subgoals:

1 (snds(l;t') @ onlnk(l;m(source(l);t'))) ~ snds(l;t'+1)
1 step

2 ||snds(l;t'+1)||||snds(l;t)||
1 step

About:

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

1	(snds(l;t') @ onlnk(l;m(source(l);t'))) ~ snds(l;t'+1)	1 step
2	\|\|snds(l;t'+1)\|\|\|\|snds(l;t)\|\|	1 step