(4steps total)
PrintForm
Definitions
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
reduce
factorization
cancel
a
,
b
:
,
f
,
g
:({
a
..
b
}
),
j
:{
a
..
b
}.
0<
f
(
j
)
0<
g
(
j
)
reduce_factorization(
f
;
j
) = reduce_factorization(
g
;
j
)
f
=
g
By:
Auto
THEN FunExtensionality
Generated subgoal:
1
1.
a
:
2.
b
:
3.
f
: {
a
..
b
}
4.
g
: {
a
..
b
}
5.
j
: {
a
..
b
}
6. 0<
f
(
j
)
7. 0<
g
(
j
)
8. reduce_factorization(
f
;
j
) = reduce_factorization(
g
;
j
)
9.
x
: {
a
..
b
}
f
(
x
) =
g
(
x
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
FTA
Sections
DiscrMathExt
Doc