Nuprl - Proof: count pairs swap 1 1 1 1 2 1 2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: count pairs swap 1 1 1 1 2 1 2 1 1 1

1. T : Type
2. L : T List
3. T

4. n :

(||L||-1)
5. (n, n+1)

||L||

||L||
6. ||swap(L;n;n+1)|| = ||L||
7. f :

||L||

||L||
8.

||L||. f(i) = (n, n+1)(i)
9. i :

||L||
10.

||L||

L[((n, n+1)((n, n+1)(i)))] = L[i]

By:	Subst' ((n, n+1)((n, n+1)(i)) = i) 0

Generated subgoals:

1 (n, n+1)((n, n+1)(i)) = i
1 step

2 L[i] = L[i]
Auto

About:

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