A,B:Type, P:(AAProp), f:(BA), x,y:B List.
  (x swap adjacent[P(f(x),f(y))] y)
  
  (map(f;x) swap adjacent[P(x,y)] map(f;y))

By:	Unfold `swap_adjacent` 0 THEN Reduce 0 THEN Inst Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   [B;A;f;x] THEN ParallelOp -2 THEN All ReduceSOAps THEN All (RWW Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]))

1

1. A : Type 2. B : Type 3. P : AAProp 4. f : BA 5. x : B List 6. y : B List 7. i : (||x||-1) 8. P(f(x[i]),f(x[(i+1)])) 9. y = swap(x;i;i+1) 10. ||map(f;x)|| = ||x||     map(f;y) = swap(map(f;x);i;i+1)

1 step

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