Nuprl - Proof: swap adjacent decomp 2 1

(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 2 1

1. A : Type
2. i :

3. 0<i
4.

L:A List.
4. i-1+1<||L||
4.

4. (

X,Y:A List.
4. (L = (X @ [L[(i-1)]; L[(i-1+1)]] @ Y)
4. (& swap(L;i-1;i-1+1) = (X @ [L[(i-1+1)]; L[(i-1)]] @ Y))
5. L : A List
6. i+1<||L||
7. ||tl(L)|| = ||L||-1
8.

X,Y:A List.
8. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y)
8. & swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y)

X,Y:A List.

[hd(L) / tl(L)] = (X @ [L[i]; L[(i+1)]] @ Y)

& swap([hd(L) / tl(L)];i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y)

By:	without_lemmas [`hd_wf_listp`] (ExRepD THEN InstConcl [[hd(L) / X];Y] THEN Reduce 0)

Generated subgoals:

1 8. X : A List
9. Y : A List
10. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y)
11. swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y)
[hd(L) / tl(L)] = [hd(L) / (X @ [L[i]; L[(i+1)] / Y])]
2 steps

2 8. X : A List
9. Y : A List
10. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y)
11. swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y)
swap([hd(L) / tl(L)];i;i+1) = [hd(L) / (X @ [L[(i+1)]; L[i] / Y])]
3 steps

About:

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

1	8. X : A List 9. Y : A List 10. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y) 11. swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y) [hd(L) / tl(L)] = [hd(L) / (X @ [L[i]; L[(i+1)] / Y])]	2 steps
2	8. X : A List 9. Y : A List 10. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y) 11. swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y) swap([hd(L) / tl(L)];i;i+1) = [hd(L) / (X @ [L[(i+1)]; L[i] / Y])]	3 steps