Origin Definitions Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Nuprl Section: int_1

Selected Objects
COMINT_DEFS_acom Integer related definitions
COMge_gt_wf_com These wf lemmas are used by EqCD during rewriting to ensure that subterms come out in right order.
deflelt i  j < k == ij & j<k
deflele i  j  k == ij & jk
defnat  == {i:| 0i }
defnat_plus  == {i:| 0<i }
THMnat_plus_properties i:. 0<i
defint_nzero  == {i:i  0 }
THMint_nzero_properties i:i  0
defint_upper {i...} == {j:ij }
THMint_upper_properties i:j:{i...}. ij
defint_lower {...i} == {j:ji }
THMint_lower_properties i:j:{...i}. ji
defint_seg {i..j} == {k:i  k < j }
THMint_seg_properties i,j:y:{i..j}. i  y < j
THMdecidable__equal_int_seg i,j:x,y:{i..j}. Dec(x = y)
defint_iseg {i...j} == {k:ik & kj }
THMint_iseg_properties i,j:y:{i...j}. iy & yj
THMint_lt_to_int_upper i:A:({i+1...}Prop). (j:i<j  A(j))  (j:{i+1...}. A(j))
THMint_le_to_int_upper i:A:({i...}Prop). (j:ij  A(j))  (j:{i...}. A(j))
COMINT_INCLUSIONS_tcom Inclusion relations between integer subypes
COMINDUCTION_tcom Induction over naturals ...
THMnat_ind_a P:(Prop). P(0)  (i:P(i-1)  P(i))  (i:P(i))
THMnat_ind_tp P:(Prop). P(0)  (i:P(i-1)  P(i))  (i:P(i))
THMnat_ind P:(Prop). P(0)  (i:P(i-1)  P(i))  (j:P(j))
THMcomp_nat_ind_tp P:(Prop). (i:. (j:j<i  P(j))  P(i))  (i:P(i))
THMcomp_nat_ind_a P:(Prop). (i:. (j:j<i  P(j))  P(i))  (i:P(i))
THMnat_well_founded WellFnd{i}(;x,y.x<y)
THMcomplete_nat_ind P:(Prop). (i:. (j:iP(j))  P(i))  (i:P(i))
defsuptype S  T == T  S
THMcomplete_nat_ind_with_y P:(Prop). (i:. (j:iP(j))  P(i))  (i:P(i))
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections StandardLIB Doc