(2steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eval
factorization
nullnorm
a
,
b
:
,
f
:({
a
..
b
}
).
b
a
{
a
..
b
}(
f
) =
{
a
..
a
}(
f
)
By:
Def of
{<int>..<int>
}(<exponents>)
Generated subgoal:
1
a
,
b
:
,
f
:({
a
..
b
}
).
b
a
(
i
:{
a
..
b
}.
i
f
(
i
)) = (
i
:{
a
..
a
}.
i
f
(
i
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
a,b:
, f:({a..b
}
). b
a 
{a..b}(f) = {a..a}(f) a,b:, f:({a..b}). ba {a..b}(f) = {a..a}(f){<int>..<int>}(<exponents>) a,b:, f:({a..b}). ba ( i:{a..b}. if(i)) = ( i:{a..a}. if(i))
