Boyer_Moore/testset/arith.ml

   1 let mytheory = ref [
   2 `m + 0 = m`;
   3 `m + (SUC n) = SUC(m + n)`;
   4 `m + n = n + m`;
   5 `m + (n + p) = (m + n) + p`;
   6 `(m + n) + p = m + (n + p)`;
   7 `(m + n = 0) <=> (m = 0) /\ (n = 0)`;
   8 `(m + n = m + p) <=> (n = p)`;
   9 `(m + p = n + p) <=> (m = n)`;
  10 `(m + n = m) <=> (n = 0)`;
  11 `(m + n = n) <=> (m = 0)`;
  12 `SUC m = m + SUC(0)`;
  13 `m * 0 = 0`;
  14 `m * (SUC n) = m + (m * n)`;
  15 `(0 * n = 0) /\ (m * 0 = 0) /\ (1 * n = n) /\ (m * 1 = m) /\ ((SUC m) * n = (m * n) + n) /\ (m * (SUC n) = m + (m * n))`;
  16 `m * n = n * m`;
  17 `m * (n + p) = (m * n) + (m * p)`;
  18 `(m + n) * p = (m * p) + (n * p)`;
  19 `m * (n * p) = (m * n) * p`;
  20 `(m * n = 0) <=> (m = 0) \/ (n = 0)`;
  21 `(m * n = m * p) <=> (m = 0) \/ (n = p)`;
  22 `(m * p = n * p) <=> (m = n) \/ (p = 0)`;
  23 `SUC(SUC(0)) * n = n + n`;
  24 `(m * n = SUC(0)) <=> (m = SUC(0)) /\ (n = SUC(0))`;
  25 `(m EXP n = 0) <=> (m = 0) /\ ~(n = 0)`;
  26 `m EXP (n + p) = (m EXP n) * (m EXP p)`;
  27 `SUC(0) EXP n = SUC(0)`;
  28 `n EXP SUC(0) = n`;
  29 `n EXP SUC(SUC(0)) = n * n`;
  30 `(m * n) EXP p = m EXP p * n EXP p`;
  31 `m EXP (n * p) = (m EXP n) EXP p`;
  32 `(SUC m <= n) <=> (m < n)`;
  33 `(m < SUC n) <=> (m <= n)`;
  34 `(SUC m <= SUC n) <=> (m <= n)`;
  35 `(SUC m < SUC n) <=> (m < n)`;
  36 `0 <= n`;
  37 `0 < SUC n`;
  38 `n <= n`;
  39 `~(n < n)`;
  40 `(m <= n /\ n <= m) <=> (m = n)`;
  41 `~(m < n /\ n < m)`;
  42 `~(m <= n /\ n < m)`;
  43 `~(m < n /\ n <= m)`;
  44 `m <= n /\ n <= p ==> m <= p`;
  45 `m < n /\ n < p ==> m < p`;
  46 `m <= n /\ n < p ==> m < p`;
  47 `m < n /\ n <= p ==> m < p`;
  48 `m <= n \/ n <= m`;
  49 `(m < n) \/ (n < m) \/ (m = n)`;
  50 `m <= n \/ n < m`;
  51 `m < n \/ n <= m`;
  52 `0 < n <=> ~(n = 0)`;
  53 `(m <= n) <=> (m < n) \/ (m = n)`;
  54 `(m < n) <=> (m <= n) /\ ~(m = n)`;
  55 `~(m <= n) <=> (n < m)`;
  56 `~(m < n) <=> n <= m`;
  57 `m < n ==> m <= n`;
  58 `(m = n) ==> m <= n`;
  59 `m <= m + n`;
  60 `n <= m + n`;
  61 `(m < m + n) <=> (0 < n)`;
  62 `(n < m + n) <=> (0 < m)`;
  63 `(m + n) <= (m + p) <=> n <= p`;
  64 `(m + p) <= (n + p) <=> (m <= n)`;
  65 `(m + n) < (m + p) <=> n < p`;
  66 `(m + p) < (n + p) <=> (m < n)`;
  67 `m <= p /\ n <= q ==> m + n <= p + q`;
  68 `m <= p /\ n < q ==> m + n < p + q`;
  69 `m < p /\ n <= q ==> m + n < p + q`;
  70 `m < p /\ n < q ==> m + n < p + q`;
  71 `(0 < m * n) <=> (0 < m) /\ (0 < n)`;
  72 `m <= n /\ p <= q ==> m * p <= n * q`;
  73 `~(m = 0) /\ n < p ==> m * n < m * p`;
  74 `(m * n) <= (m * p) <=> (m = 0) \/ n <= p`;
  75 `(m * p) <= (n * p) <=> (m <= n) \/ (p = 0)`;
  76 `(m * n) < (m * p) <=> ~(m = 0) /\ n < p`;
  77 `(m * p) < (n * p) <=> (m < n) /\ ~(p = 0)`;
  78 `(SUC m = SUC n) <=> (m = n)`;
  79 `m < n /\ p < q ==> m * p < n * q`;
  80 `n <= n * n`;
  81 `(P m n <=> P n m) /\ (m <= n ==> P m n) ==> P m n`;
  82 `(P m m) /\ (P m n <=> P n m) /\ (m < n ==> P m n) ==> P m y`;
  83 `((m < n ==> P m) ==> P n) ==> P n`;
  84 `~(EVEN n) <=> ODD n`;
  85 `~(ODD n) <=> EVEN n`;
  86 `EVEN n \/ ODD n`;
  87 `~(EVEN n /\ ODD n)`;
  88 `EVEN(m + n) <=> (EVEN m <=> EVEN n)`;
  89 `EVEN(m * n) <=> EVEN(m) \/ EVEN(n)`;
  90 `EVEN(m EXP n) <=> EVEN(m) /\ ~(n = 0)`;
  91 `ODD(m + n) <=> ~(ODD m <=> ODD n)`;
  92 `ODD(m * n) <=> ODD(m) /\ ODD(n)`;
  93 `ODD(m EXP n) <=> ODD(m) \/ (n = 0)`;
  94 `EVEN(SUC(SUC(0)) * n)`;
  95 `ODD(SUC(SUC(SUC(0)) * n))`;
  96 `(0 - m = 0) /\ (m - 0 = m)`;
  97 `PRE(SUC m - n) = m - n`;
  98 `SUC m - SUC n = m - n`;
  99 `n - n = 0`;
 100 `(m + n) - n = m`;
 101 `(m + n) - m = n`;
 102 `(m - n = 0) <=> m <= n`;
 103 `m - (m + n) = 0`;
 104 `n - (m + n) = 0`;
 105 `n <= m ==> ((m - n) + n = m)`;
 106 `(m + n) - (m + p) = n - p`;
 107 `(m + p) - (n + p) = m - n`;
 108 `m * (n - p) = m * n - m * p`;
 109 `(m - n) * p = m * p - n * p`;
 110 `!n. SUC n - SUC(0) = n`;
 111 `EVEN(m - n) <=> m <= n \/ (EVEN(m) <=> EVEN(n))`;
 112 `ODD(m - n) <=> n < m /\ ~(ODD m <=> ODD n)`;
 113 `0 < FACT n`;
 114 `1 <= FACT n`;
 115 `m <= n ==> FACT m <= FACT n`;
 116 `0 < x EXP n <=> ~(x = 0) \/ (n = 0)`;
 117 `x EXP m < x EXP n <=> SUC(SUC(0)) <= x /\ m < n \/ (x = 0) /\ ~(m = 0) /\ (n = 0)`;
 118 `x EXP m <= x EXP n <=> if x = 0 then (m = 0) ==> (n = 0) else (x = 1) \/ m <= n`;
 119 `~(p = 0) /\ m <= n ==> m DIV p <= n DIV p`;
 120 `P(PRE n) <=> n = SUC m \/ m = 0 /\ n = 0 ==> P m`
 121 ]