Use lower case in the names for the HOL4 backend

1 files changed, 401 insertions, 403 deletions

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]