Use lower case in the names for the HOL4 backend

5 files changed, 771 insertions, 832 deletions

diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index fa2f144d..79d94698 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -6,142 +6,169 @@ val _ = new_theory "primitivesArith"
 
 (* TODO: we need a better library of lemmas about arithmetic *)
 
+(* We generate and save an induction theorem for positive integers *)
+Theorem int_induction:
+  !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i
+Proof
+  ntac 4 strip_tac >>
+  Induct_on ‘Num i’ >> rpt strip_tac
+  >-(sg ‘i = 0’ >- cooper_tac >> fs []) >>
+  last_assum (qspec_assume ‘i-1’) >>
+  fs [] >> pop_assum irule >>
+  rw [] >> try_tac cooper_tac >>
+  first_assum (qspec_assume ‘i - 1’) >>
+  pop_assum irule >>
+  rw [] >> try_tac cooper_tac
+QED
+
+val _ = TypeBase.update_induction int_induction
+
 (* TODO: add those as rewriting theorems by default *)
-val NOT_LE_EQ_GT = store_thm("NOT_LE_EQ_GT", “!(x y: int). ~(x <= y) <=> x > y”, COOPER_TAC)
-val NOT_LT_EQ_GE = store_thm("NOT_LT_EQ_GE", “!(x y: int). ~(x < y) <=> x >= y”, COOPER_TAC)
-val NOT_GE_EQ_LT = store_thm("NOT_GE_EQ_LT", “!(x y: int). ~(x >= y) <=> x < y”, COOPER_TAC)
-val NOT_GT_EQ_LE = store_thm("NOT_GT_EQ_LE", “!(x y: int). ~(x > y) <=> x <= y”, COOPER_TAC)
+val not_le_eq_gt = store_thm("not_le_eq_gt", “!(x y: int). ~(x <= y) <=> x > y”, cooper_tac)
+val not_lt_eq_ge = store_thm("not_lt_eq_ge", “!(x y: int). ~(x < y) <=> x >= y”, cooper_tac)
+val not_ge_eq_lt = store_thm("not_ge_eq_lt", “!(x y: int). ~(x >= y) <=> x < y”, cooper_tac)
+val not_gt_eq_le = store_thm("not_gt_eq_le", “!(x y: int). ~(x > y) <=> x <= y”, cooper_tac)
+
+val ge_eq_le = store_thm("ge_eq_le", “!(x y : int). x >= y <=> y <= x”, cooper_tac)
+val le_eq_ge = store_thm("le_eq_ge", “!(x y : int). x <= y <=> y >= x”, cooper_tac)
+val gt_eq_lt = store_thm("gt_eq_lt", “!(x y : int). x > y <=> y < x”, cooper_tac)
+val lt_eq_gt = store_thm("lt_eq_gt", “!(x y : int). x < y <=> y > x”, cooper_tac)
 
-val GE_EQ_LE = store_thm("GE_EQ_LE", “!(x y : int). x >= y <=> y <= x”, COOPER_TAC)
-val LE_EQ_GE = store_thm("LE_EQ_GE", “!(x y : int). x <= y <=> y >= x”, COOPER_TAC)
-val GT_EQ_LT = store_thm("GT_EQ_LT", “!(x y : int). x > y <=> y < x”, COOPER_TAC)
-val LT_EQ_GT = store_thm("LT_EQ_GT", “!(x y : int). x < y <=> y > x”, COOPER_TAC)
+Theorem int_of_num:
+  ∀i. 0 ≤ i ⇒ &Num i = i
+Proof
+  fs [INT_OF_NUM]
+QED
+
+Theorem int_add:
+  ∀m n. &(m + n) = &m + &n
+Proof
+  fs [INT_ADD]
+QED
 
-Theorem INT_OF_NUM_INJ:
+Theorem int_of_num_inj:
   !n m. &n = &m ==> n = m
 Proof
   rpt strip_tac >>
   fs [Num]
 QED
 
-Theorem NUM_SUB_EQ:
+Theorem num_sub_eq:
   !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x
 Proof
   rpt strip_tac >>
-  sg ‘0 <= y’ >- COOPER_TAC >>
+  sg ‘0 <= y’ >- cooper_tac >>
   rfs [] >>
   (* Convert to integers *)
-  irule INT_OF_NUM_INJ >>
-  imp_res_tac (GSYM INT_OF_NUM) >>
+  irule int_of_num_inj >>
+  imp_res_tac int_of_num >>
   (* Associativity of & *)
-  PURE_REWRITE_TAC [GSYM INT_ADD] >>
+  pure_rewrite_tac [int_add] >>
   fs []
 QED
 
-Theorem NUM_SUB_1_EQ:
+Theorem num_sub_1_eq:
   !(x y : int). x = y - 1 ==> 0 <= x ==> Num y = SUC (Num x)
 Proof
   rpt strip_tac >>
   (* Get rid of the SUC *)
   sg ‘SUC (Num x) = 1 + Num x’ >-(rw [ADD]) >> rw [] >>
   (* Massage a bit the goal *)
-  qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- COOPER_TAC >>
+  qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- cooper_tac >>
   (* Apply the general theorem *)
-  irule NUM_SUB_EQ >>
-  COOPER_TAC
+  irule num_sub_eq >>
+  cooper_tac
 QED
 
-Theorem POS_MUL_POS_IS_POS:
+Theorem pos_mul_pos_is_pos:
   !(x y : int). 0 <= x ==> 0 <= y ==> 0 <= x * y
 Proof
   rpt strip_tac >>
-  sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> COOPER_TAC) >>
-  sg ‘&(Num x) = x’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
-  sg ‘&(Num y) = y’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >>
-  metis_tac[]
+  sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> cooper_tac) >>
+  sg_dep_rewrite_all_tac int_of_num >> try_tac cooper_tac >> fs []
 QED
 
-Theorem POS_DIV_POS_IS_POS:
+Theorem pos_div_pos_is_pos:
   !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x / y
 Proof
   rpt strip_tac >>
-  rw [LE_EQ_GE] >>  
-  sg ‘y <> 0’ >- COOPER_TAC >>
+  rw [le_eq_ge] >>
+  sg ‘y <> 0’ >- cooper_tac >>
   qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >>
-  fs [] >> pop_ignore_tac >> rw [] >- COOPER_TAC >>
-  fs [NOT_LT_EQ_GE] >>
+  fs [] >> pop_ignore_tac >> rw [] >- cooper_tac >>
+  fs [not_lt_eq_ge] >>
   (* Proof by contradiction: assume k < 0 *)
-  spose_not_then ASSUME_TAC >>
-  fs [NOT_GE_EQ_LT] >>
-  sg ‘k * y = (k + 1) * y + - y’ >- (fs [INT_RDISTRIB] >> COOPER_TAC) >>
-  sg ‘0 <= (-(k + 1)) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
-  COOPER_TAC
+  spose_not_then assume_tac >>
+  fs [not_ge_eq_lt] >>
+  sg ‘k * y = (k + 1) * y + - y’ >- (fs [INT_RDISTRIB] >> cooper_tac) >>
+  sg ‘0 <= (-(k + 1)) * y’ >- (irule pos_mul_pos_is_pos >> cooper_tac) >>
+  cooper_tac
 QED
 
-Theorem POS_DIV_POS_LE:
+Theorem pos_div_pos_le:
   !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x <= y ==> x / d <= y / d
 Proof
   rpt strip_tac >>
