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)
9. i : ||L||
10. j : ||L||
  if (f(i)<f(j))P(L[i],L[j]) 1 else 0 fi-if (i<j)P(L[i],L[j]) 1
  if (f(i)<f(j))P(L[i],L[j]) 1 else 0 fi-else 0 fi
  =
  if ((i=n)(j=n+1))P(L[i],L[j]) -1
  i; ((i=n+1)(j=n))P(L[i],L[j]) 1
  else 0 fi

By:

AutoBoolCase (i<j) THEN AutoBoolCase (f(i)<f(j)) THEN MoveToConcl -1 THEN Subst' (f(i) = (n, n+1)(i)) 0 THEN EasyHyp THEN Subst' (f(j) = (n, n+1)(j)) 0 THEN EasyHyp THEN Unfold `flip` 0 THEN Reduce 0 THEN AutoBoolCase (i=n) THEN MoveToConcl -1 THEN AutoBoolCase (j=n) THEN MoveToConcl -1 THEN AutoBoolCase (i=n+1) THEN MoveToConcl -1 THEN AutoBoolCase (j=n+1)

1

11. i<j 12. j = n+1   i = n+1      j = n      i = n      nn+1  0-if P(L[i],L[j]) 1 else 0 fi = if P(L[i],L[j]) -1 else 0 fi

1 step

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