DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
9
Thm*
(
AH
~
8)
((
AH
{1...8}) ~
64)
[chessboard_example]
cites the following:
5
Thm*
a
,
b
:
. {
a
...
b
} ~
(1+
b
-
a
)
[nsub_intiseg_rw]
8
Thm*
a
,
b
:
. (
a
b
) ~
(
a
b
)
[nsub_mul_rw]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
8) 
((AH
{1...8}) ~ 64)
a,b:
. {a...b} ~ (1+b-a)a,b:. (ab) ~ (a
b)8) ((AH{1...8}) ~ 64)a,b:. {a...b} ~ (1+b-a)a,b:. (ab) ~ (ab)