PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eval
factorization
nat
plus
a
:
,
b
:
,
f
:({
a
..
b
}
).
{
a
..
b
}(
f
)
By:
Def of
{<int>..<int>
}(<exponents>) ...
THEN
BackThru:
Thm*
x
,
y
:
.
x
y
...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
a:
, b:
, f:({a..b
}
). 
{a..b}(f) 
a:, b:, f:({a..b}). {a..b}(f) {<int>..<int>}(<exponents>) ...
x,y:. x
y ...
