Nuprl - Proof: no repeats iff 2 2 1 2 1

(26steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no repeats iff 2 2 1 2 1

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

x,y:T.
3. (

f:(

2

||l||). increasing(f;2) & (

j:

2. [x; y][j] = l[(f(j))]))

x = y
4. i :

5. j :

6. i<||l||
7. j<||l||
8.

i = j
9.

i<j
10. j1 :

2
11. j1 = 0

[l[j]; l[i]][j1] = l[j]

By:	HypSubstSq -1 0 THEN Reduce 0

Generated subgoals:

None

About:

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

(26steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc