(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
1. A : Type
2. L : A List
3. 1<||L||
  swap(L;0;1) = [L[1]; L[0] / tl(tl(L))]
By: AssertBY (||tl(L)|| = ||L||-1)
(RWW Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1   0)
THEN
AssertBY (||tl(tl(L))|| = ||L||-2)
(RWW Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1   0)
THEN
BackThru
Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b

Generated subgoals:

1 4. ||tl(L)|| = ||L||-1  
5. ||tl(tl(L))|| = ||L||-2  
  ||swap(L;0;1)|| = ||[L[1]; L[0] / tl(tl(L))]||  
1 step
2 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]
7 steps

About:
listconsconsintnatural_numbersubtractless_thanuniverseequalimpliesall
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