Nuprl - Proof: swapped select 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swapped select 1

1. T : Type
2. L1 : T List
3. L2 : T List
4. i :

||L1||
5. j :

||L1||
6. L2 = swap(L1;i;j)

L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||

& L1 = swap(L2;i;j)

& (

||L2||.

x = i

x = j

L2[x] = L1[x])

By:

AssertBY (||L2|| = ||L1||)
(HypSubst -1 0
(THEN
(BackThru Thm*

L:T List, i,j:

||L||. ||swap(L;i;j)|| = ||L||

)
THEN
AssertBY (L2 = swap(L1;i;j)) Analyze
THEN
Unfold `guard` 0
THEN
HypSubst 8 0
THEN
Try (Analyze -1 THEN Complete Auto)
THEN
Try
(RWO Thm*

L:T List, i,j,x:

||L||. swap(L;i;j)[x] = L[((i, j)(x))] 0
(THEN
(Unfold `flip` 0
(THEN
(Reduce 0
(THEN
(Repeat SplitOnConclITE
(THEN
(HypSubstSq -1 0)

Generated subgoal:

1 7. ||L2|| = ||L1||
8. L2 = swap(L1;i;j)  {L:(T List)| ||L|| = ||L1||   }
  L1 = swap(swap(L1;i;j);i;j)
1 step

About:

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