WhoCites
Definitions
DiscrMathExt
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(eliminating the power of a composite of two number by adding it to the power of its two factors)
Who Cites split
factor2?
split_factor2
Def split_factor2(
g
;
x
;
y
)(
u
)
Def
== if
u
=
x
g
(
x
)+
g
(
x
y
) ;
u
=
y
g
(
y
)+
g
(
x
y
) ;
u
=
x
y
0 else
g
(
u
) fi
Thm*
k
:{2...},
g
:({2..
k
}
),
x
,
y
:{2..
k
}.
Thm*
x
y
<
k
split_factor2(
g
;
x
;
y
)
{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