1. T : Type
2. L : T List
3. P : TT
4. n : (||L||-1)
5. (n, n+1)  ||L||||L||
6. ||swap(L;n;n+1)|| = ||L||
7. f : ||L||||L||
8. i:||L||. f(i) = (n, n+1)(i)
  if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)],L[n]) 1 else 0 fi
  =
  sum(if ((i=n)(j=n+1))P(L[i],L[j]) -1
  sum(i; ((i=n+1)(j=n))P(L[i],L[j]) 1
  sum(else 0 fi | i < ||L||; j < ||L||)

By:	Inst Thm: pair support double sum [||L|| ;||L|| ;i,j. if ((i=n)(j=n+1))P(L[i],L[j]) -1 ;i,j. i; ((i=n+1)(j=n))P(L[i],L[j]) 1 ;i,j. else 0 fi ;n ;n+1 ;n+1 ;n] THEN All ReduceSOAps

1	9. x : ||L|| 10. y : ||L|| 11. (x = n & y = n+1) 12. (x = n+1 & y = n)   if ((x=n)(y=n+1))(P(L[x],L[y])) -1   i; ((x=n+1)(y=n))(P(L[x],L[y])) 1   else 0 fi   =   0	1 step
2	9. sum(if ((x=n)(y=n+1))(P(L[x],L[y])) -1 9. sum(i; ((x=n+1)(y=n))(P(L[x],L[y])) 1 9. sum(else 0 fi | x < ||L||; y < ||L||) 9. = 9. if ((n=n)(n+1=n+1))(P(L[n],L[(n+1)])) -1 9. i; ((n=n+1)(n+1=n))(P(L[n],L[(n+1)])) 1 9. else 0 fi+if ((n+1=n)(n=n+1))(P(L[(n+1)],L[n])) -1 9. else 0 fi+i; ((n+1=n+1)(n=n))(P(L[(n+1)],L[n])) 1 9. else 0 fi+else 0 fi   if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)],L[n]) 1 else 0 fi   =   sum(if ((i=n)(j=n+1))(P(L[i],L[j])) -1   sum(i; ((i=n+1)(j=n))(P(L[i],L[j])) 1   sum(else 0 fi | i < ||L||; j < ||L||)	2 steps

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