Theory intto

Parents

Omega
toto

Contents

Type operators

(none)

Constants

intOrd : int -> int -> ordering
intto : int toto

Definitions

Theorems

BIT1_gt_neg_thm BIT1_nz BIT2_gt_neg_thm BIT2_nz ZERO_eq_neg_ZERO_thm apintto_thm gt_neg_BIT1_thm gt_neg_BIT2_thm neg_BIT1_lt_thm neg_BIT2_lt_thm neg_ZERO_eq_ZERO_thm neg_lt_BIT1_thm neg_lt_BIT2_thm neg_neg_thm pos_pos_thm

Definitions

|- intOrd = TO_of_LinearOrder $<

|- intto = TO intOrd

Theorems

BIT1_gt_neg_thm

|- !m n. intOrd (&BIT1 m) (-&n) = GREATER

|- !n. BIT1 n <> 0

BIT2_gt_neg_thm

|- !m n. intOrd (&BIT2 m) (-&n) = GREATER

|- !n. BIT2 n <> 0

ZERO_eq_neg_ZERO_thm

|- intOrd (&ZERO) (-&ZERO) = EQUAL

|- apto intto = intOrd

gt_neg_BIT1_thm

|- !m n. intOrd (&m) (-&BIT1 n) = GREATER

gt_neg_BIT2_thm

|- !m n. intOrd (&m) (-&BIT2 n) = GREATER

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

neg_lt_BIT1_thm

|- !m n. intOrd (-&m) (&BIT1 n) = LESS

neg_lt_BIT2_thm

|- !m n. intOrd (-&m) (&BIT2 n) = LESS

|- !m n. intOrd (-&m) (-&n) = numOrd n m

|- !m n. intOrd (&m) (&n) = numOrd m n