(7steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
delete
fenum
value
wf
1
1.
m
:
2.
k
:
3.
f
:
(
m
+1)
(
k
+1)
4. Inj(
(
m
+1);
(
k
+1);
f
)
(
i
.if
f
(
i
)=
k
f
(
m
) else
f
(
i
) fi)
m
k
By:
Analyze
Generated subgoal:
1
5.
i
:
m
if
f
(
i
)=
k
f
(
m
) else
f
(
i
) fi
k
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
(
i.if f(i)=
k
f(m) else f(i) fi) 
