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

By:	AssertBY (||swap(L;n;n+1)|| = ||L||) (BackThru Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  )

1

6. ||swap(L;n;n+1)|| = ||L||     sum(if (i<j)P(swap(L;n;n+1)[i],swap(L;n;n+1)[j]) 1   sum(else 0 fi | i < ||L||; j < ||L||)   =   sum(if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)+if P(L[n]   sum(if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)+if P,L[(n   sum(if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)+if P+1)])   sum(if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)+if -1   sum(if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)+else 0 fi   +if P(L[(n+1)],L[n]) 1 else 0 fi

26 steps

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