WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites div
nrel?
div_nrel
Def Div(
a
;
n
;
q
) ==
n
q
a
<
n
(
q
+1)
Thm*
a
:
,
n
:
,
q
:
. Div(
a
;
n
;
q
)
Prop
lelt
Def
i
j
<
k
==
i
j
&
j
<
k
le
Def
A
B
==
B
<
A
Thm*
i
,
j
:
. (
i
j
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
Div(
a
;
n
;
q
)
has structure:
div_nrel(
a
;
n
;
q
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc