(17steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
least
characterized
2
1
2
1
1
1
1.
k
:
2. 0<
k
3.
p
:{
p
:(
(
k
-1)
)|
i
:
(
k
-1).
p
(
i
) }.
3.
(least
i
:
.
p
(
i
))
{
i
:
(
k
-1)|
p
(
i
) & (
j
:
i
.
p
(
j
)) }
4.
p
:
k
5.
i
:
k
6.
p
(
i
)
7.
p
(0)
0
i
-1
By:
i
0
k
Asserted
Generated subgoal:
1
i
0
k
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(17steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc