FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
k
:{2...},
g
:({2..
k
}
),
x
,
y
:{2..
k
}.
Thm*
x
y
<
k
split_factor2(
g
;
x
;
y
)
{2..
k
}
[split_factor2_wf]
cites the following:
3
Thm*
i
,
j
:{2...}.
i
<
i
j
&
j
<
i
j
[factors_smaller]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
FTA
Sections
DiscrMathExt
Doc