(29steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: count pairs swap 1 1 1 1 2 1
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)
  sum(if (f(i)<f(j))P(swap(L;n;n+1)[(f(i))],swap(L;n;n+1)[(f(j))]) 1
  sum(else 0 fi-if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)
  =
  if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)],L[n]) 1 else 0 fi
By: Subst'
(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||))
0

Generated subgoals:

1   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||)
4 steps
2   sum(if (f(i)<f(j))P(swap(L;n;n+1)[(f(i))],swap(L;n;n+1)[(f(j))]) 1
  sum(else 0 fi-if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)
  =
  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||)
13 steps

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

(29steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc