(27steps 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: swap adjacent decomp 1 2 2
1. A : Type
2. L : A List
3. 1<||L||
4. ||tl(L)|| = ||L||-1
5. ||tl(tl(L))|| = ||L||-2
  i:. i<||swap(L;0;1)||  swap(L;0;1)[i] = [L[1]; L[0] / tl(tl(L))][i]
By: Auto THEN Inst Thm: swapped select [A;L;swap(L;0;1);0;1] THEN CaseNat 0 `i'
THEN
Reduce 0

Generated subgoal:

1 6. i : 
7. i<||swap(L;0;1)||
8. swap(L;0;1)[0] = L[1]
9. swap(L;0;1)[1] = L[0]
10. ||swap(L;0;1)|| = ||L||  
11. L = swap(swap(L;0;1);0;1)
12. x:||swap(L;0;1)||. x = 0  x = 1  swap(L;0;1)[x] = L[x]
13. i = 0
  swap(L;0;1)[i] = [L[1]; L[0] / tl(tl(L))][i]
6 steps

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

(27steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc