(15steps 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
cons
1
1.
T
: Type
2.
L
:
T
List
3.
x
:
T
4.
i
: {1..(||
L
||+1)
}
5.
j
: {1..(||
L
||+1)
}
||swap([
x
/
L
];
i
;
j
)|| = ||swap(
L
;
i
-1;
j
-1)||+1
By:
RWO
Thm*
L
:
T
List,
i
,
j
:
||
L
||. ||swap(
L
;
i
;
j
)|| = ||
L
||
0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(15steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
}
||swap([x / L];i;j)|| = ||swap(L;i-1;j-1)||+1 
L:T List, i,j:
||L||. ||swap(L;i;j)|| = ||L|| 