-  sg ‘d <> 0’ >- COOPER_TAC >>
-  qspecl_then [‘\k. k = x / d’, ‘x’, ‘d’] ASSUME_TAC INT_DIV_P >>
-  qspecl_then [‘\k. k = y / d’, ‘y’, ‘d’] ASSUME_TAC INT_DIV_P >>
-  rfs [NOT_LT_EQ_GE] >> TRY COOPER_TAC >>
-  sg ‘y = (x / d) * d + (r' + y - x)’ >- COOPER_TAC >>
-  qspecl_then [‘(x / d) * d’, ‘r' + y - x’, ‘d’] ASSUME_TAC INT_ADD_DIV >>
+  sg ‘d <> 0’ >- cooper_tac >>
+  qspecl_assume [‘\k. k = x / d’, ‘x’, ‘d’] INT_DIV_P >>
+  qspecl_assume [‘\k. k = y / d’, ‘y’, ‘d’] INT_DIV_P >>
+  rfs [not_lt_eq_ge] >> try_tac cooper_tac >>
+  sg ‘y = (x / d) * d + (r' + y - x)’ >- cooper_tac >>
+  qspecl_assume [‘(x / d) * d’, ‘r' + y - x’, ‘d’] INT_ADD_DIV >>
   rfs [] >>
   Cases_on ‘x = y’ >- fs [] >>
-  sg ‘r' + y ≠ x’ >- COOPER_TAC >> fs [] >>
-  sg ‘((x / d) * d) / d = x / d’ >- (irule INT_DIV_RMUL >> COOPER_TAC) >>
+  sg ‘r' + y ≠ x’ >- cooper_tac >> fs [] >>
+  sg ‘((x / d) * d) / d = x / d’ >- (irule INT_DIV_RMUL >> cooper_tac) >>
   fs [] >>
-  sg ‘0 <= (r' + y − x) / d’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
+  sg ‘0 <= (r' + y − x) / d’ >- (irule pos_div_pos_is_pos >> cooper_tac) >>
   metis_tac [INT_LE_ADDR]
 QED
 
-Theorem POS_DIV_POS_LE_INIT:
+Theorem pos_div_pos_le_init:
   !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x
 Proof
   rpt strip_tac >>
-  sg ‘y <> 0’ >- COOPER_TAC >>
-  qspecl_then [‘\k. k = x / y’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_P >>
-  rfs [NOT_LT_EQ_GE] >- COOPER_TAC >>
+  sg ‘y <> 0’ >- cooper_tac >>
+  qspecl_assume [‘\k. k = x / y’, ‘x’, ‘y’] INT_DIV_P >>
+  rfs [not_lt_eq_ge] >- cooper_tac >>
   sg ‘y = (y - 1) + 1’ >- rw [] >>
   sg ‘x = x / y + ((x / y) * (y - 1) + r)’ >-(
-    qspecl_then [‘1’, ‘y-1’, ‘x / y’] ASSUME_TAC INT_LDISTRIB >>
+    qspecl_assume [‘1’, ‘y-1’, ‘x / y’] INT_LDISTRIB >>
     rfs [] >>
-    COOPER_TAC
+    cooper_tac
   ) >>
-  sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- (COOPER_TAC) >>
+  sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- cooper_tac >>
   pop_assum irule >>
   exists_tac “x / y * (y − 1) + r” >>
-  sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
-  sg ‘0 <= (x / y) * (y - 1)’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
-  COOPER_TAC
+  sg ‘0 <= x / y’ >- (irule pos_div_pos_is_pos >> cooper_tac) >>
+  sg ‘0 <= (x / y) * (y - 1)’ >- (irule pos_mul_pos_is_pos >> cooper_tac) >>
+  cooper_tac
 QED
 
-Theorem POS_MOD_POS_IS_POS:
+Theorem pos_mod_pos_is_pos:
   !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x % y
 Proof
   rpt strip_tac >>
-  sg ‘y <> 0’ >- COOPER_TAC >>
+  sg ‘y <> 0’ >- cooper_tac >>
   imp_res_tac INT_DIVISION >>
   first_x_assum (qspec_then ‘x’ assume_tac) >>
   first_x_assum (qspec_then ‘x’ assume_tac) >>
-  sg ‘~(y < 0)’ >- COOPER_TAC >> fs []
+  sg ‘~(y < 0)’ >- cooper_tac >> fs []
 QED
 
-Theorem POS_MOD_POS_LE_INIT:
+Theorem pos_mod_pos_le_init:
   !(x y : int). 0 <= x ==> 0 < y ==> x % y <= x
 Proof
   rpt strip_tac >>
-  sg ‘y <> 0’ >- COOPER_TAC >>
+  sg ‘y <> 0’ >- cooper_tac >>
   imp_res_tac INT_DIVISION >>
   first_x_assum (qspec_then ‘x’ assume_tac) >>
   first_x_assum (qspec_then ‘x’ assume_tac) >>
-  sg ‘~(y < 0)’ >- COOPER_TAC >> fs [] >>
-  sg ‘0 <= x % y’ >- (irule POS_MOD_POS_IS_POS >> COOPER_TAC) >>
-  sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >>
-  sg ‘0 <= (x / y) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >>
-  COOPER_TAC
+  sg ‘~(y < 0)’ >- cooper_tac >> fs [] >>
+  sg ‘0 <= x % y’ >- (irule pos_mod_pos_is_pos >> cooper_tac) >>
+  sg ‘0 <= x / y’ >- (irule pos_div_pos_is_pos >> cooper_tac) >>
+  sg ‘0 <= (x / y) * y’ >- (irule pos_mul_pos_is_pos >> cooper_tac) >>
+  cooper_tac
 QED
 
 val _ = export_theory ()
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 3b157b87..73a6cf20 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -3,23 +3,26 @@ sig
   type thm = Thm.thm
   
   (*  Theorems  *)
-    val GE_EQ_LE : thm
-    val GT_EQ_LT : thm
-    val INT_OF_NUM_INJ : thm
-    val LE_EQ_GE : thm
-    val LT_EQ_GT : thm
-    val NOT_GE_EQ_LT : thm
-    val NOT_GT_EQ_LE : thm
-    val NOT_LE_EQ_GT : thm
-    val NOT_LT_EQ_GE : thm
-    val NUM_SUB_1_EQ : thm
-    val NUM_SUB_EQ : thm
-    val POS_DIV_POS_IS_POS : thm
-    val POS_DIV_POS_LE : thm
-    val POS_DIV_POS_LE_INIT : thm
-    val POS_MOD_POS_IS_POS : thm
-    val POS_MOD_POS_LE_INIT : thm
-    val POS_MUL_POS_IS_POS : thm
+    val ge_eq_le : thm
+    val gt_eq_lt : thm
+    val int_add : thm
+    val int_induction : thm
+    val int_of_num : thm
+    val int_of_num_inj : thm
+    val le_eq_ge : thm
+    val lt_eq_gt : thm
+    val not_ge_eq_lt : thm
+    val not_gt_eq_le : thm
+    val not_le_eq_gt : thm
+    val not_lt_eq_ge : thm
+    val num_sub_1_eq : thm
+    val num_sub_eq : thm
+    val pos_div_pos_is_pos : thm
+    val pos_div_pos_le : thm
+    val pos_div_pos_le_init : thm
+    val pos_mod_pos_is_pos : thm
+    val pos_mod_pos_le_init : thm
+    val pos_mul_pos_is_pos : thm
   
   val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -27,71 +30,83 @@ sig
    
    [int_arith] Parent theory of "primitivesArith"
    
-   [GE_EQ_LE]  Theorem
+   [ge_eq_le]  Theorem
       
       ⊢ ∀x y. x ≥ y ⇔ y ≤ x
    
-   [GT_EQ_LT]  Theorem
+   [gt_eq_lt]  Theorem
       
       ⊢ ∀x y. x > y ⇔ y < x
    
-   [INT_OF_NUM_INJ]  Theorem
+   [int_add]  Theorem
+      
+      ⊢ ∀m n. &(m + n) = &m + &n
+   
+   [int_induction]  Theorem
+      
+      ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i
+   
+   [int_of_num]  Theorem
+      
+      ⊢ ∀i. 0 ≤ i ⇒ &Num i = i
+   
+   [int_of_num_inj]  Theorem
       
       ⊢ ∀n m. &n = &m ⇒ n = m
    
-   [LE_EQ_GE]  Theorem
+   [le_eq_ge]  Theorem
       
       ⊢ ∀x y. x ≤ y ⇔ y ≥ x
    
-   [LT_EQ_GT]  Theorem
+   [lt_eq_gt]  Theorem
       
       ⊢ ∀x y. x < y ⇔ y > x
    
-   [NOT_GE_EQ_LT]  Theorem
+   [not_ge_eq_lt]  Theorem
       
       ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
    
-   [NOT_GT_EQ_LE]  Theorem
+   [not_gt_eq_le]  Theorem
       
       ⊢ ∀x y. ¬(x > y) ⇔ x ≤ y
    
-   [NOT_LE_EQ_GT]  Theorem
+   [not_le_eq_gt]  Theorem
       
       ⊢ ∀x y. ¬(x ≤ y) ⇔ x > y
    
-   [NOT_LT_EQ_GE]  Theorem
+   [not_lt_eq_ge]  Theorem
       
       ⊢ ∀x y. ¬(x < y) ⇔ x ≥ y
    
-   [NUM_SUB_1_EQ]  Theorem
+   [num_sub_1_eq]  Theorem
       
       ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
    
-   [NUM_SUB_EQ]  Theorem
+   [num_sub_eq]  Theorem
       
       ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
    
-   [POS_DIV_POS_IS_POS]  Theorem
+   [pos_div_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
    
-   [POS_DIV_POS_LE]  Theorem
+   [pos_div_pos_le]  Theorem
       
       ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≤ y ⇒ x / d ≤ y / d
    
-   [POS_DIV_POS_LE_INIT]  Theorem
+   [pos_div_pos_le_init]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
    
-   [POS_MOD_POS_IS_POS]  Theorem
+   [pos_mod_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y
    
-   [POS_MOD_POS_LE_INIT]  Theorem
+   [pos_mod_pos_le_init]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x
    
-   [POS_MUL_POS_IS_POS]  Theorem
+   [pos_mul_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
    
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 0368ee9a..75df3015 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -5,6 +5,9 @@ struct
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory
 
+(* Remark: below, we also have conversions *)
+val gsym = GSYM
+
 (* Ignore a theorem.
 
    To be used in conjunction with {!pop_assum} for instance.
@@ -13,12 +16,15 @@ fun ignore_tac (_ : thm) : tactic = ALL_TAC
 
 val pop_ignore_tac = pop_assum ignore_tac
 
-val try_tac = TRY
-
 (* TODO: no exfalso tactic?? *)
-val ex_falso : tactic =
+val exfalso : tactic =
   SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
 
+val try_tac = TRY
+val first_tac = FIRST
+val map_first = MAP_FIRST
+val fail_tac = FAIL_TAC
+
 fun qspec_assume x th = qspec_then x assume_tac th
 fun qspecl_assume xl th = qspecl_then xl assume_tac th
 fun first_qspec_assume x = first_assum (qspec_assume x)
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 2df3375a..9da8505d 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -534,34 +534,35 @@ fun prove_arith_op_eq (asms, g) =
       | _ => failwith "Unexpected"
     val x = (snd o dest_comb) x_to_int;
     val y = (snd o dest_comb) y_to_int;
+    val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas];
     fun inst_first_lem arg lems =
-      MAP_FIRST (fn th => (ASSUME_TAC (SPEC arg th) handle HOL_ERR _ => FAIL_TAC "")) lems;
+      map_first (fn th => (assume_tac (SPEC arg th) handle HOL_ERR _ => fail_tac "")) lems;
   in
     (rpt gen_tac >>
-     rpt DISCH_TAC >>
-     ASSUME_TAC usize_bounds >> (* Only useful for usize of course *)
-     ASSUME_TAC isize_bounds >> (* Only useful for isize of course *)
-     rw (int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas]) >>
-     fs (int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas]) >>
+     rpt disch_tac >>
+     assume_tac usize_bounds >> (* Only useful for usize of course *)
+     assume_tac isize_bounds >> (* Only useful for isize of course *)
+     rw rw_thms >>
+     fs rw_thms >>
      inst_first_lem x all_to_int_bounds_lemmas >>
      inst_first_lem y all_to_int_bounds_lemmas >>
-     gs [NOT_LE_EQ_GT, NOT_LT_EQ_GE, NOT_GE_EQ_LT, NOT_GT_EQ_LE, GE_EQ_LE, GT_EQ_LT] >>
-     TRY COOPER_TAC >>
-     FIRST [
+     gs [not_le_eq_gt, not_lt_eq_ge, not_ge_eq_lt, not_gt_eq_le, ge_eq_le, gt_eq_lt] >>
+     try_tac cooper_tac >>
+     first_tac [
        (* For division *)
-       qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_DIV_POS_IS_POS >>
-       qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_DIV_POS_LE_INIT >>
-       COOPER_TAC,
+       qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_div_pos_is_pos >>
+       qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_div_pos_le_init >>
+       cooper_tac,
        (* For remainder *)
        dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >>
-       qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_MOD_POS_IS_POS >>
-       qspecl_then [‘^x_to_int’, ‘^y_to_int’] ASSUME_TAC POS_MOD_POS_LE_INIT >>
-       COOPER_TAC,
+       qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_is_pos >>
+       qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_le_init >>
+       cooper_tac,
        dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs []
      ]) (asms, g)
   end
 
-Theorem U8_ADD_EQ:
+Theorem u8_add_eq:
   !x y.
     u8_to_int x + u8_to_int y <= u8_max ==>
     ?z. u8_add x y = Return z /\ u8_to_int z = u8_to_int x + u8_to_int y
@@ -569,7 +570,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U16_ADD_EQ:
+Theorem u16_add_eq:
   !(x y).
     u16_to_int x + u16_to_int y <= u16_max ==>
     ?(z). u16_add x y = Return z /\ u16_to_int z = u16_to_int x + u16_to_int y
@@ -577,7 +578,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U32_ADD_EQ:
+Theorem u32_add_eq:
   !x y.
     u32_to_int x + u32_to_int y <= u32_max ==>
     ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y
@@ -585,7 +586,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U64_ADD_EQ:
+Theorem u64_add_eq:
   !x y.
     u64_to_int x + u64_to_int y <= u64_max ==>
     ?z. u64_add x y = Return z /\ u64_to_int z = u64_to_int x + u64_to_int y
@@ -593,7 +594,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U128_ADD_EQ:
+Theorem u128_add_eq:
   !x y.
     u128_to_int x + u128_to_int y <= u128_max ==>
     ?z. u128_add x y = Return z /\ u128_to_int z = u128_to_int x + u128_to_int y
@@ -601,7 +602,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem USIZE_ADD_EQ:
+Theorem usize_add_eq:
   !x y.
     (usize_to_int x + usize_to_int y <= u16_max) \/ (usize_to_int x + usize_to_int y <= usize_max) ==>
     ?z. usize_add x y = Return z /\ usize_to_int z = usize_to_int x + usize_to_int y
@@ -609,7 +610,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I8_ADD_EQ:
+Theorem i8_add_eq:
   !x y.
     i8_min <= i8_to_int x + i8_to_int y ==>
     i8_to_int x + i8_to_int y <= i8_max ==>
@@ -618,7 +619,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I16_ADD_EQ:
+Theorem i16_add_eq:
   !x y.
     i16_min <= i16_to_int x + i16_to_int y ==>
     i16_to_int x + i16_to_int y <= i16_max ==>
@@ -627,7 +628,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I32_ADD_EQ:
+Theorem i32_add_eq:
   !x y.
     i32_min <= i32_to_int x + i32_to_int y ==>
     i32_to_int x + i32_to_int y <= i32_max ==>
@@ -636,7 +637,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I64_ADD_EQ:
+Theorem i64_add_eq:
   !x y.
     i64_min <= i64_to_int x + i64_to_int y ==>
     i64_to_int x + i64_to_int y <= i64_max ==>
@@ -645,7 +646,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I128_ADD_EQ:
+Theorem i128_add_eq:
   !x y.
     i128_min <= i128_to_int x + i128_to_int y ==>
     i128_to_int x + i128_to_int y <= i128_max ==>
@@ -654,7 +655,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem ISIZE_ADD_EQ:
+Theorem isize_add_eq:
   !x y.
     (i16_min <= isize_to_int x + isize_to_int y \/ isize_min <= isize_to_int x + isize_to_int y) ==>
     (isize_to_int x + isize_to_int y <= i16_max \/ isize_to_int x + isize_to_int y <= isize_max) ==>
@@ -664,21 +665,21 @@ Proof
 QED
 
 val all_add_eqs = [
-  ISIZE_ADD_EQ,
-  I8_ADD_EQ,
-  I16_ADD_EQ,
-  I32_ADD_EQ,
-  I64_ADD_EQ,
-  I128_ADD_EQ,
-  USIZE_ADD_EQ,
-  U8_ADD_EQ,
-  U16_ADD_EQ,
-  U32_ADD_EQ,
-  U64_ADD_EQ,
-  U128_ADD_EQ
+  isize_add_eq,
+  i8_add_eq,
+  i16_add_eq,
+  i32_add_eq,
+  i64_add_eq,
+  i128_add_eq,
+  usize_add_eq,
+  u8_add_eq,
+  u16_add_eq,
+  u32_add_eq,
+  u64_add_eq,
+  u128_add_eq
 ]
       
-Theorem U8_SUB_EQ:
+Theorem u8_sub_eq:
   !x y.
     0 <= u8_to_int x - u8_to_int y ==>
     ?z. u8_sub x y = Return z /\ u8_to_int z = u8_to_int x - u8_to_int y
@@ -686,7 +687,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U16_SUB_EQ:
+Theorem u16_sub_eq:
   !x y.
     0 <= u16_to_int x - u16_to_int y ==>
     ?z. u16_sub x y = Return z /\ u16_to_int z = u16_to_int x - u16_to_int y
@@ -694,7 +695,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U32_SUB_EQ:
+Theorem u32_sub_eq:
   !x y.
     0 <= u32_to_int x - u32_to_int y ==>
     ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y
@@ -702,7 +703,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U64_SUB_EQ:
+Theorem u64_sub_eq:
   !x y.
     0 <= u64_to_int x - u64_to_int y ==>
     ?z. u64_sub x y = Return z /\ u64_to_int z = u64_to_int x - u64_to_int y
@@ -710,7 +711,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U128_SUB_EQ:
+Theorem u128_sub_eq:
   !x y.
     0 <= u128_to_int x - u128_to_int y ==>
     ?z. u128_sub x y = Return z /\ u128_to_int z = u128_to_int x - u128_to_int y
@@ -718,7 +719,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem USIZE_SUB_EQ:
+Theorem usize_sub_eq:
   !x y.
     0 <= usize_to_int x - usize_to_int y ==>
     ?z. usize_sub x y = Return z /\ usize_to_int z = usize_to_int x - usize_to_int y
@@ -726,7 +727,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I8_SUB_EQ:
+Theorem i8_sub_eq:
   !x y.
     i8_min <= i8_to_int x - i8_to_int y ==>
     i8_to_int x - i8_to_int y <= i8_max ==>
@@ -735,7 +736,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I16_SUB_EQ:
+Theorem i16_sub_eq:
   !x y.
     i16_min <= i16_to_int x - i16_to_int y ==>
     i16_to_int x - i16_to_int y <= i16_max ==>
@@ -744,7 +745,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I32_SUB_EQ:
+Theorem i32_sub_eq:
   !x y.
     i32_min <= i32_to_int x - i32_to_int y ==>
     i32_to_int x - i32_to_int y <= i32_max ==>
@@ -753,7 +754,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I64_SUB_EQ:
+Theorem i64_sub_eq:
   !x y.
     i64_min <= i64_to_int x - i64_to_int y ==>
     i64_to_int x - i64_to_int y <= i64_max ==>
@@ -762,7 +763,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I128_SUB_EQ:
+Theorem i128_sub_eq:
   !x y.
     i128_min <= i128_to_int x - i128_to_int y ==>
     i128_to_int x - i128_to_int y <= i128_max ==>
@@ -771,7 +772,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem ISIZE_SUB_EQ:
+Theorem isize_sub_eq:
   !x y.
     (i16_min <= isize_to_int x - isize_to_int y \/ isize_min <= isize_to_int x - isize_to_int y) ==>
     (isize_to_int x - isize_to_int y <= i16_max \/ isize_to_int x - isize_to_int y <= isize_max) ==>
@@ -781,21 +782,21 @@ Proof
 QED
 
 val all_sub_eqs = [
-  ISIZE_SUB_EQ,
-  I8_SUB_EQ,
-  I16_SUB_EQ,
-  I32_SUB_EQ,
-  I64_SUB_EQ,
-  I128_SUB_EQ,
-  USIZE_SUB_EQ,
-  U8_SUB_EQ,
-  U16_SUB_EQ,
-  U32_SUB_EQ,
-  U64_SUB_EQ,
-  U128_SUB_EQ
+  isize_sub_eq,
+  i8_sub_eq,
+  i16_sub_eq,
+  i32_sub_eq,
+  i64_sub_eq,
+  i128_sub_eq,
+  usize_sub_eq,
+  u8_sub_eq,
+  u16_sub_eq,
+  u32_sub_eq,
+  u64_sub_eq,
+  u128_sub_eq
 ]
 
-Theorem U8_MUL_EQ:
+Theorem u8_mul_eq:
   !x y.
     u8_to_int x * u8_to_int y <= u8_max ==>
     ?z. u8_mul x y = Return z /\ u8_to_int z = u8_to_int x * u8_to_int y
@@ -803,7 +804,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U16_MUL_EQ:
+Theorem u16_mul_eq:
   !x y.
     u16_to_int x * u16_to_int y <= u16_max ==>
     ?z. u16_mul x y = Return z /\ u16_to_int z = u16_to_int x * u16_to_int y
@@ -811,7 +812,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U32_MUL_EQ:
+Theorem u32_mul_eq:
   !x y.
     u32_to_int x * u32_to_int y <= u32_max ==>
     ?z. u32_mul x y = Return z /\ u32_to_int z = u32_to_int x * u32_to_int y
@@ -819,7 +820,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U64_MUL_EQ:
+Theorem u64_mul_eq:
   !x y.
     u64_to_int x * u64_to_int y <= u64_max ==>
     ?z. u64_mul x y = Return z /\ u64_to_int z = u64_to_int x * u64_to_int y
@@ -827,7 +828,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U128_MUL_EQ:
+Theorem u128_mul_eq:
   !x y.
     u128_to_int x * u128_to_int y <= u128_max ==>
     ?z. u128_mul x y = Return z /\ u128_to_int z = u128_to_int x * u128_to_int y
@@ -835,7 +836,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem USIZE_MUL_EQ:
+Theorem usize_mul_eq:
   !x y.
     (usize_to_int x * usize_to_int y <= u16_max) \/ (usize_to_int x * usize_to_int y <= usize_max) ==>
     ?z. usize_mul x y = Return z /\ usize_to_int z = usize_to_int x * usize_to_int y
@@ -843,7 +844,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I8_MUL_EQ:
+Theorem i8_mul_eq:
   !x y.
     i8_min <= i8_to_int x * i8_to_int y ==>
     i8_to_int x * i8_to_int y <= i8_max ==>
@@ -852,7 +853,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I16_MUL_EQ:
+Theorem i16_mul_eq:
   !x y.
     i16_min <= i16_to_int x * i16_to_int y ==>
     i16_to_int x * i16_to_int y <= i16_max ==>
@@ -861,7 +862,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I32_MUL_EQ:
+Theorem i32_mul_eq:
   !x y.
     i32_min <= i32_to_int x * i32_to_int y ==>
     i32_to_int x * i32_to_int y <= i32_max ==>
@@ -870,7 +871,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I64_MUL_EQ:
+Theorem i64_mul_eq:
   !x y.
     i64_min <= i64_to_int x * i64_to_int y ==>
     i64_to_int x * i64_to_int y <= i64_max ==>
@@ -879,7 +880,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I128_MUL_EQ:
+Theorem i128_mul_eq:
   !x y.
     i128_min <= i128_to_int x * i128_to_int y ==>
     i128_to_int x * i128_to_int y <= i128_max ==>
@@ -888,7 +889,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem ISIZE_MUL_EQ:
+Theorem isize_mul_eq:
   !x y.
     (i16_min <= isize_to_int x * isize_to_int y \/ isize_min <= isize_to_int x * isize_to_int y) ==>
     (isize_to_int x * isize_to_int y <= i16_max \/ isize_to_int x * isize_to_int y <= isize_max) ==>
@@ -898,21 +899,21 @@ Proof
 QED
 
 val all_mul_eqs = [
-  ISIZE_MUL_EQ,
-  I8_MUL_EQ,
-  I16_MUL_EQ,
-  I32_MUL_EQ,
-  I64_MUL_EQ,
-  I128_MUL_EQ,
-  USIZE_MUL_EQ,
-  U8_MUL_EQ,
-  U16_MUL_EQ,
-  U32_MUL_EQ,
-  U64_MUL_EQ,
-  U128_MUL_EQ
+  isize_mul_eq,
+  i8_mul_eq,
+  i16_mul_eq,
+  i32_mul_eq,
+  i64_mul_eq,
+  i128_mul_eq,
+  usize_mul_eq,
+  u8_mul_eq,
+  u16_mul_eq,
+  u32_mul_eq,
+  u64_mul_eq,
+  u128_mul_eq
 ]
 
-Theorem U8_DIV_EQ:
+Theorem u8_div_eq:
   !x y.
     u8_to_int y <> 0 ==>
     ?z. u8_div x y = Return z /\ u8_to_int z = u8_to_int x / u8_to_int y
@@ -920,7 +921,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U16_DIV_EQ:
+Theorem u16_div_eq:
   !x y.
     u16_to_int y <> 0 ==>
     ?z. u16_div x y = Return z /\ u16_to_int z = u16_to_int x / u16_to_int y
@@ -928,7 +929,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U32_DIV_EQ:
+Theorem u32_div_eq:
   !x y.
     u32_to_int y <> 0 ==>
     ?z. u32_div x y = Return z /\ u32_to_int z = u32_to_int x / u32_to_int y
@@ -936,7 +937,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U64_DIV_EQ:
+Theorem u64_div_eq:
   !x y.
     u64_to_int y <> 0 ==>
     ?z. u64_div x y = Return z /\ u64_to_int z = u64_to_int x / u64_to_int y
@@ -944,7 +945,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U128_DIV_EQ:
+Theorem u128_div_eq:
   !x y.
     u128_to_int y <> 0 ==>
     ?z. u128_div x y = Return z /\ u128_to_int z = u128_to_int x / u128_to_int y
@@ -952,7 +953,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem USIZE_DIV_EQ:
+Theorem usize_div_eq:
   !x y.
     usize_to_int y <> 0 ==>
     ?z. usize_div x y = Return z /\ usize_to_int z = usize_to_int x / usize_to_int y
@@ -960,7 +961,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I8_DIV_EQ:
+Theorem i8_div_eq:
   !x y.
     i8_to_int y <> 0 ==>
     i8_min <= i8_to_int x / i8_to_int y ==>
@@ -970,7 +971,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I16_DIV_EQ:
+Theorem i16_div_eq:
   !x y.
     i16_to_int y <> 0 ==>
     i16_min <= i16_to_int x / i16_to_int y ==>
@@ -980,7 +981,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I32_DIV_EQ:
+Theorem i32_div_eq:
   !x y.
     i32_to_int y <> 0 ==>
     i32_min <= i32_to_int x / i32_to_int y ==>
@@ -990,7 +991,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I64_DIV_EQ:
+Theorem i64_div_eq:
   !x y.
     i64_to_int y <> 0 ==>
     i64_min <= i64_to_int x / i64_to_int y ==>
@@ -1000,7 +1001,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I128_DIV_EQ:
+Theorem i128_div_eq:
   !x y.
     i128_to_int y <> 0 ==>
     i128_min <= i128_to_int x / i128_to_int y ==>
@@ -1010,7 +1011,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem ISIZE_DIV_EQ:
+Theorem isize_div_eq:
   !x y.
     isize_to_int y <> 0 ==>
     (i16_min <= isize_to_int x / isize_to_int y \/ isize_min <= isize_to_int x / isize_to_int y) ==>
@@ -1021,21 +1022,21 @@ Proof
 QED
 
 val all_div_eqs = [
-  ISIZE_DIV_EQ,
-  I8_DIV_EQ,
-  I16_DIV_EQ,
-  I32_DIV_EQ,
-  I64_DIV_EQ,
-  I128_DIV_EQ,
-  USIZE_DIV_EQ,
-  U8_DIV_EQ,
-  U16_DIV_EQ,
-  U32_DIV_EQ,
-  U64_DIV_EQ,
-  U128_DIV_EQ
+  isize_div_eq,
+  i8_div_eq,
+  i16_div_eq,
+  i32_div_eq,
+  i64_div_eq,
+  i128_div_eq,
+  usize_div_eq,
+  u8_div_eq,
+  u16_div_eq,
+  u32_div_eq,
+  u64_div_eq,
+  u128_div_eq
 ]
 
-Theorem U8_REM_EQ:
+Theorem u8_rem_eq:
   !x y.
     u8_to_int y <> 0 ==>
     ?z. u8_rem x y = Return z /\ u8_to_int z = int_rem (u8_to_int x) (u8_to_int y)
@@ -1043,7 +1044,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U16_REM_EQ:
+Theorem u16_rem_eq:
   !x y.
     u16_to_int y <> 0 ==>
     ?z. u16_rem x y = Return z /\ u16_to_int z = int_rem (u16_to_int x) (u16_to_int y)
@@ -1051,7 +1052,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U32_REM_EQ:
+Theorem u32_rem_eq:
   !x y.
     u32_to_int y <> 0 ==>
     ?z. u32_rem x y = Return z /\ u32_to_int z = int_rem (u32_to_int x) (u32_to_int y)
@@ -1059,7 +1060,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U64_REM_EQ:
+Theorem u64_rem_eq:
   !x y.
     u64_to_int y <> 0 ==>
     ?z. u64_rem x y = Return z /\ u64_to_int z = int_rem (u64_to_int x) (u64_to_int y)
@@ -1067,7 +1068,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem U128_REM_EQ:
+Theorem u128_rem_eq:
   !x y.
     u128_to_int y <> 0 ==>
     ?z. u128_rem x y = Return z /\ u128_to_int z = int_rem (u128_to_int x) (u128_to_int y)
@@ -1075,7 +1076,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem USIZE_REM_EQ:
+Theorem usize_rem_eq:
   !x y.
     usize_to_int y <> 0 ==>
     ?z. usize_rem x y = Return z /\ usize_to_int z = int_rem (usize_to_int x) (usize_to_int y)
@@ -1083,7 +1084,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I8_REM_EQ:
+Theorem i8_rem_eq:
   !x y.
     i8_to_int y <> 0 ==>
     i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==>
@@ -1093,7 +1094,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I16_REM_EQ:
+Theorem i16_rem_eq:
   !x y.
     i16_to_int y <> 0 ==>
     i16_min <= int_rem (i16_to_int x) (i16_to_int y) ==>
@@ -1103,7 +1104,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I32_REM_EQ:
+Theorem i32_rem_eq:
   !x y.
     i32_to_int y <> 0 ==>
     i32_min <= int_rem (i32_to_int x) (i32_to_int y) ==>
@@ -1113,7 +1114,7 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I64_REM_EQ:
+Theorem i64_rem_eq:
   !x y.
     i64_to_int y <> 0 ==>
     i64_min <= int_rem (i64_to_int x) (i64_to_int y) ==>
@@ -1123,141 +1124,44 @@ Proof
   prove_arith_op_eq
 QED
 
-Theorem I8_REM_EQ:
-  !x y.
-    i8_to_int y <> 0 ==>
-    i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==>
-    int_rem (i8_to_int x) (i8_to_int y) <= i8_max ==>
-    ?z. i8_rem x y = Return z /\ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y)
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem I8_REM_EQ:
-  !x y.
-    i8_to_int y <> 0 ==>
-    i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==>
-    int_rem (i8_to_int x) (i8_to_int y) <= i8_max ==>
-    ?z. i8_rem x y = Return z /\ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y)
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem U16_DIV_EQ:
-  !x y.
-    u16_to_int y <> 0 ==>
-    ?z. u16_div x y = Return z /\ u16_to_int z = u16_to_int x / u16_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem U32_DIV_EQ:
-  !x y.
-    u32_to_int y <> 0 ==>
-    ?z. u32_div x y = Return z /\ u32_to_int z = u32_to_int x / u32_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem U64_DIV_EQ:
-  !x y.
-    u64_to_int y <> 0 ==>
-    ?z. u64_div x y = Return z /\ u64_to_int z = u64_to_int x / u64_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem U128_DIV_EQ:
-  !x y.
-    u128_to_int y <> 0 ==>
-    ?z. u128_div x y = Return z /\ u128_to_int z = u128_to_int x / u128_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem USIZE_DIV_EQ:
-  !x y.
-    usize_to_int y <> 0 ==>
-    ?z. usize_div x y = Return z /\ usize_to_int z = usize_to_int x / usize_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem I8_DIV_EQ:
-  !x y.
-    i8_to_int y <> 0 ==>
-    i8_min <= i8_to_int x / i8_to_int y ==>
-    i8_to_int x / i8_to_int y <= i8_max ==>
-    ?z. i8_div x y = Return z /\ i8_to_int z = i8_to_int x / i8_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem I16_DIV_EQ:
-  !x y.
-    i16_to_int y <> 0 ==>
-    i16_min <= i16_to_int x / i16_to_int y ==>
-    i16_to_int x / i16_to_int y <= i16_max ==>
-    ?z. i16_div x y = Return z /\ i16_to_int z = i16_to_int x / i16_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem I32_DIV_EQ:
-  !x y.
-    i32_to_int y <> 0 ==>
-    i32_min <= i32_to_int x / i32_to_int y ==>
-    i32_to_int x / i32_to_int y <= i32_max ==>
-    ?z. i32_div x y = Return z /\ i32_to_int z = i32_to_int x / i32_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem I64_DIV_EQ:
-  !x y.
-    i64_to_int y <> 0 ==>
-    i64_min <= i64_to_int x / i64_to_int y ==>
-    i64_to_int x / i64_to_int y <= i64_max ==>
-    ?z. i64_div x y = Return z /\ i64_to_int z = i64_to_int x / i64_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-Theorem I128_DIV_EQ:
+Theorem i128_rem_eq:
   !x y.
     i128_to_int y <> 0 ==>
-    i128_min <= i128_to_int x / i128_to_int y ==>
-    i128_to_int x / i128_to_int y <= i128_max ==>
-    ?z. i128_div x y = Return z /\ i128_to_int z = i128_to_int x / i128_to_int y
+    i128_min <= int_rem (i128_to_int x) (i128_to_int y) ==>
+    int_rem (i128_to_int x) (i128_to_int y) <= i128_max ==>
+    ?z. i128_rem x y = Return z /\ i128_to_int z = int_rem (i128_to_int x) (i128_to_int y)
 Proof
   prove_arith_op_eq
 QED
 
-Theorem ISIZE_DIV_EQ:
+Theorem isize_rem_eq:
   !x y.
     isize_to_int y <> 0 ==>
-    (i16_min <= isize_to_int x / isize_to_int y \/ isize_min <= isize_to_int x / isize_to_int y) ==>
-    (isize_to_int x / isize_to_int y <= i16_max \/ isize_to_int x / isize_to_int y <= isize_max) ==>
-    ?z. isize_div x y = Return z /\ isize_to_int z = isize_to_int x / isize_to_int y
-Proof
-  prove_arith_op_eq
-QED
-
-val all_div_eqs = [
-  ISIZE_DIV_EQ,
-  I8_DIV_EQ,
-  I16_DIV_EQ,
-  I32_DIV_EQ,
-  I64_DIV_EQ,
-  I128_DIV_EQ,
-  USIZE_DIV_EQ,
-  U8_DIV_EQ,
-  U16_DIV_EQ,
-  U32_DIV_EQ,
-  U64_DIV_EQ,
-  U128_DIV_EQ
+    (i16_min <= int_rem (isize_to_int x) (isize_to_int y) \/
+     isize_min <= int_rem (isize_to_int x) (isize_to_int y)) ==>
+    (int_rem (isize_to_int x) (isize_to_int y) <= i16_max \/
+     int_rem (isize_to_int x) (isize_to_int y) <= isize_max) ==>
+    ?z. isize_rem x y = Return z /\ isize_to_int z = int_rem (isize_to_int x) (isize_to_int y)
+Proof
+  prove_arith_op_eq
+QED
+
+val all_rem_eqs = [
+  isize_rem_eq,
+  i8_rem_eq,
+  i16_rem_eq,
+  i32_rem_eq,
+  i64_rem_eq,
+  i128_rem_eq,
+  usize_rem_eq,
+  u8_rem_eq,
+  u16_rem_eq,
+  u32_rem_eq,
+  u64_rem_eq,
+  u128_rem_eq
 ]
 
+
 (***
  * Vectors
  *)
@@ -1268,98 +1172,102 @@ val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)
 val _ = new_constant ("mk_vec", “:'a list -> 'a vec result”)
 
 
-val VEC_TO_LIST_NUM_BOUNDS =
-  new_axiom ("VEC_TO_LIST_BOUNDS",
+val vec_to_list_num_bounds =
+  new_axiom ("vec_to_list_num_bounds",
     “!v. let l = LENGTH (vec_to_list v) in
      (0:num) <= l /\ l <= Num usize_max”)
 
-Theorem VEC_TO_LIST_INT_BOUNDS:
+Theorem vec_to_list_int_bounds:
   !v. 0 <= int_of_num (LENGTH (vec_to_list v)) /\ int_of_num (LENGTH (vec_to_list v)) <= usize_max
 Proof
   gen_tac >>
-  assume_tac VEC_TO_LIST_NUM_BOUNDS >>
-  pop_assum (qspec_then ‘v’ ASSUME_TAC) >>
-  pop_assum MP_TAC >>
-  PURE_ONCE_REWRITE_TAC [GSYM INT_LE] >>
-  sg ‘0 ≤ usize_max’ >- (ASSUME_TAC usize_bounds >> fs [u16_max_def] >> COOPER_TAC) >>
+  assume_tac vec_to_list_num_bounds >>
+  pop_assum (qspec_assume ‘v’) >>
+  pop_assum mp_tac >>
+  pure_once_rewrite_tac [GSYM INT_LE] >>
+  sg ‘0 ≤ usize_max’ >- (assume_tac usize_bounds >> fs [u16_max_def] >> cooper_tac) >>
   metis_tac [INT_OF_NUM]
 QED
 
-val VEC_LEN_DEF = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’
-Theorem VEC_LEN_SPEC:
+val vec_len_def = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’
+Theorem vec_len_spec:
   ∀v.
     vec_len v = int_to_usize (&(LENGTH (vec_to_list v))) ∧
     0 ≤ &(LENGTH (vec_to_list v)) ∧ &(LENGTH (vec_to_list v)) ≤ usize_max
 Proof
-  gen_tac >> rw [VEC_LEN_DEF] >>
-  qspec_then ‘v’ ASSUME_TAC VEC_TO_LIST_INT_BOUNDS >>
+  gen_tac >> rw [vec_len_def] >>
+  qspec_assume ‘v’ vec_to_list_int_bounds >>
   fs []
 QED
 
-val MK_VEC_SPEC = new_axiom ("MK_VEC_SPEC", “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
+val mk_vec_spec = new_axiom ("mk_vec_spec",
+  “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
 
-val VEC_NEW_DEF = Define ‘vec_new = case mk_vec [] of Return v => v’
-Theorem VEC_NEW_SPEC:
+val vec_new_def = Define ‘vec_new = case mk_vec [] of Return v => v’
+Theorem vec_new_spec:
   vec_to_list vec_new = []
 Proof
-  rw [VEC_NEW_DEF] >>
+  rw [vec_new_def] >>
   qabbrev_tac ‘l = []’ >>
-  qspec_then ‘l’ ASSUME_TAC MK_VEC_SPEC >>
+  qspec_assume ‘l’ mk_vec_spec >>
   Cases_on ‘mk_vec l’ >>
-  rfs [markerTheory.Abbrev_def, NOT_LE_EQ_GT] >> fs [] >>
-  ASSUME_TAC usize_bounds >> fs[u16_max_def] >> TRY (ex_falso >> COOPER_TAC) >>
-  sg ‘0 ≤ usize_max’ >- COOPER_TAC >>
+  rfs [markerTheory.Abbrev_def, not_le_eq_gt] >> fs [] >>
+  assume_tac usize_bounds >> fs[u16_max_def] >> try_tac (exfalso >> cooper_tac) >>
+  sg ‘0 ≤ usize_max’ >- cooper_tac >>
   fs []
 QED
 
-val VEC_PUSH_DEF = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’
-Theorem VEC_PUSH_SPEC:
+val vec_push_def = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’
+Theorem vec_push_spec:
   ∀v x. usize_to_int (vec_len v) < usize_max ⇒
     ∃vx. vec_push_back v x = Return vx ∧
     vec_to_list vx = vec_to_list v ++ [x]
 Proof
-  rpt strip_tac >> fs [VEC_PUSH_DEF] >>
-  qspec_then ‘v’ ASSUME_TAC VEC_LEN_SPEC >> rw [] >>
-  qspec_then ‘vec_to_list v ++ [x]’ ASSUME_TAC MK_VEC_SPEC >>
-  fs [VEC_LEN_DEF] >> rw [] >>
+  rpt strip_tac >> fs [vec_push_def] >>
+  qspec_assume ‘v’ vec_len_spec >> rw [] >>
+  qspec_assume ‘vec_to_list v ++ [x]’ mk_vec_spec >>
+  fs [vec_len_def] >> rw [] >>
   pop_assum irule >>
-  pop_last_assum MP_TAC >>
+  pop_last_assum mp_tac >>
   dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >>
-  COOPER_TAC
+  cooper_tac
 QED
 
-val UPDATE_DEF = Define ‘
+val update_def = Define ‘
   update ([] : 'a list) (i : num) (y : 'a) : 'a list = [] ∧
   update (_ :: ls) (0: num) y = y :: ls ∧
   update (x :: ls) (SUC i) y = x :: update ls i y
 ’
 
-Theorem UPDATE_LENGTH:
+Theorem update_length:
   ∀ls i y. LENGTH (update ls i y) = LENGTH ls
 Proof
-  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [UPDATE_DEF]
+  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def]
 QED
 
-Theorem UPDATE_SPEC:
+Theorem update_spec:
   ∀ls i y. i < LENGTH ls ==>
     LENGTH (update ls i y) = LENGTH ls ∧
     EL i (update ls i y) = y ∧
     ∀j. j < LENGTH ls ⇒ j ≠ i ⇒ EL j (update ls i y) = EL j ls
 Proof
-  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [UPDATE_DEF] >>
+  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] >>
   Cases_on ‘j’ >> fs []
 QED
 
 (* TODO: this is the base definition for index. Shall we remove the ‘return’ type? *)
-val VEC_INDEX_DEF = Define ‘
-  vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (EL (Num (usize_to_int i)) (vec_to_list v)) else Fail Failure’
+val vec_index_def = Define ‘
+  vec_index i v =
+    if usize_to_int i ≤ usize_to_int (vec_len v)
+    then Return (EL (Num (usize_to_int i)) (vec_to_list v))
+    else Fail Failure’
 
 (* TODO: shortcut for qspec_then ... ASSUME_TAC *)
 (* TODO: use cooper_tac everywhere *)
 (* TODO: use pure_once_rewrite_tac everywhere *)
 
 (* TODO: injectivity lemmas for ..._to_int *)
-Theorem USIZE_TO_INT_INJ:
+Theorem usize_to_int_inj:
   ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
 Proof
   rpt strip_tac >>
@@ -1368,23 +1276,16 @@ Proof
   metis_tac []
 QED
 
-Theorem USIZE_TO_INT_NEQ_INJ:
+Theorem usize_to_int_neq_inj:
   ∀i j. i <> j ==> usize_to_int i <> usize_to_int j
 Proof
-  metis_tac [USIZE_TO_INT_INJ]
-QED
-
-(* TODO: move *)
-Theorem INT_OF_NUM:
-  ∀i. 0 ≤ i ⇒ &Num i = i
-Proof
-  metis_tac[integerTheory.INT_OF_NUM]
+  metis_tac [usize_to_int_inj]
 QED
 
-Theorem INT_OF_NUM_NEQ_INJ:
+Theorem int_of_num_neq_inj:
   ∀n m. &n ≠ &m ⇒ n ≠ m
 Proof
-  metis_tac [INT_OF_NUM_INJ]
+  metis_tac [int_of_num_inj]
 QED
 
 (* TODO: automate: take assumption, intro first premise as subgoal *)
@@ -1403,10 +1304,10 @@ QED
   &n < &m
 *)
 
-val VEC_INSERT_BACK_DEF = Define ‘
+val vec_insert_back_def = Define ‘
   vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (Num (usize_to_int i)) x)’
 
-Theorem VEC_INSERT_BACK_SPEC:
+Theorem vec_insert_back_spec:
   ∀v i x.
     usize_to_int i < usize_to_int (vec_len v) ⇒
     ∃nv. vec_insert_back v i x = Return nv ∧
@@ -1415,20 +1316,21 @@ Theorem VEC_INSERT_BACK_SPEC:
     (* TODO: usize_to_int j ≠ usize_to_int i ? *)
     (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ j ≠ i ⇒ vec_index j nv = vec_index j v)
 Proof
-  rpt strip_tac >> fs [VEC_INSERT_BACK_DEF] >>
-  qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ MK_VEC_SPEC >>
-  qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] UPDATE_LENGTH >>
+  rpt strip_tac >> fs [vec_insert_back_def] >>
+  qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ mk_vec_spec >>
+  qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_length >>
   fs [] >>
-  qspec_assume ‘v’ VEC_LEN_SPEC >>
+  qspec_assume ‘v’ vec_len_spec >>
   rw [] >> gvs [] >>
-  fs [VEC_LEN_DEF, VEC_INDEX_DEF] >>
-  sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’ >-(irule int_to_usize_id >> COOPER_TAC) >>
+  fs [vec_len_def, vec_index_def] >>
+  sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’
+  >-(irule int_to_usize_id >> cooper_tac) >>
   fs [] >>
-  qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] UPDATE_SPEC >> rfs [] >>
+  qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_spec >> rfs [] >>
   sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-(
     (* TODO: automate *)
-    pure_once_rewrite_tac [GSYM INT_LT] >>
-    dep_pure_once_rewrite_tac [INT_OF_NUM] >>
+    pure_once_rewrite_tac [gsym INT_LT] >>
+    dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >>
     qspec_assume ‘i’ usize_to_int_bounds >> fs []
   ) >>
   fs [] >>
@@ -1437,35 +1339,19 @@ Proof
   first_x_assum irule >>
   rw [] >-(
     (* TODO: automate *)
-    irule INT_OF_NUM_NEQ_INJ >>
-    dep_pure_rewrite_tac [INT_OF_NUM] >>
+    irule int_of_num_neq_inj >>
+    dep_pure_rewrite_tac [primitivesArithTheory.int_of_num] >>
     rw [usize_to_int_bounds] >>
-    metis_tac [USIZE_TO_INT_NEQ_INJ]
+    metis_tac [usize_to_int_neq_inj]
   ) >>
   (* TODO: automate *)
-  pure_once_rewrite_tac [GSYM INT_LT] >>
-  dep_pure_once_rewrite_tac [INT_OF_NUM] >>
+  pure_once_rewrite_tac [gsym INT_LT] >>
+  dep_pure_once_rewrite_tac [primitivesArithTheory.int_of_num] >>
   qspec_assume ‘j’ usize_to_int_bounds >> fs []
 QED
 
 (* TODO: use lowercase everywhere for the theorem names *)
 
-(* We generate and save an induction theorem for positive integers *)
-Theorem int_induction:
-  !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i
-Proof
-  ntac 4 strip_tac >>
-  Induct_on ‘Num i’ >> rpt strip_tac
-  >-(sg ‘i = 0’ >- cooper_tac >> fs []) >>
-  last_assum (qspec_assume ‘i-1’) >>
-  fs [] >> pop_assum irule >>
-  rw [] >> try_tac cooper_tac >>
-  first_assum (qspec_assume ‘i - 1’) >>
-  pop_assum irule >>
-  rw [] >> try_tac cooper_tac
-QED
-
-val _ = TypeBase.update_induction int_induction
 
 (* Small experiment: trying to redefine common functions with integers instead of nums *)
 val index_def = Define ‘
@@ -1479,7 +1365,9 @@ val len_def = Define ‘
 
 val update_def = Define ‘
   update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧
-  update (x :: ls) (i : int) y = if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
+
+  update (x :: ls) (i : int) y =
+    if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
 ’
 
 Theorem update_len:
@@ -1496,7 +1384,8 @@ Theorem update_spec:
     index i (update ls i y) = y ∧
     ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
 Proof
-  Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >> try_tac (ex_falso >> cooper_tac) >>
+  Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >>
+  try_tac (exfalso >> cooper_tac) >>
   try_tac (
     pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >>
     pop_assum sg_premise_tac >- cooper_tac >>
@@ -1550,10 +1439,14 @@ Proof
 QED
 
 val vec_index_def = Define ‘
-  vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (index (usize_to_int i) (vec_to_list v)) else Fail Failure’
+  vec_index i v =
+    if usize_to_int i ≤ usize_to_int (vec_len v)
+    then Return (index (usize_to_int i) (vec_to_list v))
+    else Fail Failure’
 
 (* TODO: *)
-val mk_vec_spec = new_axiom ("mk_vec_spec", “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
+val mk_vec_spec = new_axiom ("mk_vec_spec",
+  “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
 
 (* Redefining ‘vec_insert_back’ *)
 val vec_insert_back_def = Define ‘
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index cc2f3115..66adac64 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -3,8 +3,6 @@ sig
   type thm = Thm.thm
   
   (*  Axioms  *)
-    val MK_VEC_SPEC : thm
-    val VEC_TO_LIST_BOUNDS : thm
     val i128_to_int_bounds : thm
     val i16_to_int_bounds : thm
     val i32_to_int_bounds : thm
@@ -44,6 +42,7 @@ sig
     val u8_to_int_bounds : thm
     val usize_bounds : thm
     val usize_to_int_bounds : thm
+    val vec_to_list_num_bounds : thm
   
   (*  Definitions  *)
     val bind_def : thm
@@ -156,70 +155,6 @@ sig
     val vec_push_back_def : thm
   
   (*  Theorems  *)
-    val I128_ADD_EQ : thm
-    val I128_DIV_EQ : thm
-    val I128_MUL_EQ : thm
-    val I128_SUB_EQ : thm
-    val I16_ADD_EQ : thm
-    val I16_DIV_EQ : thm
-    val I16_MUL_EQ : thm
-    val I16_REM_EQ : thm
-    val I16_SUB_EQ : thm
-    val I32_ADD_EQ : thm
-    val I32_DIV_EQ : thm
-    val I32_MUL_EQ : thm
-    val I32_REM_EQ : thm
-    val I32_SUB_EQ : thm
-    val I64_ADD_EQ : thm
-    val I64_DIV_EQ : thm
-    val I64_MUL_EQ : thm
-    val I64_REM_EQ : thm
-    val I64_SUB_EQ : thm
-    val I8_ADD_EQ : thm
-    val I8_DIV_EQ : thm
-    val I8_MUL_EQ : thm
-    val I8_REM_EQ : thm
-    val I8_SUB_EQ : thm
-    val INT_OF_NUM : thm
-    val INT_OF_NUM_NEQ_INJ : thm
-    val ISIZE_ADD_EQ : thm
-    val ISIZE_DIV_EQ : thm
-    val ISIZE_MUL_EQ : thm
-    val ISIZE_SUB_EQ : thm
-    val U128_ADD_EQ : thm
-    val U128_DIV_EQ : thm
-    val U128_MUL_EQ : thm
-    val U128_REM_EQ : thm
-    val U128_SUB_EQ : thm
-    val U16_ADD_EQ : thm
-    val U16_DIV_EQ : thm
-    val U16_MUL_EQ : thm
-    val U16_REM_EQ : thm
-    val U16_SUB_EQ : thm
-    val U32_ADD_EQ : thm
-    val U32_DIV_EQ : thm
-    val U32_MUL_EQ : thm
-    val U32_REM_EQ : thm
-    val U32_SUB_EQ : thm
-    val U64_ADD_EQ : thm
-    val U64_DIV_EQ : thm
-    val U64_MUL_EQ : thm
-    val U64_REM_EQ : thm
-    val U64_SUB_EQ : thm
-    val U8_ADD_EQ : thm
-    val U8_DIV_EQ : thm
-    val U8_MUL_EQ : thm
-    val U8_REM_EQ : thm
-    val U8_SUB_EQ : thm
-    val USIZE_ADD_EQ : thm
-    val USIZE_DIV_EQ : thm
-    val USIZE_MUL_EQ : thm
-    val USIZE_REM_EQ : thm
-    val USIZE_SUB_EQ : thm
-    val USIZE_TO_INT_INJ : thm
-    val USIZE_TO_INT_NEQ_INJ : thm
-    val VEC_NEW_SPEC : thm
-    val VEC_TO_LIST_INT_BOUNDS : thm
     val datatype_error : thm
     val datatype_result : thm
     val error2num_11 : thm
@@ -233,9 +168,39 @@ sig
     val error_case_eq : thm
     val error_induction : thm
     val error_nchotomy : thm
+    val i128_add_eq : thm
+    val i128_div_eq : thm
+    val i128_mul_eq : thm
+    val i128_rem_eq : thm
+    val i128_sub_eq : thm
+    val i16_add_eq : thm
+    val i16_div_eq : thm
+    val i16_mul_eq : thm
+    val i16_rem_eq : thm
+    val i16_sub_eq : thm
+    val i32_add_eq : thm
+    val i32_div_eq : thm
+    val i32_mul_eq : thm
+    val i32_rem_eq : thm
+    val i32_sub_eq : thm
+    val i64_add_eq : thm
+    val i64_div_eq : thm
+    val i64_mul_eq : thm
+    val i64_rem_eq : thm
+    val i64_sub_eq : thm
+    val i8_add_eq : thm
+    val i8_div_eq : thm
+    val i8_mul_eq : thm
+    val i8_rem_eq : thm
+    val i8_sub_eq : thm
     val index_update_diff : thm
     val index_update_same : thm
-    val int_induction : thm
+    val int_of_num_neq_inj : thm
+    val isize_add_eq : thm
+    val isize_div_eq : thm
+    val isize_mul_eq : thm
+    val isize_rem_eq : thm
+    val isize_sub_eq : thm
     val num2error_11 : thm
     val num2error_ONTO : thm
     val num2error_error2num : thm
@@ -247,9 +212,41 @@ sig
     val result_distinct : thm
     val result_induction : thm
     val result_nchotomy : thm
+    val u128_add_eq : thm
+    val u128_div_eq : thm
+    val u128_mul_eq : thm
+    val u128_rem_eq : thm
+    val u128_sub_eq : thm
+    val u16_add_eq : thm
+    val u16_div_eq : thm
+    val u16_mul_eq : thm
+    val u16_rem_eq : thm
+    val u16_sub_eq : thm
+    val u32_add_eq : thm
+    val u32_div_eq : thm
+    val u32_mul_eq : thm
+    val u32_rem_eq : thm
+    val u32_sub_eq : thm
+    val u64_add_eq : thm
+    val u64_div_eq : thm
+    val u64_mul_eq : thm
+    val u64_rem_eq : thm
+    val u64_sub_eq : thm
+    val u8_add_eq : thm
+    val u8_div_eq : thm
+    val u8_mul_eq : thm
+    val u8_rem_eq : thm
+    val u8_sub_eq : thm
     val update_ind : thm
     val update_len : thm
     val update_spec : thm
+    val usize_add_eq : thm
+    val usize_div_eq : thm
+    val usize_mul_eq : thm
+    val usize_rem_eq : thm
+    val usize_sub_eq : thm
+    val usize_to_int_inj : thm
+    val usize_to_int_neq_inj : thm
     val vec_insert_back_spec : thm
     val vec_len_spec : thm
     val vec_to_list_int_bounds : thm
@@ -265,207 +262,201 @@ sig
       [oracles: ] [axioms: mk_vec_spec] []
       ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
    
-   [VEC_TO_LIST_BOUNDS]  Axiom
+   [vec_to_list_num_bounds]  Axiom
       
-      [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
+      [oracles: ] [axioms: vec_to_list_num_bounds] []
       ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max)
    
-   [isize_bounds]  Axiom
-      
-      [oracles: ] [axioms: isize_bounds] []
-      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
-   
-   [usize_bounds]  Axiom
+   [int_to_usize_usize_to_int]  Axiom
       
-      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
+      [oracles: ] [axioms: int_to_usize_usize_to_int] []
+      ⊢ ∀i. int_to_usize (usize_to_int i) = i
    
-   [isize_to_int_bounds]  Axiom
+   [int_to_u128_u128_to_int]  Axiom
       
-      [oracles: ] [axioms: isize_to_int_bounds] []
-      ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
+      [oracles: ] [axioms: int_to_u128_u128_to_int] []
+      ⊢ ∀i. int_to_u128 (u128_to_int i) = i
    
-   [i8_to_int_bounds]  Axiom
+   [int_to_u64_u64_to_int]  Axiom
       
-      [oracles: ] [axioms: i8_to_int_bounds] []
-      ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
+      [oracles: ] [axioms: int_to_u64_u64_to_int] []
+      ⊢ ∀i. int_to_u64 (u64_to_int i) = i
    
-   [i16_to_int_bounds]  Axiom
+   [int_to_u32_u32_to_int]  Axiom
       
-      [oracles: ] [axioms: i16_to_int_bounds] []
-      ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
+      [oracles: ] [axioms: int_to_u32_u32_to_int] []
+      ⊢ ∀i. int_to_u32 (u32_to_int i) = i
    
-   [i32_to_int_bounds]  Axiom
+   [int_to_u16_u16_to_int]  Axiom
       
-      [oracles: ] [axioms: i32_to_int_bounds] []
-      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
+      [oracles: ] [axioms: int_to_u16_u16_to_int] []
+      ⊢ ∀i. int_to_u16 (u16_to_int i) = i
    
-   [i64_to_int_bounds]  Axiom
+   [int_to_u8_u8_to_int]  Axiom
       
-      [oracles: ] [axioms: i64_to_int_bounds] []
-      ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
+      [oracles: ] [axioms: int_to_u8_u8_to_int] []
+      ⊢ ∀i. int_to_u8 (u8_to_int i) = i
    
-   [i128_to_int_bounds]  Axiom
+   [int_to_isize_isize_to_int]  Axiom
       
-      [oracles: ] [axioms: i128_to_int_bounds] []
-      ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
+      [oracles: ] [axioms: int_to_isize_isize_to_int] []
+      ⊢ ∀i. int_to_isize (isize_to_int i) = i
    
-   [usize_to_int_bounds]  Axiom
+   [int_to_i128_i128_to_int]  Axiom
       
-      [oracles: ] [axioms: usize_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+      [oracles: ] [axioms: int_to_i128_i128_to_int] []
+      ⊢ ∀i. int_to_i128 (i128_to_int i) = i
    
-   [u8_to_int_bounds]  Axiom
+   [int_to_i64_i64_to_int]  Axiom
       
-      [oracles: ] [axioms: u8_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+      [oracles: ] [axioms: int_to_i64_i64_to_int] []
+      ⊢ ∀i. int_to_i64 (i64_to_int i) = i
    
-   [u16_to_int_bounds]  Axiom
+   [int_to_i32_i32_to_int]  Axiom
       
-      [oracles: ] [axioms: u16_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+      [oracles: ] [axioms: int_to_i32_i32_to_int] []
+      ⊢ ∀i. int_to_i32 (i32_to_int i) = i
    
-   [u32_to_int_bounds]  Axiom
+   [int_to_i16_i16_to_int]  Axiom
       
-      [oracles: ] [axioms: u32_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+      [oracles: ] [axioms: int_to_i16_i16_to_int] []
+      ⊢ ∀i. int_to_i16 (i16_to_int i) = i
    
-   [u64_to_int_bounds]  Axiom
+   [int_to_i8_i8_to_int]  Axiom
       
-      [oracles: ] [axioms: u64_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+      [oracles: ] [axioms: int_to_i8_i8_to_int] []
+      ⊢ ∀i. int_to_i8 (i8_to_int i) = i
    
-   [u128_to_int_bounds]  Axiom
+   [int_to_u128_id]  Axiom
       
-      [oracles: ] [axioms: u128_to_int_bounds] []
-      ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
+      [oracles: ] [axioms: int_to_u128_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
    
-   [int_to_isize_id]  Axiom
+   [int_to_u64_id]  Axiom
       
-      [oracles: ] [axioms: int_to_isize_id] []
-      ⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒
-            isize_to_int (int_to_isize n) = n
+      [oracles: ] [axioms: int_to_u64_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
    
-   [int_to_usize_id]  Axiom
+   [int_to_u32_id]  Axiom
       
-      [oracles: ] [axioms: int_to_usize_id] []
-      ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
-            usize_to_int (int_to_usize n) = n
+      [oracles: ] [axioms: int_to_u32_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
    
-   [int_to_i8_id]  Axiom
+   [int_to_u16_id]  Axiom
       
-      [oracles: ] [axioms: int_to_i8_id] []
-      ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
+      [oracles: ] [axioms: int_to_u16_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
    
-   [int_to_i16_id]  Axiom
+   [int_to_u8_id]  Axiom
       
-      [oracles: ] [axioms: int_to_i16_id] []
-      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
+      [oracles: ] [axioms: int_to_u8_id] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
    
-   [int_to_i32_id]  Axiom
+   [int_to_i128_id]  Axiom
       
-      [oracles: ] [axioms: int_to_i32_id] []
-      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+      [oracles: ] [axioms: int_to_i128_id] []
+      ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
    
    [int_to_i64_id]  Axiom
       
       [oracles: ] [axioms: int_to_i64_id] []
       ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
    
-   [int_to_i128_id]  Axiom
+   [int_to_i32_id]  Axiom
       
-      [oracles: ] [axioms: int_to_i128_id] []
-      ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
+      [oracles: ] [axioms: int_to_i32_id] []
+      ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
    
-   [int_to_u8_id]  Axiom
+   [int_to_i16_id]  Axiom
       
-      [oracles: ] [axioms: int_to_u8_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
+      [oracles: ] [axioms: int_to_i16_id] []
+      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
    
-   [int_to_u16_id]  Axiom
+   [int_to_i8_id]  Axiom
       
-      [oracles: ] [axioms: int_to_u16_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
+      [oracles: ] [axioms: int_to_i8_id] []
+      ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
    
-   [int_to_u32_id]  Axiom
+   [int_to_usize_id]  Axiom
       
-      [oracles: ] [axioms: int_to_u32_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
+      [oracles: ] [axioms: int_to_usize_id] []
+      ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
+            usize_to_int (int_to_usize n) = n
    
-   [int_to_u64_id]  Axiom
+   [int_to_isize_id]  Axiom
       
-      [oracles: ] [axioms: int_to_u64_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
+      [oracles: ] [axioms: int_to_isize_id] []
+      ⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒
+            isize_to_int (int_to_isize n) = n
    
-   [int_to_u128_id]  Axiom
+   [u128_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u128_id] []
-      ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
+      [oracles: ] [axioms: u128_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
    
-   [int_to_i8_i8_to_int]  Axiom
+   [u64_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i8_i8_to_int] []
-      ⊢ ∀i. int_to_i8 (i8_to_int i) = i
+      [oracles: ] [axioms: u64_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
    
-   [int_to_i16_i16_to_int]  Axiom
+   [u32_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i16_i16_to_int] []
-      ⊢ ∀i. int_to_i16 (i16_to_int i) = i
+      [oracles: ] [axioms: u32_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
    
-   [int_to_i32_i32_to_int]  Axiom
+   [u16_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i32_i32_to_int] []
-      ⊢ ∀i. int_to_i32 (i32_to_int i) = i
+      [oracles: ] [axioms: u16_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
    
-   [int_to_i64_i64_to_int]  Axiom
+   [u8_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i64_i64_to_int] []
-      ⊢ ∀i. int_to_i64 (i64_to_int i) = i
+      [oracles: ] [axioms: u8_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
    
-   [int_to_i128_i128_to_int]  Axiom
+   [usize_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_i128_i128_to_int] []
-      ⊢ ∀i. int_to_i128 (i128_to_int i) = i
+      [oracles: ] [axioms: usize_to_int_bounds] []
+      ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
    
-   [int_to_isize_isize_to_int]  Axiom
+   [i128_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_isize_isize_to_int] []
-      ⊢ ∀i. int_to_isize (isize_to_int i) = i
+      [oracles: ] [axioms: i128_to_int_bounds] []
+      ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
    
-   [int_to_u8_u8_to_int]  Axiom
+   [i64_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u8_u8_to_int] []
-      ⊢ ∀i. int_to_u8 (u8_to_int i) = i
+      [oracles: ] [axioms: i64_to_int_bounds] []
+      ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
    
-   [int_to_u16_u16_to_int]  Axiom
+   [i32_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u16_u16_to_int] []
-      ⊢ ∀i. int_to_u16 (u16_to_int i) = i
+      [oracles: ] [axioms: i32_to_int_bounds] []
+      ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
    
-   [int_to_u32_u32_to_int]  Axiom
+   [i16_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u32_u32_to_int] []
-      ⊢ ∀i. int_to_u32 (u32_to_int i) = i
+      [oracles: ] [axioms: i16_to_int_bounds] []
+      ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
    
-   [int_to_u64_u64_to_int]  Axiom
+   [i8_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u64_u64_to_int] []
-      ⊢ ∀i. int_to_u64 (u64_to_int i) = i
+      [oracles: ] [axioms: i8_to_int_bounds] []
+      ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
    
-   [int_to_u128_u128_to_int]  Axiom
+   [isize_to_int_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_u128_u128_to_int] []
-      ⊢ ∀i. int_to_u128 (u128_to_int i) = i
+      [oracles: ] [axioms: isize_to_int_bounds] []
+      ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
    
-   [int_to_usize_usize_to_int]  Axiom
+   [usize_bounds]  Axiom
       
-      [oracles: ] [axioms: int_to_usize_usize_to_int] []
-      ⊢ ∀i. int_to_usize (usize_to_int i) = i
+      [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
    
-   [MK_VEC_SPEC]  Axiom
+   [isize_bounds]  Axiom
       
-      [oracles: ] [axioms: MK_VEC_SPEC] []
-      ⊢ ∀l. &LENGTH l ≤ usize_max ⇒
-            ∃v. mk_vec l = Return v ∧ vec_to_list v = l
+      [oracles: ] [axioms: isize_bounds] []
+      ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
    
    [bind_def]  Definition
       
@@ -1035,7 +1026,61 @@ sig
       
       ⊢ ∀v x. vec_push_back v x = mk_vec (vec_to_list v ⧺ [x])
    
-   [I128_ADD_EQ]  Theorem
+   [datatype_error]  Theorem
+      
+      ⊢ DATATYPE (error Failure)
+   
+   [datatype_result]  Theorem
+      
+      ⊢ DATATYPE (result Return Fail Loop)
+   
+   [error2num_11]  Theorem
+      
+      ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a'
+   
+   [error2num_ONTO]  Theorem
+      
+      ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a
+   
+   [error2num_num2error]  Theorem
+      
+      ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r
+   
+   [error2num_thm]  Theorem
+      
+      ⊢ error2num Failure = 0
+   
+   [error_Axiom]  Theorem
+      
+      ⊢ ∀x0. ∃f. f Failure = x0
+   
+   [error_EQ_error]  Theorem
+      
+      ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a'
+   
+   [error_case_cong]  Theorem
+      
+      ⊢ ∀M M' v0.
+          M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒
+          (case M of Failure => v0) = case M' of Failure => v0'
+   
+   [error_case_def]  Theorem
+      
+      ⊢ ∀v0. (case Failure of Failure => v0) = v0
+   
+   [error_case_eq]  Theorem
+      
+      ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v
+   
+   [error_induction]  Theorem
+      
+      ⊢ ∀P. P Failure ⇒ ∀a. P a
+   
+   [error_nchotomy]  Theorem
+      
+      ⊢ ∀a. a = Failure
+   
+   [i128_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
@@ -1045,7 +1090,7 @@ sig
           ∃z. i128_add x y = Return z ∧
               i128_to_int z = i128_to_int x + i128_to_int y
    
-   [I128_DIV_EQ]  Theorem
+   [i128_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
@@ -1056,7 +1101,7 @@ sig
           ∃z. i128_div x y = Return z ∧
               i128_to_int z = i128_to_int x / i128_to_int y
    
-   [I128_MUL_EQ]  Theorem
+   [i128_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
@@ -1066,7 +1111,19 @@ sig
           ∃z. i128_mul x y = Return z ∧
               i128_to_int z = i128_to_int x * i128_to_int y
    
-   [I128_SUB_EQ]  Theorem
+   [i128_rem_eq]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: isize_bounds, int_to_i128_id, i128_to_int_bounds,
+       usize_bounds] []
+      ⊢ ∀x y.
+          i128_to_int y ≠ 0 ⇒
+          i128_min ≤ int_rem (i128_to_int x) (i128_to_int y) ⇒
+          int_rem (i128_to_int x) (i128_to_int y) ≤ i128_max ⇒
+          ∃z. i128_rem x y = Return z ∧
+              i128_to_int z = int_rem (i128_to_int x) (i128_to_int y)
+   
+   [i128_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
@@ -1076,7 +1133,7 @@ sig
           ∃z. i128_sub x y = Return z ∧
               i128_to_int z = i128_to_int x − i128_to_int y
    
-   [I16_ADD_EQ]  Theorem
+   [i16_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
@@ -1086,7 +1143,7 @@ sig
           ∃z. i16_add x y = Return z ∧
               i16_to_int z = i16_to_int x + i16_to_int y
    
-   [I16_DIV_EQ]  Theorem
+   [i16_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
@@ -1097,7 +1154,7 @@ sig
           ∃z. i16_div x y = Return z ∧
               i16_to_int z = i16_to_int x / i16_to_int y
    
-   [I16_MUL_EQ]  Theorem
+   [i16_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
@@ -1107,7 +1164,7 @@ sig
           ∃z. i16_mul x y = Return z ∧
               i16_to_int z = i16_to_int x * i16_to_int y
    
-   [I16_REM_EQ]  Theorem
+   [i16_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i16_id, i16_to_int_bounds, usize_bounds]
@@ -1119,7 +1176,7 @@ sig
           ∃z. i16_rem x y = Return z ∧
               i16_to_int z = int_rem (i16_to_int x) (i16_to_int y)
    
-   [I16_SUB_EQ]  Theorem
+   [i16_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
@@ -1129,7 +1186,7 @@ sig
           ∃z. i16_sub x y = Return z ∧
               i16_to_int z = i16_to_int x − i16_to_int y
    
-   [I32_ADD_EQ]  Theorem
+   [i32_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
@@ -1139,7 +1196,7 @@ sig
           ∃z. i32_add x y = Return z ∧
               i32_to_int z = i32_to_int x + i32_to_int y
    
-   [I32_DIV_EQ]  Theorem
+   [i32_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
@@ -1150,7 +1207,7 @@ sig
           ∃z. i32_div x y = Return z ∧
               i32_to_int z = i32_to_int x / i32_to_int y
    
-   [I32_MUL_EQ]  Theorem
+   [i32_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
@@ -1160,7 +1217,7 @@ sig
           ∃z. i32_mul x y = Return z ∧
               i32_to_int z = i32_to_int x * i32_to_int y
    
-   [I32_REM_EQ]  Theorem
+   [i32_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i32_id, i32_to_int_bounds, usize_bounds]
@@ -1172,7 +1229,7 @@ sig
           ∃z. i32_rem x y = Return z ∧
               i32_to_int z = int_rem (i32_to_int x) (i32_to_int y)
    
-   [I32_SUB_EQ]  Theorem
+   [i32_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
@@ -1182,7 +1239,7 @@ sig
           ∃z. i32_sub x y = Return z ∧
               i32_to_int z = i32_to_int x − i32_to_int y
    
-   [I64_ADD_EQ]  Theorem
+   [i64_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
@@ -1192,7 +1249,7 @@ sig
           ∃z. i64_add x y = Return z ∧
               i64_to_int z = i64_to_int x + i64_to_int y
    
-   [I64_DIV_EQ]  Theorem
+   [i64_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
@@ -1203,7 +1260,7 @@ sig
           ∃z. i64_div x y = Return z ∧
               i64_to_int z = i64_to_int x / i64_to_int y
    
-   [I64_MUL_EQ]  Theorem
+   [i64_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
@@ -1213,7 +1270,7 @@ sig
           ∃z. i64_mul x y = Return z ∧
               i64_to_int z = i64_to_int x * i64_to_int y
    
-   [I64_REM_EQ]  Theorem
+   [i64_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i64_id, i64_to_int_bounds, usize_bounds]
@@ -1225,7 +1282,7 @@ sig
           ∃z. i64_rem x y = Return z ∧
               i64_to_int z = int_rem (i64_to_int x) (i64_to_int y)
    
-   [I64_SUB_EQ]  Theorem
+   [i64_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
@@ -1235,7 +1292,7 @@ sig
           ∃z. i64_sub x y = Return z ∧
               i64_to_int z = i64_to_int x − i64_to_int y
    
-   [I8_ADD_EQ]  Theorem
+   [i8_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
@@ -1245,7 +1302,7 @@ sig
           ∃z. i8_add x y = Return z ∧
               i8_to_int z = i8_to_int x + i8_to_int y
    
-   [I8_DIV_EQ]  Theorem
+   [i8_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
@@ -1256,7 +1313,7 @@ sig
           ∃z. i8_div x y = Return z ∧
               i8_to_int z = i8_to_int x / i8_to_int y
    
-   [I8_MUL_EQ]  Theorem
+   [i8_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
@@ -1266,7 +1323,7 @@ sig
           ∃z. i8_mul x y = Return z ∧
               i8_to_int z = i8_to_int x * i8_to_int y
    
-   [I8_REM_EQ]  Theorem
+   [i8_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i8_id, i8_to_int_bounds, usize_bounds]
@@ -1278,7 +1335,7 @@ sig
           ∃z. i8_rem x y = Return z ∧
               i8_to_int z = int_rem (i8_to_int x) (i8_to_int y)
    
-   [I8_SUB_EQ]  Theorem
+   [i8_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
@@ -1288,15 +1345,24 @@ sig
           ∃z. i8_sub x y = Return z ∧
               i8_to_int z = i8_to_int x − i8_to_int y
    
-   [INT_OF_NUM]  Theorem
+   [index_update_diff]  Theorem
       
-      ⊢ ∀i. 0 ≤ i ⇒ &Num i = i
+      ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y
    
-   [INT_OF_NUM_NEQ_INJ]  Theorem
+   [index_update_same]  Theorem
+      
+      ⊢ ∀ls i j y.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          j < len ls ⇒
+          j ≠ i ⇒
+          index j (update ls i y) = index j ls
+   
+   [int_of_num_neq_inj]  Theorem
       
       ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m
    
-   [ISIZE_ADD_EQ]  Theorem
+   [isize_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
@@ -1309,7 +1375,7 @@ sig
           ∃z. isize_add x y = Return z ∧
               isize_to_int z = isize_to_int x + isize_to_int y
    
-   [ISIZE_DIV_EQ]  Theorem
+   [isize_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
@@ -1323,7 +1389,7 @@ sig
           ∃z. isize_div x y = Return z ∧
               isize_to_int z = isize_to_int x / isize_to_int y
    
-   [ISIZE_MUL_EQ]  Theorem
+   [isize_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
@@ -1336,7 +1402,21 @@ sig
           ∃z. isize_mul x y = Return z ∧
               isize_to_int z = isize_to_int x * isize_to_int y
    
-   [ISIZE_SUB_EQ]  Theorem
+   [isize_rem_eq]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
+       usize_bounds] []
+      ⊢ ∀x y.
+          isize_to_int y ≠ 0 ⇒
+          i16_min ≤ int_rem (isize_to_int x) (isize_to_int y) ∨
+          isize_min ≤ int_rem (isize_to_int x) (isize_to_int y) ⇒
+          int_rem (isize_to_int x) (isize_to_int y) ≤ i16_max ∨
+          int_rem (isize_to_int x) (isize_to_int y) ≤ isize_max ⇒
+          ∃z. isize_rem x y = Return z ∧
+              isize_to_int z = int_rem (isize_to_int x) (isize_to_int y)
+   
+   [isize_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
@@ -1349,7 +1429,60 @@ sig
           ∃z. isize_sub x y = Return z ∧
               isize_to_int z = isize_to_int x − isize_to_int y
    
-   [U128_ADD_EQ]  Theorem
+   [num2error_11]  Theorem
+      
+      ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
+   
+   [num2error_ONTO]  Theorem
+      
+      ⊢ ∀a. ∃r. a = num2error r ∧ r < 1
+   
+   [num2error_error2num]  Theorem
+      
+      ⊢ ∀a. num2error (error2num a) = a
+   
+   [num2error_thm]  Theorem
+      
+      ⊢ num2error 0 = Failure
+   
+   [result_11]  Theorem
+      
+      ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧
+        ∀a a'. Fail a = Fail a' ⇔ a = a'
+   
+   [result_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2. ∃fn.
+          (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧
+          fn Loop = f2
+   
+   [result_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1 v.
+          M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧
+          (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒
+          result_CASE M f f1 v = result_CASE M' f' f1' v'
+   
+   [result_case_eq]  Theorem
+      
+      ⊢ result_CASE x f f1 v = v' ⇔
+        (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨
+        x = Loop ∧ v = v'
+   
+   [result_distinct]  Theorem
+      
+      ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧
+        ∀a. Fail a ≠ Loop
+   
+   [result_induction]  Theorem
+      
+      ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r
+   
+   [result_nchotomy]  Theorem
+      
+      ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
+   
+   [u128_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
@@ -1359,7 +1492,7 @@ sig
           ∃z. u128_add x y = Return z ∧
               u128_to_int z = u128_to_int x + u128_to_int y
    
-   [U128_DIV_EQ]  Theorem
+   [u128_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
@@ -1369,7 +1502,7 @@ sig
           ∃z. u128_div x y = Return z ∧
               u128_to_int z = u128_to_int x / u128_to_int y
    
-   [U128_MUL_EQ]  Theorem
+   [u128_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
@@ -1379,7 +1512,7 @@ sig
           ∃z. u128_mul x y = Return z ∧
               u128_to_int z = u128_to_int x * u128_to_int y
    
-   [U128_REM_EQ]  Theorem
+   [u128_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
@@ -1389,7 +1522,7 @@ sig
           ∃z. u128_rem x y = Return z ∧
               u128_to_int z = int_rem (u128_to_int x) (u128_to_int y)
    
-   [U128_SUB_EQ]  Theorem
+   [u128_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
@@ -1399,7 +1532,7 @@ sig
           ∃z. u128_sub x y = Return z ∧
               u128_to_int z = u128_to_int x − u128_to_int y
    
-   [U16_ADD_EQ]  Theorem
+   [u16_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
@@ -1409,7 +1542,7 @@ sig
           ∃z. u16_add x y = Return z ∧
               u16_to_int z = u16_to_int x + u16_to_int y
    
-   [U16_DIV_EQ]  Theorem
+   [u16_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
@@ -1419,7 +1552,7 @@ sig
           ∃z. u16_div x y = Return z ∧
               u16_to_int z = u16_to_int x / u16_to_int y
    
-   [U16_MUL_EQ]  Theorem
+   [u16_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
@@ -1429,7 +1562,7 @@ sig
           ∃z. u16_mul x y = Return z ∧
               u16_to_int z = u16_to_int x * u16_to_int y
    
-   [U16_REM_EQ]  Theorem
+   [u16_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
@@ -1439,7 +1572,7 @@ sig
           ∃z. u16_rem x y = Return z ∧
               u16_to_int z = int_rem (u16_to_int x) (u16_to_int y)
    
-   [U16_SUB_EQ]  Theorem
+   [u16_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
@@ -1449,7 +1582,7 @@ sig
           ∃z. u16_sub x y = Return z ∧
               u16_to_int z = u16_to_int x − u16_to_int y
    
-   [U32_ADD_EQ]  Theorem
+   [u32_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
@@ -1459,7 +1592,7 @@ sig
           ∃z. u32_add x y = Return z ∧
               u32_to_int z = u32_to_int x + u32_to_int y
    
-   [U32_DIV_EQ]  Theorem
+   [u32_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
@@ -1469,7 +1602,7 @@ sig
           ∃z. u32_div x y = Return z ∧
               u32_to_int z = u32_to_int x / u32_to_int y
    
-   [U32_MUL_EQ]  Theorem
+   [u32_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
@@ -1479,7 +1612,7 @@ sig
           ∃z. u32_mul x y = Return z ∧
               u32_to_int z = u32_to_int x * u32_to_int y
    
-   [U32_REM_EQ]  Theorem
+   [u32_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
@@ -1489,7 +1622,7 @@ sig
           ∃z. u32_rem x y = Return z ∧
               u32_to_int z = int_rem (u32_to_int x) (u32_to_int y)
    
-   [U32_SUB_EQ]  Theorem
+   [u32_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
@@ -1499,7 +1632,7 @@ sig
           ∃z. u32_sub x y = Return z ∧
               u32_to_int z = u32_to_int x − u32_to_int y
    
-   [U64_ADD_EQ]  Theorem
+   [u64_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
@@ -1509,7 +1642,7 @@ sig
           ∃z. u64_add x y = Return z ∧
               u64_to_int z = u64_to_int x + u64_to_int y
    
-   [U64_DIV_EQ]  Theorem
+   [u64_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
@@ -1519,7 +1652,7 @@ sig
           ∃z. u64_div x y = Return z ∧
               u64_to_int z = u64_to_int x / u64_to_int y
    
-   [U64_MUL_EQ]  Theorem
+   [u64_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
@@ -1529,7 +1662,7 @@ sig
           ∃z. u64_mul x y = Return z ∧
               u64_to_int z = u64_to_int x * u64_to_int y
    
-   [U64_REM_EQ]  Theorem
+   [u64_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
@@ -1539,7 +1672,7 @@ sig
           ∃z. u64_rem x y = Return z ∧
               u64_to_int z = int_rem (u64_to_int x) (u64_to_int y)
    
-   [U64_SUB_EQ]  Theorem
+   [u64_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
@@ -1549,7 +1682,7 @@ sig
           ∃z. u64_sub x y = Return z ∧
               u64_to_int z = u64_to_int x − u64_to_int y
    
-   [U8_ADD_EQ]  Theorem
+   [u8_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
@@ -1559,7 +1692,7 @@ sig
           ∃z. u8_add x y = Return z ∧
               u8_to_int z = u8_to_int x + u8_to_int y
    
-   [U8_DIV_EQ]  Theorem
+   [u8_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
@@ -1569,7 +1702,7 @@ sig
           ∃z. u8_div x y = Return z ∧
               u8_to_int z = u8_to_int x / u8_to_int y
    
-   [U8_MUL_EQ]  Theorem
+   [u8_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
@@ -1579,7 +1712,7 @@ sig
           ∃z. u8_mul x y = Return z ∧
               u8_to_int z = u8_to_int x * u8_to_int y
    
-   [U8_REM_EQ]  Theorem
+   [u8_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
@@ -1589,7 +1722,7 @@ sig
           ∃z. u8_rem x y = Return z ∧
               u8_to_int z = int_rem (u8_to_int x) (u8_to_int y)
    
-   [U8_SUB_EQ]  Theorem
+   [u8_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
@@ -1599,7 +1732,25 @@ sig
           ∃z. u8_sub x y = Return z ∧
               u8_to_int z = u8_to_int x − u8_to_int y
    
-   [USIZE_ADD_EQ]  Theorem
+   [update_ind]  Theorem
+      
+      ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧
+            (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒
+            ∀v v1 v2. P v v1 v2
+   
+   [update_len]  Theorem
+      
+      ⊢ ∀ls i y. len (update ls i y) = len ls
+   
+   [update_spec]  Theorem
+      
+      ⊢ ∀ls i y.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧
+          ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+   
+   [usize_add_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
@@ -1610,7 +1761,7 @@ sig
           ∃z. usize_add x y = Return z ∧
               usize_to_int z = usize_to_int x + usize_to_int y
    
-   [USIZE_DIV_EQ]  Theorem
+   [usize_div_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
@@ -1620,7 +1771,7 @@ sig
           ∃z. usize_div x y = Return z ∧
               usize_to_int z = usize_to_int x / usize_to_int y
    
-   [USIZE_MUL_EQ]  Theorem
+   [usize_mul_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
@@ -1631,7 +1782,7 @@ sig
           ∃z. usize_mul x y = Return z ∧
               usize_to_int z = usize_to_int x * usize_to_int y
    
-   [USIZE_REM_EQ]  Theorem
+   [usize_rem_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
@@ -1641,7 +1792,7 @@ sig
           ∃z. usize_rem x y = Return z ∧
               usize_to_int z = int_rem (usize_to_int x) (usize_to_int y)
    
-   [USIZE_SUB_EQ]  Theorem
+   [usize_sub_eq]  Theorem
       
       [oracles: DISK_THM]
       [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
@@ -1651,169 +1802,16 @@ sig
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_to_int y
    
-   [USIZE_TO_INT_INJ]  Theorem
+   [usize_to_int_inj]  Theorem
       
       [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
       ⊢ ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
    
-   [USIZE_TO_INT_NEQ_INJ]  Theorem
+   [usize_to_int_neq_inj]  Theorem
       
       [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
       ⊢ ∀i j. i ≠ j ⇒ usize_to_int i ≠ usize_to_int j
    
-   [VEC_NEW_SPEC]  Theorem
-      
-      [oracles: DISK_THM] [axioms: usize_bounds, MK_VEC_SPEC] []
-      ⊢ vec_to_list vec_new = []
-   
-   [VEC_TO_LIST_INT_BOUNDS]  Theorem
-      
-      [oracles: DISK_THM] [axioms: usize_bounds, VEC_TO_LIST_BOUNDS] []
-      ⊢ ∀v. 0 ≤ &LENGTH (vec_to_list v) ∧
-            &LENGTH (vec_to_list v) ≤ usize_max
-   
-   [datatype_error]  Theorem
-      
-      ⊢ DATATYPE (error Failure)
-   
-   [datatype_result]  Theorem
-      
-      ⊢ DATATYPE (result Return Fail Loop)
-   
-   [error2num_11]  Theorem
-      
-      ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a'
-   
-   [error2num_ONTO]  Theorem
-      
-      ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a
-   
-   [error2num_num2error]  Theorem
-      
-      ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r
-   
-   [error2num_thm]  Theorem
-      
-      ⊢ error2num Failure = 0
-   
-   [error_Axiom]  Theorem
-      
-      ⊢ ∀x0. ∃f. f Failure = x0
-   
-   [error_EQ_error]  Theorem
-      
-      ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a'
-   
-   [error_case_cong]  Theorem
-      
-      ⊢ ∀M M' v0.
-          M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒
-          (case M of Failure => v0) = case M' of Failure => v0'
-   
-   [error_case_def]  Theorem
-      
-      ⊢ ∀v0. (case Failure of Failure => v0) = v0
-   
-   [error_case_eq]  Theorem
-      
-      ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v
-   
-   [error_induction]  Theorem
-      
-      ⊢ ∀P. P Failure ⇒ ∀a. P a
-   
-   [error_nchotomy]  Theorem
-      
-      ⊢ ∀a. a = Failure
-   
-   [index_update_diff]  Theorem
-      
-      ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y
-   
-   [index_update_same]  Theorem
-      
-      ⊢ ∀ls i j y.
-          0 ≤ i ⇒
-          i < len ls ⇒
-          j < len ls ⇒
-          j ≠ i ⇒
-          index j (update ls i y) = index j ls
-   
-   [int_induction]  Theorem
-      
-      ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i
-   
-   [num2error_11]  Theorem
-      
-      ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
-   
-   [num2error_ONTO]  Theorem
-      
-      ⊢ ∀a. ∃r. a = num2error r ∧ r < 1
-   
-   [num2error_error2num]  Theorem
-      
-      ⊢ ∀a. num2error (error2num a) = a
-   
-   [num2error_thm]  Theorem
-      
-      ⊢ num2error 0 = Failure
-   
-   [result_11]  Theorem
-      
-      ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧
-        ∀a a'. Fail a = Fail a' ⇔ a = a'
-   
-   [result_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1 f2. ∃fn.
-          (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧
-          fn Loop = f2
-   
-   [result_case_cong]  Theorem
-      
-      ⊢ ∀M M' f f1 v.
-          M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧
-          (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒
-          result_CASE M f f1 v = result_CASE M' f' f1' v'
-   
-   [result_case_eq]  Theorem
-      
-      ⊢ result_CASE x f f1 v = v' ⇔
-        (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨
-        x = Loop ∧ v = v'
-   
-   [result_distinct]  Theorem
-      
-      ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧
-        ∀a. Fail a ≠ Loop
-   
-   [result_induction]  Theorem
-      
-      ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r
-   
-   [result_nchotomy]  Theorem
-      
-      ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
-   
-   [update_ind]  Theorem
-      
-      ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧
-            (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒
-            ∀v v1 v2. P v v1 v2
-   
-   [update_len]  Theorem
-      
-      ⊢ ∀ls i y. len (update ls i y) = len ls
-   
-   [update_spec]  Theorem
-      
-      ⊢ ∀ls i y.
-          0 ≤ i ⇒
-          i < len ls ⇒
-          len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧
-          ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
-   
    [vec_insert_back_spec]  Theorem
       
       [oracles: DISK_THM, cheat]