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

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 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))\|\| ) THEN Unfold `w-Msg` 0

Generated subgoals:

None

About:

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