T:Type, L:T List, P:(TT), n:(||L||-1).
  count(x < y in swap(L;n;n+1) | P(x,y))
  =
  count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)]
  count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P,L[n])
  count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if 1
  count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+else 0 fi

By:	Auto THEN Unfold `count_pairs` 0 THEN Subst' (||swap(L;n;n+1)|| = ||L||) 0 THEN Try (BackThru Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  )

1

1. T : Type 2. L : T List 3. P : TT 4. n : (||L||-1)   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

28 steps

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