Def  == {i:| 0i }

is mentioned by

Thm* a:, n:. (a mod n)	[modulus_wf]
Thm* a:, n:. ((a rem n) rem n) = (a rem n)	[rem_rem_to_rem]
Thm* i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)	[rem_addition]
Thm* a,b:, n:. ((a+bn) rem n) = (a rem n)	[rem_invariant]
Thm* a:, n:. an  (a rem n) = ((a-n) rem n)	[rem_rec_case]
Thm* a:, n:. a<n  (a rem n) = a	[rem_base_case]
Thm* a:, n:. an  (a  n) = ((a-n)  n)+1	[div_rec_case]
Thm* a:, n:. a<n  (a  n) = 0	[div_base_case]
Thm* a:, n:. Rem(a;n;a rem n)	[rem_fun_sat_rem_nrel]
Thm* a:, n:, k:. k(a  n)  kna	[div_lbound_1]
Thm* a:, n:, p,q:. Div(a;n;p)  Div(a;n;q)  p = q	[div_unique]
Thm* a:, n:. q:. Div(a;n;q) & (a  n) = q	[div_elim]
Thm* a:, n:. Div(a;n;a  n)	[div_fun_sat_div_nrel]
Thm* a:, n:. 0(a  n)	[div_bounds_1]
Thm* a:, n:{...-1}. (a rem n) = (a rem -n)	[rem_4_to_1]
Thm* a:, n:{...-1}. (a  n)  {...0}	[division_typing2b_sfa]
Thm* a:{...0}, n:{...-1}. (a  n)	[division_typing2a_sfa]
Thm* a:, n:. (a  n)	[division_typing1a_sfa]
Thm* a:, b:{...-1}. (a  b) = -(a  (-b))	[div_4_to_1]
Thm* a:, n:{...-1}. (a rem n)  (-n)	[rem_bounds_4_typing_sfa]
Thm* a:, n:. (a rem n)  n	[rem_bounds_1_typing_sfa]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n)<-n	[rem_bounds_4]
Thm* a:, n:. 0(a rem n) & (a rem n)<n	[rem_bounds_1]
Thm* a,b:. (a -- (a -- b)) = imin(a;b)	[ndiff_ndiff_eq_imin]
Thm* a,b:, c:. ((a -- b) -- c) = (a -- (b+c))	[ndiff_ndiff]
Thm* a:, b:. ((a+b) -- b) = a	[ndiff_inv]
Thm* a:. (0 -- a) = 0	[ndiff_ann_l]
Thm* a:. (a -- 0) = a	[ndiff_id_r]
Thm* P:(Prop). (x:. P(|x|))  (x:. P(x))	[absval_elim]
Thm* i:, n:. |i|>n  i<-n  i>n	[absval_lbound]
Thm* i:, n:. |i|n  -ni & in	[absval_ubound]
Thm* i:. |i| = i	[absval_pos]
Thm* x:. |x|	[absval_wf]
Thm* i,j:. ij	[multiply_nat_wf]
Thm* a,b:. 0ab	[mul_bounds_1a]
Thm* i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2	[multiply_functionality_wrt_le]
Thm* a,b:, n:. ab  nanb	[mul_preserves_le]
Def Rem(a;n;r) == q:. Div(a;n;q) & qn+r = a	[rem_nrel]

In prior sections: int 1 bool 1

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html