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

(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 1

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

T

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. x :

||L||
10. y :

||L||
11.

(x = n & y = n+1)
12.

(x = n+1 & y = n)

if ((x=

n)

(y=

n+1))

(P(L[x],L[y]))

-1

i; ((x=

n+1)

(y=

n))

(P(L[x],L[y]))

1

else 0 fi

=

0

By:	AutoBoolCase (x=n) THEN AutoBoolCase (y=n+1) THEN AutoBoolCase (x=n+1) THEN AutoBoolCase (y=n) THEN AllHyps (h.Analyze h THEN Complete Auto)

Generated subgoals:

None

About:

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