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

By:

Unfold `w-snds` 0 THEN RW (AddrC [2] (RecUnfoldC `upto`)) 0 THEN SplitOnConclITE THEN Try (Complete Auto) THEN Subst' (t+1-1 = t) 0 THEN RWO Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as')) 0 THEN Reduce 0 THEN RWO Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2)) 0 THEN Analyze THEN Try Trivial THEN RWO Thm* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll)) 0 THEN Reduce 0 THEN RWO Thm* l:T List. (l @ nil) ~ l 0 THEN Unfold `w-ml` 0

None

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