(4steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eval
reduce
factorization
less
1
1
1
1.
a
:
2.
b
:
3.
f
: {
a
..
b
}
4.
j
: {
a
..
b
}
5. 2
j
6. 0<
f
(
j
)
{
a
..
b
}(reduce_factorization(
f
;
j
))
{1...}
By:
BackThru:
Thm*
a
:
,
b
:
,
f
:({
a
..
b
}
).
{
a
..
b
}(
f
)
...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
}
j
{a..b
{1...}
a:
