Nuprl - Proof: world-event-system 12 1 1 1 2 2 2 2 1 1 1 1 1 3 1 2 1 1 2 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 3 1 2 1 1 2 2

1. the_w : World
2. t' :

3. t :

4. l : IdLnk
5. t<t'

||snds(l;t+1)||

||snds(l;t')||

By:	BackThru Thm* l1,l2:T List. l1 l2 \|\|l1\|\|\|\|l2\|\| THEN Unfold `w-snds` 0 THEN BackThru Thm* ll1,ll2:(T List) List. ll1 ll2 concat(ll1) concat(ll2) THEN BackThru Thm* f:(AB), L1,L2:A List. L1 L2 map(f;L1) map(f;L2) THEN BackThru Thm* i,j:. ij upto(i) upto(j)

Generated subgoals:

None

About:

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