int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def P  Q == PQ

is mentioned by

Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))[decidable__all_int_seg]
Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))[decidable__ex_int_seg]
Thm* i,j:.
Thm* i<j
Thm* 
Thm* (F:({i..j}Prop). (k:{i..j}. F(k))  F(i) & (k:{(i+1)..j}. F(k)))		[split_int_seg_all_dom_sfa]
Thm* i,j:.
Thm* i<j
Thm* 
Thm* (F:({i..j}Prop). (k:{i..j}. F(k))  F(i)  (k:{(i+1)..j}. F(k)))		[split_int_seg_exist_dom_sfa]
Thm* i:, j:{i+1...}, E:({i..j}Prop).
Thm* E(i)  (k:{(i+1)..j}. E(k-1)  E(k))  (k:{i..j}. E(k))		[int_seg_ind]
Thm* i:, E:({...i}Prop).
Thm* E(i)  (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k))		[int_lower_ind]
Thm* i:, E:({i...}Prop).
Thm* E(i)  (k:{i+1...}. E(k-1)  E(k))  (k:{i...}. E(k))		[int_upper_ind]
Thm* a:, b:. |a| = |b|  (a rem b) = 0[rem_eq_args_z]
Thm* a:, b:. |a|<|b|  (a rem b) = a[rem_base_case_z]
Thm* a:, n:. an  (a rem n) = ((a-n) rem n)[rem_rec_case]
Thm* a:, n:. |a|<|n|  (a rem n) = a[rem_gen_base_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:, p,q:. Div(a;n;p)  Div(a;n;q)  p = q[div_unique]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1q2k-r2  q1q2[division_mono2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2  q1q2[division_mono1_sfa]
Thm* k:, r1,r2:k, q1,q2:.
Thm* q1k+r1 = q2k-r2  q1 = q2 & r1 = 0 & r2 = 0  q2 = q1+1 & r2 = k-r1		[division4_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = -(q2k+r2)  q1 = -q2 & r1 = r2[division3_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = q2k-r2  q1 = q2 & r1 = r2[division2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2[division1_sfa]
Thm* a,b:. a  0  b  0  ab  0[int_entire_a]
Thm* a,b:. ab = 0  a = 0  b = 0[int_entire]
Thm* i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2[multiply_functionality_wrt_le]
Thm* a,b:, n:. na<nb  a<b[mul_cancel_in_lt]
Thm* a,b:, n:. na = nb  a = b[mul_cancel_in_eq]
Thm* a,b:, n:. nanb  ab[mul_cancel_in_le]
Thm* a,b:, n:. a<b  na<nb[mul_preserves_lt]
Thm* a,b:, n:. ab  nanb[mul_preserves_le]
Thm* a,b:. ab = 0  a = 0 & b = 0[zero_ann_b]
Thm* a,b:. a = 0  b = 0  ab = 0[zero_ann_a]

In prior sections: core well fnd int 1 bool 1

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

int 2 Sections StandardLIB Doc