(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
1. T : Type
2. l : T List
3. x,y:T.
3. (f:(||[x; y]||||l||). 
3. (increasing(f;||[x; y]||) & (j:||[x; y]||. [x; y][j] = l[(f(j))]))
3. 
3. x = y
4. i : 
5. j : 
6. i<||l||
7. j<||l||
8. i = j
9. i<j
  l[j] = l[i]
By: BackThruSomeHyp THEN InstConcl [x.if x=0 j else i fi] THEN Reduce 0
THEN
All Reduce

Generated subgoals:

1 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
  increasing(x.if x=0 j else i fi;2)
2 steps
2 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
  [l[j]; l[i]][j1] = l[if j1=0 j else i fi]
3 steps
3 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. f : 2||l||
11. j1 : 2
  0f(j1)
Auto
4 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. f : 2||l||
11. j1 : 2
  f(j1)<||l||
Auto

About:
listconsnilifthenelsenatural_numberless_thanlambda
applyfunctionuniverseequalimpliesandallexists
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