- apintto_thm
-
|- apto intto = intOrd
- pos_pos_thm
-
|- ∀m n. intOrd (&m) (&n) = numOrd m n
- neg_neg_thm
-
|- ∀m n. intOrd (-&m) (-&n) = numOrd n m
- BIT1_nz
-
|- ∀n. BIT1 n ≠ 0
- BIT2_nz
-
|- ∀n. BIT2 n ≠ 0
- neg_lt_BIT1_thm
-
|- ∀m n. intOrd (-&m) (&BIT1 n) = LESS
- neg_lt_BIT2_thm
-
|- ∀m n. intOrd (-&m) (&BIT2 n) = LESS
- neg_BIT1_lt_thm
-
|- ∀m n. intOrd (-&BIT1 m) (&n) = LESS
- neg_BIT2_lt_thm
-
|- ∀m n. intOrd (-&BIT2 m) (&n) = LESS
- neg_ZERO_eq_ZERO_thm
-
|- intOrd (-&ZERO) (&ZERO) = EQUAL
- BIT1_gt_neg_thm
-
|- ∀m n. intOrd (&BIT1 m) (-&n) = GREATER
- BIT2_gt_neg_thm
-
|- ∀m n. intOrd (&BIT2 m) (-&n) = GREATER
- gt_neg_BIT1_thm
-
|- ∀m n. intOrd (&m) (-&BIT1 n) = GREATER
- gt_neg_BIT2_thm
-
|- ∀m n. intOrd (&m) (-&BIT2 n) = GREATER
- ZERO_eq_neg_ZERO_thm
-
|- intOrd (&ZERO) (-&ZERO) = EQUAL