WhoCites
Definitions
DiscrMathExt
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites split
factor1?
split_factor1
Def split_factor1(
g
;
x
)(
u
)
Def
== if
u
=
x
g
(
x
)+
g
(
x
x
)+
g
(
x
x
) ;
u
=
x
x
0 else
g
(
u
) fi
Thm*
k
:{2...},
g
:({2..
k
}
),
x
:{2..
k
}.
Thm*
x
x
<
k
split_factor1(
g
;
x
)
{2..
k
}
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
DiscrMathExt
Sections
NuprlLIB
Doc