Selected Objects
| COM | INT_DEFS_acom |
Integer related definitions |
| COM | ge_gt_wf_com |
These wf lemmas are used by EqCD during rewriting to ensure that subterms come out in right order. |
| def | lelt |
i  j < k == ij & j<k |
| def | lele |
i j k == ij & jk |
| def | nat |
 == {i: | 0i } |
| def | nat_plus |
 == {i:| 0<i } |
| THM | nat_plus_properties |
 i:. 0<i |
| def | int_nzero |
  == {i:| i  0 } |
| THM | int_nzero_properties |
i:. i 0 |
| def | int_upper |
{i...} == {j:| ij } |
| THM | int_upper_properties |
i:, j:{i...}. ij |
| def | int_lower |
{...i} == {j:| ji } |
| THM | int_lower_properties |
i:, j:{...i}. ji |
| def | int_seg |
{i..j} == {k:| i k < j } |
| THM | int_seg_properties |
i,j:, y:{i..j}. i y < j |
| THM | decidable__equal_int_seg |
i,j:, x,y:{i..j}. Dec(x = y) |
| def | int_iseg |
{i...j} == {k:| ik & kj } |
| THM | int_iseg_properties |
i,j:, y:{i...j}. iy & yj |
| THM | int_lt_to_int_upper |
i:, A:({i+1...}  Prop). (j:. i<j   A(j))  (j:{i+1...}. A(j)) |
| THM | int_le_to_int_upper |
i:, A:({i...}Prop). (j:. ij A(j)) (j:{i...}. A(j)) |
| COM | INT_INCLUSIONS_tcom |
Inclusion relations between integer subypes |
| COM | INDUCTION_tcom |
Induction over naturals
... |
| THM | nat_ind_a |
P:(Prop). P(0) (i:. P(i-1) P(i)) (i:. P(i)) |
| THM | nat_ind_tp |
P:(Prop). P(0) (i:. P(i-1) P(i)) (i:. P(i)) |
| THM | nat_ind |
P:(Prop). P(0) (i:. P(i-1) P(i)) (j:. P(j)) |
| THM | comp_nat_ind_tp |
P:(Prop). (i:. (j:. j<i P(j)) P(i)) (i:. P(i)) |
| THM | comp_nat_ind_a |
P:(Prop). (i:. (j:. j<i P(j)) P(i)) (i:. P(i)) |
| THM | nat_well_founded |
WellFnd{i}(;x,y.x<y) |
| COM | OLD_INDUCTION |
|
| THM | complete_nat_ind |
P:(Prop). (i:. (j:i. P(j)) P(i)) (i:. P(i)) |
| def | suptype |
S  T == T  S |
| THM | complete_nat_ind_with_y |
P:(Prop). (i:. (j:i. P(j)) P(i)) (i:. P(i)) |