(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.
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)
i
:
(
k
-1).
p
(
i
+1)
By:
Witness:
i
-1
Generated subgoals:
1
0
i
-1
3
steps
2
p
(
i
-1+1)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(17steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc