Def {...i} == {j:| ji }

is mentioned by

Thm* i:, E:({...i}Prop). Thm* E(i)  (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k))	[int_lower_ind]
Thm* n:. WellFnd{i}({...n};x,y.x>y)	[int_lower_well_founded]
Thm* a:, n:{...-1}. (a rem n) = (a rem -n)	[rem_4_to_1]
Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)	[rem_3_to_1]
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)	[rem_2_to_1]
Thm* a:, n:{...-1}. (a  n)  {...0}	[division_typing2b_sfa]
Thm* a:{...0}, n:. (a  n)  {...0}	[division_typing1b_sfa]
Thm* a:{...0}, n:{...-1}. (a  n)	[division_typing2a_sfa]
Thm* a:, b:{...-1}. (a  b) = -(a  (-b))	[div_4_to_1]
Thm* a:{...0}, b:{...-1}. (a  b) = ((-a)  (-b))	[div_3_to_1]
Thm* a:{...0}, b:. (a  b) = -((-a)  b)	[div_2_to_1]
Thm* a:, n:{...-1}. (a rem n)  (-n)	[rem_bounds_4_typing_sfa]
Thm* a:{...0}, n:{...-1}. -(a rem n)  (-n)	[rem_bounds_3_typing_sfa]
Thm* a:{...0}, n:. -(a rem n)  n	[rem_bounds_2_typing_sfa]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n)<-n	[rem_bounds_4]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n)>n	[rem_bounds_3]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n)>-n	[rem_bounds_2]
Thm* i:{...0}. |i| = -i	[absval_neg]

In prior sections: int 1

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