Nuprl - Proof: swap adjacent decomp 1 1 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap adjacent decomp 1 1 2 1 1 1 1

1. A : Type
2. L : A List
3. 1<||L||
4. ||tl(tl(L))|| = ||L||-2
5. i :

6. i<||L||
7.

i = 0
8.

i = 1

L[i] = tl(tl(L))[(i-1-1)]

By:	Repeat (RWO Thm* as:A List, n:(\|\|as\|\|-1). tl(as)[n] = as[(n+1)] 0)

Generated subgoal:

1 i-1-1 (||tl(L)||-1)
2 steps

About:

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