Rename some subdirectories for consistency

7 files changed, 0 insertions, 1871 deletions

diff --git a/tests/hol4/hashmap_on_disk/Holmakefile b/tests/hol4/hashmap_on_disk/Holmakefile
deleted file mode 100644
index 3c4b8973..00000000
--- a/tests/hol4/hashmap_on_disk/Holmakefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# This file was automatically generated - modify ../Holmakefile.template instead
-INCLUDES =  ../../../backends/hol4
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
deleted file mode 100644
index c1e30aa6..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ /dev/null
@@ -1,647 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: function definitions *)
-open primitivesLib divDefLib
-open hashmapMain_TypesTheory hashmapMain_OpaqueTheory
-
-val _ = new_theory "hashmapMain_Funs"
-
-
-val hashmap_hash_key_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::hash_key]: forward function *)
-  hashmap_hash_key_fwd (k : usize) : usize result =
-    Return k
-’
-
-val [hashmap_hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
-  hashmap_hash_map_allocate_slots_loop_fwd
-    (slots : 't hashmap_list_t vec) (n : usize) :
-    't hashmap_list_t vec result
-    =
-    if usize_gt n (int_to_usize 0)
-    then (
-      do
-      slots0 <- vec_push_back slots HashmapListNil;
-      n0 <- usize_sub n (int_to_usize 1);
-      hashmap_hash_map_allocate_slots_loop_fwd slots0 n0
-      od)
-    else Return slots
-’
-
-val hashmap_hash_map_allocate_slots_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *)
-  hashmap_hash_map_allocate_slots_fwd
-    (slots : 't hashmap_list_t vec) (n : usize) :
-    't hashmap_list_t vec result
-    =
-    hashmap_hash_map_allocate_slots_loop_fwd slots n
-’
-
-val hashmap_hash_map_new_with_capacity_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *)
-  hashmap_hash_map_new_with_capacity_fwd
-    (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) :
-    't hashmap_hash_map_t result
-    =
-    let v = vec_new in
-    do
-    slots <- hashmap_hash_map_allocate_slots_fwd v capacity;
-    i <- usize_mul capacity max_load_dividend;
-    i0 <- usize_div i max_load_divisor;
-    Return
-      (<|
-         hashmap_hash_map_num_entries := (int_to_usize 0);
-         hashmap_hash_map_max_load_factor :=
-           (max_load_dividend, max_load_divisor);
-         hashmap_hash_map_max_load := i0;
-         hashmap_hash_map_slots := slots
-         |>)
-    od
-’
-
-val hashmap_hash_map_new_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *)
-  hashmap_hash_map_new_fwd : 't hashmap_hash_map_t result =
-    hashmap_hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4)
-      (int_to_usize 5)
-’
-
-val [hashmap_hash_map_clear_loop_fwd_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_clear_loop_fwd_back
-    (slots : 't hashmap_list_t vec) (i : usize) :
-    't hashmap_list_t vec result
-    =
-    let i0 = vec_len slots in
-    if usize_lt i i0
-    then (
-      do
-      i1 <- usize_add i (int_to_usize 1);
-      slots0 <- vec_index_mut_back slots i HashmapListNil;
-      hashmap_hash_map_clear_loop_fwd_back slots0 i1
-      od)
-    else Return slots
-’
-
-val hashmap_hash_map_clear_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_clear_fwd_back
-    (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
-    do
-    v <-
-      hashmap_hash_map_clear_loop_fwd_back self.hashmap_hash_map_slots
-        (int_to_usize 0);
-    Return
-      (self
-         with
-         <|
-         hashmap_hash_map_num_entries := (int_to_usize 0);
-         hashmap_hash_map_slots := v
-         |>)
-    od
-’
-
-val hashmap_hash_map_len_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *)
-  hashmap_hash_map_len_fwd (self : 't hashmap_hash_map_t) : usize result =
-    Return self.hashmap_hash_map_num_entries
-’
-
-val [hashmap_hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
-  hashmap_hash_map_insert_in_list_loop_fwd
-    (key : usize) (value : 't) (ls : 't hashmap_list_t) : bool result =
-    (case ls of
-    | HashmapListCons ckey cvalue tl =>
-      if ckey = key
-      then Return F
-      else hashmap_hash_map_insert_in_list_loop_fwd key value tl
-    | HashmapListNil => Return T)
-’
-
-val hashmap_hash_map_insert_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *)
-  hashmap_hash_map_insert_in_list_fwd
-    (key : usize) (value : 't) (ls : 't hashmap_list_t) : bool result =
-    hashmap_hash_map_insert_in_list_loop_fwd key value ls
-’
-
-val [hashmap_hash_map_insert_in_list_loop_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
-  hashmap_hash_map_insert_in_list_loop_back
-    (key : usize) (value : 't) (ls : 't hashmap_list_t) :
-    't hashmap_list_t result
-    =
-    (case ls of
-    | HashmapListCons ckey cvalue tl =>
-      if ckey = key
-      then Return (HashmapListCons ckey value tl)
-      else (
-        do
-        tl0 <- hashmap_hash_map_insert_in_list_loop_back key value tl;
-        Return (HashmapListCons ckey cvalue tl0)
-        od)
-    | HashmapListNil =>
-      let l = HashmapListNil in Return (HashmapListCons key value l))
-’
-
-val hashmap_hash_map_insert_in_list_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
-  hashmap_hash_map_insert_in_list_back
-    (key : usize) (value : 't) (ls : 't hashmap_list_t) :
-    't hashmap_list_t result
-    =
-    hashmap_hash_map_insert_in_list_loop_back key value ls
-’
-
-val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_insert_no_resize_fwd_back
-    (self : 't hashmap_hash_map_t) (key : usize) (value : 't) :
-    't hashmap_hash_map_t result
-    =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-    inserted <- hashmap_hash_map_insert_in_list_fwd key value l;
-    if inserted
-    then (
-      do
-      i0 <- usize_add self.hashmap_hash_map_num_entries (int_to_usize 1);
-      l0 <- hashmap_hash_map_insert_in_list_back key value l;
-      v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
-      Return
-        (self
-           with
-           <|
-           hashmap_hash_map_num_entries := i0; hashmap_hash_map_slots := v
-           |>)
-      od)
-    else (
-      do
-      l0 <- hashmap_hash_map_insert_in_list_back key value l;
-      v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
-      Return (self with <| hashmap_hash_map_slots := v |>)
-      od)
-    od
-    od
-’
-
-val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_move_elements_from_list_loop_fwd_back
-    (ntable : 't hashmap_hash_map_t) (ls : 't hashmap_list_t) :
-    't hashmap_hash_map_t result
-    =
-    (case ls of
-    | HashmapListCons k v tl =>
-      do
-      ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back ntable k v;
-      hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable0 tl
-      od
-    | HashmapListNil => Return ntable)
-’
-
-val hashmap_hash_map_move_elements_from_list_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_move_elements_from_list_fwd_back
-    (ntable : 't hashmap_hash_map_t) (ls : 't hashmap_list_t) :
-    't hashmap_hash_map_t result
-    =
-    hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls
-’
-
-val [hashmap_hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_move_elements_loop_fwd_back
-    (ntable : 't hashmap_hash_map_t) (slots : 't hashmap_list_t vec)
-    (i : usize) :
-    ('t hashmap_hash_map_t # 't hashmap_list_t vec) result
-    =
-    let i0 = vec_len slots in
-    if usize_lt i i0
-    then (
-      do
-      l <- vec_index_mut_fwd slots i;
-      let ls = mem_replace_fwd l HashmapListNil in
-      do
-      ntable0 <- hashmap_hash_map_move_elements_from_list_fwd_back ntable ls;
-      i1 <- usize_add i (int_to_usize 1);
-      let l0 = mem_replace_back l HashmapListNil in
-      do
-      slots0 <- vec_index_mut_back slots i l0;
-      hashmap_hash_map_move_elements_loop_fwd_back ntable0 slots0 i1
-      od
-      od
-      od)
-    else Return (ntable, slots)
-’
-
-val hashmap_hash_map_move_elements_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_move_elements_fwd_back
-    (ntable : 't hashmap_hash_map_t) (slots : 't hashmap_list_t vec)
-    (i : usize) :
-    ('t hashmap_hash_map_t # 't hashmap_list_t vec) result
-    =
-    hashmap_hash_map_move_elements_loop_fwd_back ntable slots i
-’
-
-val hashmap_hash_map_try_resize_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_try_resize_fwd_back
-    (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
-    do
-    max_usize <- mk_usize (u32_to_int core_u32_max);
-    let capacity = vec_len self.hashmap_hash_map_slots in
-    do
-    n1 <- usize_div max_usize (int_to_usize 2);
-    let (i, i0) = self.hashmap_hash_map_max_load_factor in
-    do
-    i1 <- usize_div n1 i;
-    if usize_le capacity i1
-    then (
-      do
-      i2 <- usize_mul capacity (int_to_usize 2);
-      ntable <- hashmap_hash_map_new_with_capacity_fwd i2 i i0;
-      (ntable0, _) <-
-        hashmap_hash_map_move_elements_fwd_back ntable
-          self.hashmap_hash_map_slots (int_to_usize 0);
-      Return
-        (ntable0
-           with
-           <|
-           hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries;
-           hashmap_hash_map_max_load_factor := (i, i0)
-           |>)
-      od)
-    else Return (self with <| hashmap_hash_map_max_load_factor := (i, i0) |>)
-    od
-    od
-    od
-’
-
-val hashmap_hash_map_insert_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  hashmap_hash_map_insert_fwd_back
-    (self : 't hashmap_hash_map_t) (key : usize) (value : 't) :
-    't hashmap_hash_map_t result
-    =
-    do
-    self0 <- hashmap_hash_map_insert_no_resize_fwd_back self key value;
-    i <- hashmap_hash_map_len_fwd self0;
-    if usize_gt i self0.hashmap_hash_map_max_load
-    then hashmap_hash_map_try_resize_fwd_back self0
-    else Return self0
-    od
-’
-
-val [hashmap_hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
-  hashmap_hash_map_contains_key_in_list_loop_fwd
-    (key : usize) (ls : 't hashmap_list_t) : bool result =
-    (case ls of
-    | HashmapListCons ckey t tl =>
-      if ckey = key
-      then Return T
-      else hashmap_hash_map_contains_key_in_list_loop_fwd key tl
-    | HashmapListNil => Return F)
-’
-
-val hashmap_hash_map_contains_key_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
-  hashmap_hash_map_contains_key_in_list_fwd
-    (key : usize) (ls : 't hashmap_list_t) : bool result =
-    hashmap_hash_map_contains_key_in_list_loop_fwd key ls
-’
-
-val hashmap_hash_map_contains_key_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *)
-  hashmap_hash_map_contains_key_fwd
-    (self : 't hashmap_hash_map_t) (key : usize) : bool result =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod;
-    hashmap_hash_map_contains_key_in_list_fwd key l
-    od
-    od
-’
-
-val [hashmap_hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
-  hashmap_hash_map_get_in_list_loop_fwd
-    (key : usize) (ls : 't hashmap_list_t) : 't result =
-    (case ls of
-    | HashmapListCons ckey cvalue tl =>
-      if ckey = key
-      then Return cvalue
-      else hashmap_hash_map_get_in_list_loop_fwd key tl
-    | HashmapListNil => Fail Failure)
-’
-
-val hashmap_hash_map_get_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *)
-  hashmap_hash_map_get_in_list_fwd
-    (key : usize) (ls : 't hashmap_list_t) : 't result =
-    hashmap_hash_map_get_in_list_loop_fwd key ls
-’
-
-val hashmap_hash_map_get_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *)
-  hashmap_hash_map_get_fwd
-    (self : 't hashmap_hash_map_t) (key : usize) : 't result =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod;
-    hashmap_hash_map_get_in_list_fwd key l
-    od
-    od
-’
-
-val [hashmap_hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
-  hashmap_hash_map_get_mut_in_list_loop_fwd
-    (ls : 't hashmap_list_t) (key : usize) : 't result =
-    (case ls of
-    | HashmapListCons ckey cvalue tl =>
-      if ckey = key
-      then Return cvalue
-      else hashmap_hash_map_get_mut_in_list_loop_fwd tl key
-    | HashmapListNil => Fail Failure)
-’
-
-val hashmap_hash_map_get_mut_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
-  hashmap_hash_map_get_mut_in_list_fwd
-    (ls : 't hashmap_list_t) (key : usize) : 't result =
-    hashmap_hash_map_get_mut_in_list_loop_fwd ls key
-’
-
-val [hashmap_hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
-  hashmap_hash_map_get_mut_in_list_loop_back
-    (ls : 't hashmap_list_t) (key : usize) (ret : 't) :
-    't hashmap_list_t result
-    =
-    (case ls of
-    | HashmapListCons ckey cvalue tl =>
-      if ckey = key
-      then Return (HashmapListCons ckey ret tl)
-      else (
-        do
-        tl0 <- hashmap_hash_map_get_mut_in_list_loop_back tl key ret;
-        Return (HashmapListCons ckey cvalue tl0)
-        od)
-    | HashmapListNil => Fail Failure)
-’
-
-val hashmap_hash_map_get_mut_in_list_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
-  hashmap_hash_map_get_mut_in_list_back
-    (ls : 't hashmap_list_t) (key : usize) (ret : 't) :
-    't hashmap_list_t result
-    =
-    hashmap_hash_map_get_mut_in_list_loop_back ls key ret
-’
-
-val hashmap_hash_map_get_mut_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *)
-  hashmap_hash_map_get_mut_fwd
-    (self : 't hashmap_hash_map_t) (key : usize) : 't result =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-    hashmap_hash_map_get_mut_in_list_fwd l key
-    od
-    od
-’
-
-val hashmap_hash_map_get_mut_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *)
-  hashmap_hash_map_get_mut_back
-    (self : 't hashmap_hash_map_t) (key : usize) (ret : 't) :
-    't hashmap_hash_map_t result
-    =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-    l0 <- hashmap_hash_map_get_mut_in_list_back l key ret;
-    v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
-    Return (self with <| hashmap_hash_map_slots := v |>)
-    od
-    od
-’
-
-val [hashmap_hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
-  hashmap_hash_map_remove_from_list_loop_fwd
-    (key : usize) (ls : 't hashmap_list_t) : 't option result =
-    (case ls of
-    | HashmapListCons ckey t tl =>
-      if ckey = key
-      then
-        let mv_ls = mem_replace_fwd (HashmapListCons ckey t tl) HashmapListNil
-          in
-        (case mv_ls of
-        | HashmapListCons i cvalue tl0 => Return (SOME cvalue)
-        | HashmapListNil => Fail Failure)
-      else hashmap_hash_map_remove_from_list_loop_fwd key tl
-    | HashmapListNil => Return NONE)
-’
-
-val hashmap_hash_map_remove_from_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *)
-  hashmap_hash_map_remove_from_list_fwd
-    (key : usize) (ls : 't hashmap_list_t) : 't option result =
-    hashmap_hash_map_remove_from_list_loop_fwd key ls
-’
-
-val [hashmap_hash_map_remove_from_list_loop_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
-  hashmap_hash_map_remove_from_list_loop_back
-    (key : usize) (ls : 't hashmap_list_t) : 't hashmap_list_t result =
-    (case ls of
-    | HashmapListCons ckey t tl =>
-      if ckey = key
-      then
-        let mv_ls = mem_replace_fwd (HashmapListCons ckey t tl) HashmapListNil
-          in
-        (case mv_ls of
-        | HashmapListCons i cvalue tl0 => Return tl0
-        | HashmapListNil => Fail Failure)
-      else (
-        do
-        tl0 <- hashmap_hash_map_remove_from_list_loop_back key tl;
-        Return (HashmapListCons ckey t tl0)
-        od)
-    | HashmapListNil => Return HashmapListNil)
-’
-
-val hashmap_hash_map_remove_from_list_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
-  hashmap_hash_map_remove_from_list_back
-    (key : usize) (ls : 't hashmap_list_t) : 't hashmap_list_t result =
-    hashmap_hash_map_remove_from_list_loop_back key ls
-’
-
-val hashmap_hash_map_remove_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *)
-  hashmap_hash_map_remove_fwd
-    (self : 't hashmap_hash_map_t) (key : usize) : 't option result =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-    x <- hashmap_hash_map_remove_from_list_fwd key l;
-    (case x of
-    | NONE => Return NONE
-    | SOME x0 =>
-      do
-      _ <- usize_sub self.hashmap_hash_map_num_entries (int_to_usize 1);
-      Return (SOME x0)
-      od)
-    od
-    od
-’
-
-val hashmap_hash_map_remove_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *)
-  hashmap_hash_map_remove_back
-    (self : 't hashmap_hash_map_t) (key : usize) :
-    't hashmap_hash_map_t result
-    =
-    do
-    hash <- hashmap_hash_key_fwd key;
-    let i = vec_len self.hashmap_hash_map_slots in
-    do
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-    x <- hashmap_hash_map_remove_from_list_fwd key l;
-    (case x of
-    | NONE =>
-      do
-      l0 <- hashmap_hash_map_remove_from_list_back key l;
-      v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
-      Return (self with <| hashmap_hash_map_slots := v |>)
-      od
-    | SOME x0 =>
-      do
-      i0 <- usize_sub self.hashmap_hash_map_num_entries (int_to_usize 1);
-      l0 <- hashmap_hash_map_remove_from_list_back key l;
-      v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
-      Return
-        (self
-           with
-           <|
-           hashmap_hash_map_num_entries := i0; hashmap_hash_map_slots := v
-           |>)
-      od)
-    od
-    od
-’
-
-val hashmap_test1_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::test1]: forward function *)
-  hashmap_test1_fwd : unit result =
-    do
-    hm <- hashmap_hash_map_new_fwd;
-    hm0 <-
-      hashmap_hash_map_insert_fwd_back hm (int_to_usize 0) (int_to_u64 42);
-    hm1 <-
-      hashmap_hash_map_insert_fwd_back hm0 (int_to_usize 128) (int_to_u64 18);
-    hm2 <-
-      hashmap_hash_map_insert_fwd_back hm1 (int_to_usize 1024) (int_to_u64 138);
-    hm3 <-
-      hashmap_hash_map_insert_fwd_back hm2 (int_to_usize 1056) (int_to_u64 256);
-    i <- hashmap_hash_map_get_fwd hm3 (int_to_usize 128);
-    if ~ (i = int_to_u64 18)
-    then Fail Failure
-    else (
-      do
-      hm4 <-
-        hashmap_hash_map_get_mut_back hm3 (int_to_usize 1024) (int_to_u64 56);
-      i0 <- hashmap_hash_map_get_fwd hm4 (int_to_usize 1024);
-      if ~ (i0 = int_to_u64 56)
-      then Fail Failure
-      else (
-        do
-        x <- hashmap_hash_map_remove_fwd hm4 (int_to_usize 1024);
-        (case x of
-        | NONE => Fail Failure
-        | SOME x0 =>
-          if ~ (x0 = int_to_u64 56)
-          then Fail Failure
-          else (
-            do
-            hm5 <- hashmap_hash_map_remove_back hm4 (int_to_usize 1024);
-            i1 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 0);
-            if ~ (i1 = int_to_u64 42)
-            then Fail Failure
-            else (
-              do
-              i2 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 128);
-              if ~ (i2 = int_to_u64 18)
-              then Fail Failure
-              else (
-                do
-                i3 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 1056);
-                if ~ (i3 = int_to_u64 256) then Fail Failure else Return ()
-                od)
-              od)
-            od))
-        od)
-      od)
-    od
-’
-
-(** Unit test for [hashmap_main::hashmap::test1] *)
-val _ = assert_return (“hashmap_test1_fwd”)
-
-val insert_on_disk_fwd_def = Define ‘
-  (** [hashmap_main::insert_on_disk]: forward function *)
-  insert_on_disk_fwd
-    (key : usize) (value : u64) (st : state) : (state # unit) result =
-    do
-    (st0, hm) <- hashmap_utils_deserialize_fwd st;
-    hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
-    (st1, _) <- hashmap_utils_serialize_fwd hm0 st0;
-    Return (st1, ())
-    od
-’
-
-val main_fwd_def = Define ‘
-  (** [hashmap_main::main]: forward function *)
-  main_fwd : unit result =
-    Return ()
-’
-
-(** Unit test for [hashmap_main::main] *)
-val _ = assert_return (“main_fwd”)
-
-val _ = export_theory ()
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
deleted file mode 100644
index d4e43d9a..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ /dev/null
@@ -1,598 +0,0 @@
-signature hashmapMain_FunsTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val hashmap_hash_key_fwd_def : thm
-    val hashmap_hash_map_allocate_slots_fwd_def : thm
-    val hashmap_hash_map_allocate_slots_loop_fwd_def : thm
-    val hashmap_hash_map_clear_fwd_back_def : thm
-    val hashmap_hash_map_clear_loop_fwd_back_def : thm
-    val hashmap_hash_map_contains_key_fwd_def : thm
-    val hashmap_hash_map_contains_key_in_list_fwd_def : thm
-    val hashmap_hash_map_contains_key_in_list_loop_fwd_def : thm
-    val hashmap_hash_map_get_fwd_def : thm
-    val hashmap_hash_map_get_in_list_fwd_def : thm
-    val hashmap_hash_map_get_in_list_loop_fwd_def : thm
-    val hashmap_hash_map_get_mut_back_def : thm
-    val hashmap_hash_map_get_mut_fwd_def : thm
-    val hashmap_hash_map_get_mut_in_list_back_def : thm
-    val hashmap_hash_map_get_mut_in_list_fwd_def : thm
-    val hashmap_hash_map_get_mut_in_list_loop_back_def : thm
-    val hashmap_hash_map_get_mut_in_list_loop_fwd_def : thm
-    val hashmap_hash_map_insert_fwd_back_def : thm
-    val hashmap_hash_map_insert_in_list_back_def : thm
-    val hashmap_hash_map_insert_in_list_fwd_def : thm
-    val hashmap_hash_map_insert_in_list_loop_back_def : thm
-    val hashmap_hash_map_insert_in_list_loop_fwd_def : thm
-    val hashmap_hash_map_insert_no_resize_fwd_back_def : thm
-    val hashmap_hash_map_len_fwd_def : thm
-    val hashmap_hash_map_move_elements_from_list_fwd_back_def : thm
-    val hashmap_hash_map_move_elements_from_list_loop_fwd_back_def : thm
-    val hashmap_hash_map_move_elements_fwd_back_def : thm
-    val hashmap_hash_map_move_elements_loop_fwd_back_def : thm
-    val hashmap_hash_map_new_fwd_def : thm
-    val hashmap_hash_map_new_with_capacity_fwd_def : thm
-    val hashmap_hash_map_remove_back_def : thm
-    val hashmap_hash_map_remove_from_list_back_def : thm
-    val hashmap_hash_map_remove_from_list_fwd_def : thm
-    val hashmap_hash_map_remove_from_list_loop_back_def : thm
-    val hashmap_hash_map_remove_from_list_loop_fwd_def : thm
-    val hashmap_hash_map_remove_fwd_def : thm
-    val hashmap_hash_map_try_resize_fwd_back_def : thm
-    val hashmap_test1_fwd_def : thm
-    val insert_on_disk_fwd_def : thm
-    val main_fwd_def : thm
-  
-  val hashmapMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [hashmapMain_Opaque] Parent theory of "hashmapMain_Funs"
-   
-   [hashmap_hash_key_fwd_def]  Definition
-      
-      ⊢ ∀k. hashmap_hash_key_fwd k = Return k
-   
-   [hashmap_hash_map_allocate_slots_fwd_def]  Definition
-      
-      ⊢ ∀slots n.
-          hashmap_hash_map_allocate_slots_fwd slots n =
-          hashmap_hash_map_allocate_slots_loop_fwd slots n
-   
-   [hashmap_hash_map_allocate_slots_loop_fwd_def]  Definition
-      
-      ⊢ ∀slots n.
-          hashmap_hash_map_allocate_slots_loop_fwd slots n =
-          if usize_gt n (int_to_usize 0) then
-            do
-              slots0 <- vec_push_back slots HashmapListNil;
-              n0 <- usize_sub n (int_to_usize 1);
-              hashmap_hash_map_allocate_slots_loop_fwd slots0 n0
-            od
-          else Return slots
-   
-   [hashmap_hash_map_clear_fwd_back_def]  Definition
-      
-      ⊢ ∀self.
-          hashmap_hash_map_clear_fwd_back self =
-          do
-            v <-
-              hashmap_hash_map_clear_loop_fwd_back
-                self.hashmap_hash_map_slots (int_to_usize 0);
-            Return
-              (self with
-               <|hashmap_hash_map_num_entries := int_to_usize 0;
-                 hashmap_hash_map_slots := v|>)
-          od
-   
-   [hashmap_hash_map_clear_loop_fwd_back_def]  Definition
-      
-      ⊢ ∀slots i.
-          hashmap_hash_map_clear_loop_fwd_back slots i =
-          (let
-             i0 = vec_len slots
-           in
-             if usize_lt i i0 then
-               do
-                 i1 <- usize_add i (int_to_usize 1);
-                 slots0 <- vec_index_mut_back slots i HashmapListNil;
-                 hashmap_hash_map_clear_loop_fwd_back slots0 i1
-               od
-             else Return slots)
-   
-   [hashmap_hash_map_contains_key_fwd_def]  Definition
-      
-      ⊢ ∀self key.
-          hashmap_hash_map_contains_key_fwd self key =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod;
-            hashmap_hash_map_contains_key_in_list_fwd key l
-          od
-   
-   [hashmap_hash_map_contains_key_in_list_fwd_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_contains_key_in_list_fwd key ls =
-          hashmap_hash_map_contains_key_in_list_loop_fwd key ls
-   
-   [hashmap_hash_map_contains_key_in_list_loop_fwd_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_contains_key_in_list_loop_fwd key ls =
-          case ls of
-            HashmapListCons ckey t tl =>
-              if ckey = key then Return T
-              else hashmap_hash_map_contains_key_in_list_loop_fwd key tl
-          | HashmapListNil => Return F
-   
-   [hashmap_hash_map_get_fwd_def]  Definition
-      
-      ⊢ ∀self key.
-          hashmap_hash_map_get_fwd self key =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod;
-            hashmap_hash_map_get_in_list_fwd key l
-          od
-   
-   [hashmap_hash_map_get_in_list_fwd_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_get_in_list_fwd key ls =
-          hashmap_hash_map_get_in_list_loop_fwd key ls
-   
-   [hashmap_hash_map_get_in_list_loop_fwd_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_get_in_list_loop_fwd key ls =
-          case ls of
-            HashmapListCons ckey cvalue tl =>
-              if ckey = key then Return cvalue
-              else hashmap_hash_map_get_in_list_loop_fwd key tl
-          | HashmapListNil => Fail Failure
-   
-   [hashmap_hash_map_get_mut_back_def]  Definition
-      
-      ⊢ ∀self key ret.
-          hashmap_hash_map_get_mut_back self key ret =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-            l0 <- hashmap_hash_map_get_mut_in_list_back l key ret;
-            v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
-            Return (self with hashmap_hash_map_slots := v)
-          od
-   
-   [hashmap_hash_map_get_mut_fwd_def]  Definition
-      
-      ⊢ ∀self key.
-          hashmap_hash_map_get_mut_fwd self key =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-            hashmap_hash_map_get_mut_in_list_fwd l key
-          od
-   
-   [hashmap_hash_map_get_mut_in_list_back_def]  Definition
-      
-      ⊢ ∀ls key ret.
-          hashmap_hash_map_get_mut_in_list_back ls key ret =
-          hashmap_hash_map_get_mut_in_list_loop_back ls key ret
-   
-   [hashmap_hash_map_get_mut_in_list_fwd_def]  Definition
-      
-      ⊢ ∀ls key.
-          hashmap_hash_map_get_mut_in_list_fwd ls key =
-          hashmap_hash_map_get_mut_in_list_loop_fwd ls key
-   
-   [hashmap_hash_map_get_mut_in_list_loop_back_def]  Definition
-      
-      ⊢ ∀ls key ret.
-          hashmap_hash_map_get_mut_in_list_loop_back ls key ret =
-          case ls of
-            HashmapListCons ckey cvalue tl =>
-              if ckey = key then Return (HashmapListCons ckey ret tl)
-              else
-                do
-                  tl0 <-
-                    hashmap_hash_map_get_mut_in_list_loop_back tl key ret;
-                  Return (HashmapListCons ckey cvalue tl0)
-                od
-          | HashmapListNil => Fail Failure
-   
-   [hashmap_hash_map_get_mut_in_list_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls key.
-          hashmap_hash_map_get_mut_in_list_loop_fwd ls key =
-          case ls of
-            HashmapListCons ckey cvalue tl =>
-              if ckey = key then Return cvalue
-              else hashmap_hash_map_get_mut_in_list_loop_fwd tl key
-          | HashmapListNil => Fail Failure
-   
-   [hashmap_hash_map_insert_fwd_back_def]  Definition
-      
-      ⊢ ∀self key value.
-          hashmap_hash_map_insert_fwd_back self key value =
-          do
-            self0 <-
-              hashmap_hash_map_insert_no_resize_fwd_back self key value;
-            i <- hashmap_hash_map_len_fwd self0;
-            if usize_gt i self0.hashmap_hash_map_max_load then
-              hashmap_hash_map_try_resize_fwd_back self0
-            else Return self0
-          od
-   
-   [hashmap_hash_map_insert_in_list_back_def]  Definition
-      
-      ⊢ ∀key value ls.
-          hashmap_hash_map_insert_in_list_back key value ls =
-          hashmap_hash_map_insert_in_list_loop_back key value ls
-   
-   [hashmap_hash_map_insert_in_list_fwd_def]  Definition
-      
-      ⊢ ∀key value ls.
-          hashmap_hash_map_insert_in_list_fwd key value ls =
-          hashmap_hash_map_insert_in_list_loop_fwd key value ls
-   
-   [hashmap_hash_map_insert_in_list_loop_back_def]  Definition
-      
-      ⊢ ∀key value ls.
-          hashmap_hash_map_insert_in_list_loop_back key value ls =
-          case ls of
-            HashmapListCons ckey cvalue tl =>
-              if ckey = key then Return (HashmapListCons ckey value tl)
-              else
-                do
-                  tl0 <-
-                    hashmap_hash_map_insert_in_list_loop_back key value tl;
-                  Return (HashmapListCons ckey cvalue tl0)
-                od
-          | HashmapListNil =>
-            (let
-               l = HashmapListNil
-             in
-               Return (HashmapListCons key value l))
-   
-   [hashmap_hash_map_insert_in_list_loop_fwd_def]  Definition
-      
-      ⊢ ∀key value ls.
-          hashmap_hash_map_insert_in_list_loop_fwd key value ls =
-          case ls of
-            HashmapListCons ckey cvalue tl =>
-              if ckey = key then Return F
-              else hashmap_hash_map_insert_in_list_loop_fwd key value tl
-          | HashmapListNil => Return T
-   
-   [hashmap_hash_map_insert_no_resize_fwd_back_def]  Definition
-      
-      ⊢ ∀self key value.
-          hashmap_hash_map_insert_no_resize_fwd_back self key value =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-            inserted <- hashmap_hash_map_insert_in_list_fwd key value l;
-            if inserted then
-              do
-                i0 <-
-                  usize_add self.hashmap_hash_map_num_entries
-                    (int_to_usize 1);
-                l0 <- hashmap_hash_map_insert_in_list_back key value l;
-                v <-
-                  vec_index_mut_back self.hashmap_hash_map_slots hash_mod
-                    l0;
-                Return
-                  (self with
-                   <|hashmap_hash_map_num_entries := i0;
-                     hashmap_hash_map_slots := v|>)
-              od
-            else
-              do
-                l0 <- hashmap_hash_map_insert_in_list_back key value l;
-                v <-
-                  vec_index_mut_back self.hashmap_hash_map_slots hash_mod
-                    l0;
-                Return (self with hashmap_hash_map_slots := v)
-              od
-          od
-   
-   [hashmap_hash_map_len_fwd_def]  Definition
-      
-      ⊢ ∀self.
-          hashmap_hash_map_len_fwd self =
-          Return self.hashmap_hash_map_num_entries
-   
-   [hashmap_hash_map_move_elements_from_list_fwd_back_def]  Definition
-      
-      ⊢ ∀ntable ls.
-          hashmap_hash_map_move_elements_from_list_fwd_back ntable ls =
-          hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls
-   
-   [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def]  Definition
-      
-      ⊢ ∀ntable ls.
-          hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls =
-          case ls of
-            HashmapListCons k v tl =>
-              do
-                ntable0 <-
-                  hashmap_hash_map_insert_no_resize_fwd_back ntable k v;
-                hashmap_hash_map_move_elements_from_list_loop_fwd_back
-                  ntable0 tl
-              od
-          | HashmapListNil => Return ntable
-   
-   [hashmap_hash_map_move_elements_fwd_back_def]  Definition
-      
-      ⊢ ∀ntable slots i.
-          hashmap_hash_map_move_elements_fwd_back ntable slots i =
-          hashmap_hash_map_move_elements_loop_fwd_back ntable slots i
-   
-   [hashmap_hash_map_move_elements_loop_fwd_back_def]  Definition
-      
-      ⊢ ∀ntable slots i.
-          hashmap_hash_map_move_elements_loop_fwd_back ntable slots i =
-          (let
-             i0 = vec_len slots
-           in
-             if usize_lt i i0 then
-               do
-                 l <- vec_index_mut_fwd slots i;
-                 ls <<- mem_replace_fwd l HashmapListNil;
-                 ntable0 <-
-                   hashmap_hash_map_move_elements_from_list_fwd_back ntable
-                     ls;
-                 i1 <- usize_add i (int_to_usize 1);
-                 l0 <<- mem_replace_back l HashmapListNil;
-                 slots0 <- vec_index_mut_back slots i l0;
-                 hashmap_hash_map_move_elements_loop_fwd_back ntable0
-                   slots0 i1
-               od
-             else Return (ntable,slots))
-   
-   [hashmap_hash_map_new_fwd_def]  Definition
-      
-      ⊢ hashmap_hash_map_new_fwd =
-        hashmap_hash_map_new_with_capacity_fwd (int_to_usize 32)
-          (int_to_usize 4) (int_to_usize 5)
-   
-   [hashmap_hash_map_new_with_capacity_fwd_def]  Definition
-      
-      ⊢ ∀capacity max_load_dividend max_load_divisor.
-          hashmap_hash_map_new_with_capacity_fwd capacity max_load_dividend
-            max_load_divisor =
-          (let
-             v = vec_new
-           in
-             do
-               slots <- hashmap_hash_map_allocate_slots_fwd v capacity;
-               i <- usize_mul capacity max_load_dividend;
-               i0 <- usize_div i max_load_divisor;
-               Return
-                 <|hashmap_hash_map_num_entries := int_to_usize 0;
-                   hashmap_hash_map_max_load_factor :=
-                     (max_load_dividend,max_load_divisor);
-                   hashmap_hash_map_max_load := i0;
-                   hashmap_hash_map_slots := slots|>
-             od)
-   
-   [hashmap_hash_map_remove_back_def]  Definition
-      
-      ⊢ ∀self key.
-          hashmap_hash_map_remove_back self key =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-            x <- hashmap_hash_map_remove_from_list_fwd key l;
-            case x of
-              NONE =>
-                do
-                  l0 <- hashmap_hash_map_remove_from_list_back key l;
-                  v <-
-                    vec_index_mut_back self.hashmap_hash_map_slots hash_mod
-                      l0;
-                  Return (self with hashmap_hash_map_slots := v)
-                od
-            | SOME x0 =>
-              do
-                i0 <-
-                  usize_sub self.hashmap_hash_map_num_entries
-                    (int_to_usize 1);
-                l0 <- hashmap_hash_map_remove_from_list_back key l;
-                v <-
-                  vec_index_mut_back self.hashmap_hash_map_slots hash_mod
-                    l0;
-                Return
-                  (self with
-                   <|hashmap_hash_map_num_entries := i0;
-                     hashmap_hash_map_slots := v|>)
-              od
-          od
-   
-   [hashmap_hash_map_remove_from_list_back_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_remove_from_list_back key ls =
-          hashmap_hash_map_remove_from_list_loop_back key ls
-   
-   [hashmap_hash_map_remove_from_list_fwd_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_remove_from_list_fwd key ls =
-          hashmap_hash_map_remove_from_list_loop_fwd key ls
-   
-   [hashmap_hash_map_remove_from_list_loop_back_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_remove_from_list_loop_back key ls =
-          case ls of
-            HashmapListCons ckey t tl =>
-              if ckey = key then
-                (let
-                   mv_ls =
-                     mem_replace_fwd (HashmapListCons ckey t tl)
-                       HashmapListNil
-                 in
-                   case mv_ls of
-                     HashmapListCons i cvalue tl0 => Return tl0
-                   | HashmapListNil => Fail Failure)
-              else
-                do
-                  tl0 <- hashmap_hash_map_remove_from_list_loop_back key tl;
-                  Return (HashmapListCons ckey t tl0)
-                od
-          | HashmapListNil => Return HashmapListNil
-   
-   [hashmap_hash_map_remove_from_list_loop_fwd_def]  Definition
-      
-      ⊢ ∀key ls.
-          hashmap_hash_map_remove_from_list_loop_fwd key ls =
-          case ls of
-            HashmapListCons ckey t tl =>
-              if ckey = key then
-                (let
-                   mv_ls =
-                     mem_replace_fwd (HashmapListCons ckey t tl)
-                       HashmapListNil
-                 in
-                   case mv_ls of
-                     HashmapListCons i cvalue tl0 => Return (SOME cvalue)
-                   | HashmapListNil => Fail Failure)
-              else hashmap_hash_map_remove_from_list_loop_fwd key tl
-          | HashmapListNil => Return NONE
-   
-   [hashmap_hash_map_remove_fwd_def]  Definition
-      
-      ⊢ ∀self key.
-          hashmap_hash_map_remove_fwd self key =
-          do
-            hash <- hashmap_hash_key_fwd key;
-            i <<- vec_len self.hashmap_hash_map_slots;
-            hash_mod <- usize_rem hash i;
-            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
-            x <- hashmap_hash_map_remove_from_list_fwd key l;
-            case x of
-              NONE => Return NONE
-            | SOME x0 =>
-              monad_ignore_bind
-                (usize_sub self.hashmap_hash_map_num_entries
-                   (int_to_usize 1)) (Return (SOME x0))
-          od
-   
-   [hashmap_hash_map_try_resize_fwd_back_def]  Definition
-      
-      ⊢ ∀self.
-          hashmap_hash_map_try_resize_fwd_back self =
-          do
-            max_usize <- mk_usize (u32_to_int core_u32_max);
-            capacity <<- vec_len self.hashmap_hash_map_slots;
-            n1 <- usize_div max_usize (int_to_usize 2);
-            (i,i0) <<- self.hashmap_hash_map_max_load_factor;
-            i1 <- usize_div n1 i;
-            if usize_le capacity i1 then
-              do
-                i2 <- usize_mul capacity (int_to_usize 2);
-                ntable <- hashmap_hash_map_new_with_capacity_fwd i2 i i0;
-                (ntable0,_) <-
-                  hashmap_hash_map_move_elements_fwd_back ntable
-                    self.hashmap_hash_map_slots (int_to_usize 0);
-                Return
-                  (ntable0 with
-                   <|hashmap_hash_map_num_entries :=
-                       self.hashmap_hash_map_num_entries;
-                     hashmap_hash_map_max_load_factor := (i,i0)|>)
-              od
-            else
-              Return (self with hashmap_hash_map_max_load_factor := (i,i0))
-          od
-   
-   [hashmap_test1_fwd_def]  Definition
-      
-      ⊢ hashmap_test1_fwd =
-        do
-          hm <- hashmap_hash_map_new_fwd;
-          hm0 <-
-            hashmap_hash_map_insert_fwd_back hm (int_to_usize 0)
-              (int_to_u64 42);
-          hm1 <-
-            hashmap_hash_map_insert_fwd_back hm0 (int_to_usize 128)
-              (int_to_u64 18);
-          hm2 <-
-            hashmap_hash_map_insert_fwd_back hm1 (int_to_usize 1024)
-              (int_to_u64 138);
-          hm3 <-
-            hashmap_hash_map_insert_fwd_back hm2 (int_to_usize 1056)
-              (int_to_u64 256);
-          i <- hashmap_hash_map_get_fwd hm3 (int_to_usize 128);
-          if i ≠ int_to_u64 18 then Fail Failure
-          else
-            do
-              hm4 <-
-                hashmap_hash_map_get_mut_back hm3 (int_to_usize 1024)
-                  (int_to_u64 56);
-              i0 <- hashmap_hash_map_get_fwd hm4 (int_to_usize 1024);
-              if i0 ≠ int_to_u64 56 then Fail Failure
-              else
-                do
-                  x <- hashmap_hash_map_remove_fwd hm4 (int_to_usize 1024);
-                  case x of
-                    NONE => Fail Failure
-                  | SOME x0 =>
-                    if x0 ≠ int_to_u64 56 then Fail Failure
-                    else
-                      do
-                        hm5 <-
-                          hashmap_hash_map_remove_back hm4
-                            (int_to_usize 1024);
-                        i1 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 0);
-                        if i1 ≠ int_to_u64 42 then Fail Failure
-                        else
-                          do
-                            i2 <-
-                              hashmap_hash_map_get_fwd hm5
-                                (int_to_usize 128);
-                            if i2 ≠ int_to_u64 18 then Fail Failure
-                            else
-                              do
-                                i3 <-
-                                  hashmap_hash_map_get_fwd hm5
-                                    (int_to_usize 1056);
-                                if i3 ≠ int_to_u64 256 then Fail Failure
-                                else Return ()
-                              od
-                          od
-                      od
-                od
-            od
-        od
-   
-   [insert_on_disk_fwd_def]  Definition
-      
-      ⊢ ∀key value st.
-          insert_on_disk_fwd key value st =
-          do
-            (st0,hm) <- hashmap_utils_deserialize_fwd st;
-            hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
-            (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
-            Return (st1,())
-          od
-   
-   [main_fwd_def]  Definition
-      
-      ⊢ main_fwd = Return ()
-   
-   
-*)
-end
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
deleted file mode 100644
index f7221d92..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ /dev/null
@@ -1,15 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: external function declarations *)
-open primitivesLib divDefLib
-open hashmapMain_TypesTheory
-
-val _ = new_theory "hashmapMain_Opaque"
-
-
-(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
-  “:state -> (state # u64 hashmap_hash_map_t) result”)
-
-(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
-  “:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
-
-val _ = export_theory ()
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig
deleted file mode 100644
index f7373609..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig
+++ /dev/null
@@ -1,11 +0,0 @@
-signature hashmapMain_OpaqueTheory =
-sig
-  type thm = Thm.thm
-  
-  val hashmapMain_Opaque_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [hashmapMain_Types] Parent theory of "hashmapMain_Opaque"
-   
-   
-*)
-end
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml
deleted file mode 100644
index 3f8ca9b9..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml
+++ /dev/null
@@ -1,27 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: type definitions *)
-open primitivesLib divDefLib
-
-val _ = new_theory "hashmapMain_Types"
-
-
-Datatype:
-  (** [hashmap_main::hashmap::List] *)
-  hashmap_list_t = | HashmapListCons usize 't hashmap_list_t | HashmapListNil
-End
-
-Datatype:
-  (** [hashmap_main::hashmap::HashMap] *)
-  hashmap_hash_map_t =
-  <|
-    hashmap_hash_map_num_entries : usize;
-    hashmap_hash_map_max_load_factor : (usize # usize);
-    hashmap_hash_map_max_load : usize;
-    hashmap_hash_map_slots : 't hashmap_list_t vec;
-  |>
-End
-
-(** The state type used in the state-error monad *)
-val _ = new_type ("state", 0)
-
-val _ = export_theory ()
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
deleted file mode 100644
index a3e770ea..00000000
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ /dev/null
@@ -1,568 +0,0 @@
-signature hashmapMain_TypesTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val hashmap_hash_map_t_TY_DEF : thm
-    val hashmap_hash_map_t_case_def : thm
-    val hashmap_hash_map_t_hashmap_hash_map_max_load : thm
-    val hashmap_hash_map_t_hashmap_hash_map_max_load_factor : thm
-    val hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd : thm
-    val hashmap_hash_map_t_hashmap_hash_map_max_load_fupd : thm
-    val hashmap_hash_map_t_hashmap_hash_map_num_entries : thm
-    val hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd : thm
-    val hashmap_hash_map_t_hashmap_hash_map_slots : thm
-    val hashmap_hash_map_t_hashmap_hash_map_slots_fupd : thm
-    val hashmap_hash_map_t_size_def : thm
-    val hashmap_list_t_TY_DEF : thm
-    val hashmap_list_t_case_def : thm
-    val hashmap_list_t_size_def : thm
-  
-  (*  Theorems  *)
-    val EXISTS_hashmap_hash_map_t : thm
-    val FORALL_hashmap_hash_map_t : thm
-    val datatype_hashmap_hash_map_t : thm
-    val datatype_hashmap_list_t : thm
-    val hashmap_hash_map_t_11 : thm
-    val hashmap_hash_map_t_Axiom : thm
-    val hashmap_hash_map_t_accessors : thm
-    val hashmap_hash_map_t_accfupds : thm
-    val hashmap_hash_map_t_case_cong : thm
-    val hashmap_hash_map_t_case_eq : thm
-    val hashmap_hash_map_t_component_equality : thm
-    val hashmap_hash_map_t_fn_updates : thm
-    val hashmap_hash_map_t_fupdcanon : thm
-    val hashmap_hash_map_t_fupdcanon_comp : thm
-    val hashmap_hash_map_t_fupdfupds : thm
-    val hashmap_hash_map_t_fupdfupds_comp : thm
-    val hashmap_hash_map_t_induction : thm
-    val hashmap_hash_map_t_literal_11 : thm
-    val hashmap_hash_map_t_literal_nchotomy : thm
-    val hashmap_hash_map_t_nchotomy : thm
-    val hashmap_hash_map_t_updates_eq_literal : thm
-    val hashmap_list_t_11 : thm
-    val hashmap_list_t_Axiom : thm
-    val hashmap_list_t_case_cong : thm
-    val hashmap_list_t_case_eq : thm
-    val hashmap_list_t_distinct : thm
-    val hashmap_list_t_induction : thm
-    val hashmap_list_t_nchotomy : thm
-  
-  val hashmapMain_Types_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [divDef] Parent theory of "hashmapMain_Types"
-   
-   [hashmap_hash_map_t_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('hashmap_hash_map_t').
-                   (∀a0'.
-                      (∃a0 a1 a2 a3.
-                         a0' =
-                         (λa0 a1 a2 a3.
-                              ind_type$CONSTR 0 (a0,a1,a2,a3)
-                                (λn. ind_type$BOTTOM)) a0 a1 a2 a3) ⇒
-                      $var$('hashmap_hash_map_t') a0') ⇒
-                   $var$('hashmap_hash_map_t') a0') rep
-   
-   [hashmap_hash_map_t_case_def]  Definition
-      
-      ⊢ ∀a0 a1 a2 a3 f.
-          hashmap_hash_map_t_CASE (hashmap_hash_map_t a0 a1 a2 a3) f =
-          f a0 a1 a2 a3
-   
-   [hashmap_hash_map_t_hashmap_hash_map_max_load]  Definition
-      
-      ⊢ ∀u p u0 v.
-          (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0
-   
-   [hashmap_hash_map_t_hashmap_hash_map_max_load_factor]  Definition
-      
-      ⊢ ∀u p u0 v.
-          (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor =
-          p
-   
-   [hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hashmap_hash_map_t u p u0 v with
-          hashmap_hash_map_max_load_factor updated_by f =
-          hashmap_hash_map_t u (f p) u0 v
-   
-   [hashmap_hash_map_t_hashmap_hash_map_max_load_fupd]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hashmap_hash_map_t u p u0 v with
-          hashmap_hash_map_max_load updated_by f =
-          hashmap_hash_map_t u p (f u0) v
-   
-   [hashmap_hash_map_t_hashmap_hash_map_num_entries]  Definition
-      
-      ⊢ ∀u p u0 v.
-          (hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u
-   
-   [hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hashmap_hash_map_t u p u0 v with
-          hashmap_hash_map_num_entries updated_by f =
-          hashmap_hash_map_t (f u) p u0 v
-   
-   [hashmap_hash_map_t_hashmap_hash_map_slots]  Definition
-      
-      ⊢ ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v
-   
-   [hashmap_hash_map_t_hashmap_hash_map_slots_fupd]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hashmap_hash_map_t u p u0 v with
-          hashmap_hash_map_slots updated_by f =
-          hashmap_hash_map_t u p u0 (f v)
-   
-   [hashmap_hash_map_t_size_def]  Definition
-      
-      ⊢ ∀f a0 a1 a2 a3.
-          hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
-          1 + pair_size (λv. 0) (λv. 0) a1
-   
-   [hashmap_list_t_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('hashmap_list_t').
-                   (∀a0'.
-                      (∃a0 a1 a2.
-                         a0' =
-                         (λa0 a1 a2.
-                              ind_type$CONSTR 0 (a0,a1)
-                                (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
-                           a0 a1 a2 ∧ $var$('hashmap_list_t') a2) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) (ARB,ARB)
-                        (λn. ind_type$BOTTOM) ⇒
-                      $var$('hashmap_list_t') a0') ⇒
-                   $var$('hashmap_list_t') a0') rep
-   
-   [hashmap_list_t_case_def]  Definition
-      
-      ⊢ (∀a0 a1 a2 f v.
-           hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
-        ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
-   
-   [hashmap_list_t_size_def]  Definition
-      
-      ⊢ (∀f a0 a1 a2.
-           hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
-           1 + (f a1 + hashmap_list_t_size f a2)) ∧
-        ∀f. hashmap_list_t_size f HashmapListNil = 0
-   
-   [EXISTS_hashmap_hash_map_t]  Theorem
-      
-      ⊢ ∀P. (∃h. P h) ⇔
-            ∃u0 p u v.
-              P
-                <|hashmap_hash_map_num_entries := u0;
-                  hashmap_hash_map_max_load_factor := p;
-                  hashmap_hash_map_max_load := u;
-                  hashmap_hash_map_slots := v|>
-   
-   [FORALL_hashmap_hash_map_t]  Theorem
-      
-      ⊢ ∀P. (∀h. P h) ⇔
-            ∀u0 p u v.
-              P
-                <|hashmap_hash_map_num_entries := u0;
-                  hashmap_hash_map_max_load_factor := p;
-                  hashmap_hash_map_max_load := u;
-                  hashmap_hash_map_slots := v|>
-   
-   [datatype_hashmap_hash_map_t]  Theorem
-      
-      ⊢ DATATYPE
-          (record hashmap_hash_map_t hashmap_hash_map_num_entries
-             hashmap_hash_map_max_load_factor hashmap_hash_map_max_load
-             hashmap_hash_map_slots)
-   
-   [datatype_hashmap_list_t]  Theorem
-      
-      ⊢ DATATYPE (hashmap_list_t HashmapListCons HashmapListNil)
-   
-   [hashmap_hash_map_t_11]  Theorem
-      
-      ⊢ ∀a0 a1 a2 a3 a0' a1' a2' a3'.
-          hashmap_hash_map_t a0 a1 a2 a3 =
-          hashmap_hash_map_t a0' a1' a2' a3' ⇔
-          a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3'
-   
-   [hashmap_hash_map_t_Axiom]  Theorem
-      
-      ⊢ ∀f. ∃fn. ∀a0 a1 a2 a3.
-          fn (hashmap_hash_map_t a0 a1 a2 a3) = f a0 a1 a2 a3
-   
-   [hashmap_hash_map_t_accessors]  Theorem
-      
-      ⊢ (∀u p u0 v.
-           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u) ∧
-        (∀u p u0 v.
-           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor =
-           p) ∧
-        (∀u p u0 v.
-           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0) ∧
-        ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v
-   
-   [hashmap_hash_map_t_accfupds]  Theorem
-      
-      ⊢ (∀h f.
-           (h with hashmap_hash_map_max_load_factor updated_by f).
-           hashmap_hash_map_num_entries =
-           h.hashmap_hash_map_num_entries) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load updated_by f).
-           hashmap_hash_map_num_entries =
-           h.hashmap_hash_map_num_entries) ∧
-        (∀h f.
-           (h with hashmap_hash_map_slots updated_by f).
-           hashmap_hash_map_num_entries =
-           h.hashmap_hash_map_num_entries) ∧
-        (∀h f.
-           (h with hashmap_hash_map_num_entries updated_by f).
-           hashmap_hash_map_max_load_factor =
-           h.hashmap_hash_map_max_load_factor) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load updated_by f).
-           hashmap_hash_map_max_load_factor =
-           h.hashmap_hash_map_max_load_factor) ∧
-        (∀h f.
-           (h with hashmap_hash_map_slots updated_by f).
-           hashmap_hash_map_max_load_factor =
-           h.hashmap_hash_map_max_load_factor) ∧
-        (∀h f.
-           (h with hashmap_hash_map_num_entries updated_by f).
-           hashmap_hash_map_max_load =
-           h.hashmap_hash_map_max_load) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load_factor updated_by f).
-           hashmap_hash_map_max_load =
-           h.hashmap_hash_map_max_load) ∧
-        (∀h f.
-           (h with hashmap_hash_map_slots updated_by f).
-           hashmap_hash_map_max_load =
-           h.hashmap_hash_map_max_load) ∧
-        (∀h f.
-           (h with hashmap_hash_map_num_entries updated_by f).
-           hashmap_hash_map_slots =
-           h.hashmap_hash_map_slots) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load_factor updated_by f).
-           hashmap_hash_map_slots =
-           h.hashmap_hash_map_slots) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load updated_by f).
-           hashmap_hash_map_slots =
-           h.hashmap_hash_map_slots) ∧
-        (∀h f.
-           (h with hashmap_hash_map_num_entries updated_by f).
-           hashmap_hash_map_num_entries =
-           f h.hashmap_hash_map_num_entries) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load_factor updated_by f).
-           hashmap_hash_map_max_load_factor =
-           f h.hashmap_hash_map_max_load_factor) ∧
-        (∀h f.
-           (h with hashmap_hash_map_max_load updated_by f).
-           hashmap_hash_map_max_load =
-           f h.hashmap_hash_map_max_load) ∧
-        ∀h f.
-          (h with hashmap_hash_map_slots updated_by f).
-          hashmap_hash_map_slots =
-          f h.hashmap_hash_map_slots
-   
-   [hashmap_hash_map_t_case_cong]  Theorem
-      
-      ⊢ ∀M M' f.
-          M = M' ∧
-          (∀a0 a1 a2 a3.
-             M' = hashmap_hash_map_t a0 a1 a2 a3 ⇒
-             f a0 a1 a2 a3 = f' a0 a1 a2 a3) ⇒
-          hashmap_hash_map_t_CASE M f = hashmap_hash_map_t_CASE M' f'
-   
-   [hashmap_hash_map_t_case_eq]  Theorem
-      
-      ⊢ hashmap_hash_map_t_CASE x f = v ⇔
-        ∃u p u0 v'. x = hashmap_hash_map_t u p u0 v' ∧ f u p u0 v' = v
-   
-   [hashmap_hash_map_t_component_equality]  Theorem
-      
-      ⊢ ∀h1 h2.
-          h1 = h2 ⇔
-          h1.hashmap_hash_map_num_entries = h2.hashmap_hash_map_num_entries ∧
-          h1.hashmap_hash_map_max_load_factor =
-          h2.hashmap_hash_map_max_load_factor ∧
-          h1.hashmap_hash_map_max_load = h2.hashmap_hash_map_max_load ∧
-          h1.hashmap_hash_map_slots = h2.hashmap_hash_map_slots
-   
-   [hashmap_hash_map_t_fn_updates]  Theorem
-      
-      ⊢ (∀f u p u0 v.
-           hashmap_hash_map_t u p u0 v with
-           hashmap_hash_map_num_entries updated_by f =
-           hashmap_hash_map_t (f u) p u0 v) ∧
-        (∀f u p u0 v.
-           hashmap_hash_map_t u p u0 v with
-           hashmap_hash_map_max_load_factor updated_by f =
-           hashmap_hash_map_t u (f p) u0 v) ∧
-        (∀f u p u0 v.
-           hashmap_hash_map_t u p u0 v with
-           hashmap_hash_map_max_load updated_by f =
-           hashmap_hash_map_t u p (f u0) v) ∧
-        ∀f u p u0 v.
-          hashmap_hash_map_t u p u0 v with
-          hashmap_hash_map_slots updated_by f =
-          hashmap_hash_map_t u p u0 (f v)
-   
-   [hashmap_hash_map_t_fupdcanon]  Theorem
-      
-      ⊢ (∀h g f.
-           h with
-           <|hashmap_hash_map_max_load_factor updated_by f;
-             hashmap_hash_map_num_entries updated_by g|> =
-           h with
-           <|hashmap_hash_map_num_entries updated_by g;
-             hashmap_hash_map_max_load_factor updated_by f|>) ∧
-        (∀h g f.
-           h with
-           <|hashmap_hash_map_max_load updated_by f;
-             hashmap_hash_map_num_entries updated_by g|> =
-           h with
-           <|hashmap_hash_map_num_entries updated_by g;
-             hashmap_hash_map_max_load updated_by f|>) ∧
-        (∀h g f.
-           h with
-           <|hashmap_hash_map_max_load updated_by f;
-             hashmap_hash_map_max_load_factor updated_by g|> =
-           h with
-           <|hashmap_hash_map_max_load_factor updated_by g;
-             hashmap_hash_map_max_load updated_by f|>) ∧
-        (∀h g f.
-           h with
-           <|hashmap_hash_map_slots updated_by f;
-             hashmap_hash_map_num_entries updated_by g|> =
-           h with
-           <|hashmap_hash_map_num_entries updated_by g;
-             hashmap_hash_map_slots updated_by f|>) ∧
-        (∀h g f.
-           h with
-           <|hashmap_hash_map_slots updated_by f;
-             hashmap_hash_map_max_load_factor updated_by g|> =
-           h with
-           <|hashmap_hash_map_max_load_factor updated_by g;
-             hashmap_hash_map_slots updated_by f|>) ∧
-        ∀h g f.
-          h with
-          <|hashmap_hash_map_slots updated_by f;
-            hashmap_hash_map_max_load updated_by g|> =
-          h with
-          <|hashmap_hash_map_max_load updated_by g;
-            hashmap_hash_map_slots updated_by f|>
-   
-   [hashmap_hash_map_t_fupdcanon_comp]  Theorem
-      
-      ⊢ ((∀g f.
-            hashmap_hash_map_max_load_factor_fupd f ∘
-            hashmap_hash_map_num_entries_fupd g =
-            hashmap_hash_map_num_entries_fupd g ∘
-            hashmap_hash_map_max_load_factor_fupd f) ∧
-         ∀h g f.
-           hashmap_hash_map_max_load_factor_fupd f ∘
-           hashmap_hash_map_num_entries_fupd g ∘ h =
-           hashmap_hash_map_num_entries_fupd g ∘
-           hashmap_hash_map_max_load_factor_fupd f ∘ h) ∧
-        ((∀g f.
-            hashmap_hash_map_max_load_fupd f ∘
-            hashmap_hash_map_num_entries_fupd g =
-            hashmap_hash_map_num_entries_fupd g ∘
-            hashmap_hash_map_max_load_fupd f) ∧
-         ∀h g f.
-           hashmap_hash_map_max_load_fupd f ∘
-           hashmap_hash_map_num_entries_fupd g ∘ h =
-           hashmap_hash_map_num_entries_fupd g ∘
-           hashmap_hash_map_max_load_fupd f ∘ h) ∧
-        ((∀g f.
-            hashmap_hash_map_max_load_fupd f ∘
-            hashmap_hash_map_max_load_factor_fupd g =
-            hashmap_hash_map_max_load_factor_fupd g ∘
-            hashmap_hash_map_max_load_fupd f) ∧
-         ∀h g f.
-           hashmap_hash_map_max_load_fupd f ∘
-           hashmap_hash_map_max_load_factor_fupd g ∘ h =
-           hashmap_hash_map_max_load_factor_fupd g ∘
-           hashmap_hash_map_max_load_fupd f ∘ h) ∧
-        ((∀g f.
-            hashmap_hash_map_slots_fupd f ∘
-            hashmap_hash_map_num_entries_fupd g =
-            hashmap_hash_map_num_entries_fupd g ∘
-            hashmap_hash_map_slots_fupd f) ∧
-         ∀h g f.
-           hashmap_hash_map_slots_fupd f ∘
-           hashmap_hash_map_num_entries_fupd g ∘ h =
-           hashmap_hash_map_num_entries_fupd g ∘
-           hashmap_hash_map_slots_fupd f ∘ h) ∧
-        ((∀g f.
-            hashmap_hash_map_slots_fupd f ∘
-            hashmap_hash_map_max_load_factor_fupd g =
-            hashmap_hash_map_max_load_factor_fupd g ∘
-            hashmap_hash_map_slots_fupd f) ∧
-         ∀h g f.
-           hashmap_hash_map_slots_fupd f ∘
-           hashmap_hash_map_max_load_factor_fupd g ∘ h =
-           hashmap_hash_map_max_load_factor_fupd g ∘
-           hashmap_hash_map_slots_fupd f ∘ h) ∧
-        (∀g f.
-           hashmap_hash_map_slots_fupd f ∘ hashmap_hash_map_max_load_fupd g =
-           hashmap_hash_map_max_load_fupd g ∘ hashmap_hash_map_slots_fupd f) ∧
-        ∀h g f.
-          hashmap_hash_map_slots_fupd f ∘
-          hashmap_hash_map_max_load_fupd g ∘ h =
-          hashmap_hash_map_max_load_fupd g ∘
-          hashmap_hash_map_slots_fupd f ∘ h
-   
-   [hashmap_hash_map_t_fupdfupds]  Theorem
-      
-      ⊢ (∀h g f.
-           h with
-           <|hashmap_hash_map_num_entries updated_by f;
-             hashmap_hash_map_num_entries updated_by g|> =
-           h with hashmap_hash_map_num_entries updated_by f ∘ g) ∧
-        (∀h g f.
-           h with
-           <|hashmap_hash_map_max_load_factor updated_by f;
-             hashmap_hash_map_max_load_factor updated_by g|> =
-           h with hashmap_hash_map_max_load_factor updated_by f ∘ g) ∧
-        (∀h g f.
-           h with
-           <|hashmap_hash_map_max_load updated_by f;
-             hashmap_hash_map_max_load updated_by g|> =
-           h with hashmap_hash_map_max_load updated_by f ∘ g) ∧
-        ∀h g f.
-          h with
-          <|hashmap_hash_map_slots updated_by f;
-            hashmap_hash_map_slots updated_by g|> =
-          h with hashmap_hash_map_slots updated_by f ∘ g
-   
-   [hashmap_hash_map_t_fupdfupds_comp]  Theorem
-      
-      ⊢ ((∀g f.
-            hashmap_hash_map_num_entries_fupd f ∘
-            hashmap_hash_map_num_entries_fupd g =
-            hashmap_hash_map_num_entries_fupd (f ∘ g)) ∧
-         ∀h g f.
-           hashmap_hash_map_num_entries_fupd f ∘
-           hashmap_hash_map_num_entries_fupd g ∘ h =
-           hashmap_hash_map_num_entries_fupd (f ∘ g) ∘ h) ∧
-        ((∀g f.
-            hashmap_hash_map_max_load_factor_fupd f ∘
-            hashmap_hash_map_max_load_factor_fupd g =
-            hashmap_hash_map_max_load_factor_fupd (f ∘ g)) ∧
-         ∀h g f.
-           hashmap_hash_map_max_load_factor_fupd f ∘
-           hashmap_hash_map_max_load_factor_fupd g ∘ h =
-           hashmap_hash_map_max_load_factor_fupd (f ∘ g) ∘ h) ∧
-        ((∀g f.
-            hashmap_hash_map_max_load_fupd f ∘
-            hashmap_hash_map_max_load_fupd g =
-            hashmap_hash_map_max_load_fupd (f ∘ g)) ∧
-         ∀h g f.
-           hashmap_hash_map_max_load_fupd f ∘
-           hashmap_hash_map_max_load_fupd g ∘ h =
-           hashmap_hash_map_max_load_fupd (f ∘ g) ∘ h) ∧
-        (∀g f.
-           hashmap_hash_map_slots_fupd f ∘ hashmap_hash_map_slots_fupd g =
-           hashmap_hash_map_slots_fupd (f ∘ g)) ∧
-        ∀h g f.
-          hashmap_hash_map_slots_fupd f ∘ hashmap_hash_map_slots_fupd g ∘ h =
-          hashmap_hash_map_slots_fupd (f ∘ g) ∘ h
-   
-   [hashmap_hash_map_t_induction]  Theorem
-      
-      ⊢ ∀P. (∀u p u0 v. P (hashmap_hash_map_t u p u0 v)) ⇒ ∀h. P h
-   
-   [hashmap_hash_map_t_literal_11]  Theorem
-      
-      ⊢ ∀u01 p1 u1 v1 u02 p2 u2 v2.
-          <|hashmap_hash_map_num_entries := u01;
-            hashmap_hash_map_max_load_factor := p1;
-            hashmap_hash_map_max_load := u1; hashmap_hash_map_slots := v1|> =
-          <|hashmap_hash_map_num_entries := u02;
-            hashmap_hash_map_max_load_factor := p2;
-            hashmap_hash_map_max_load := u2; hashmap_hash_map_slots := v2|> ⇔
-          u01 = u02 ∧ p1 = p2 ∧ u1 = u2 ∧ v1 = v2
-   
-   [hashmap_hash_map_t_literal_nchotomy]  Theorem
-      
-      ⊢ ∀h. ∃u0 p u v.
-          h =
-          <|hashmap_hash_map_num_entries := u0;
-            hashmap_hash_map_max_load_factor := p;
-            hashmap_hash_map_max_load := u; hashmap_hash_map_slots := v|>
-   
-   [hashmap_hash_map_t_nchotomy]  Theorem
-      
-      ⊢ ∀hh. ∃u p u0 v. hh = hashmap_hash_map_t u p u0 v
-   
-   [hashmap_hash_map_t_updates_eq_literal]  Theorem
-      
-      ⊢ ∀h u0 p u v.
-          h with
-          <|hashmap_hash_map_num_entries := u0;
-            hashmap_hash_map_max_load_factor := p;
-            hashmap_hash_map_max_load := u; hashmap_hash_map_slots := v|> =
-          <|hashmap_hash_map_num_entries := u0;
-            hashmap_hash_map_max_load_factor := p;
-            hashmap_hash_map_max_load := u; hashmap_hash_map_slots := v|>
-   
-   [hashmap_list_t_11]  Theorem
-      
-      ⊢ ∀a0 a1 a2 a0' a1' a2'.
-          HashmapListCons a0 a1 a2 = HashmapListCons a0' a1' a2' ⇔
-          a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
-   
-   [hashmap_list_t_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1. ∃fn.
-          (∀a0 a1 a2. fn (HashmapListCons a0 a1 a2) = f0 a0 a1 a2 (fn a2)) ∧
-          fn HashmapListNil = f1
-   
-   [hashmap_list_t_case_cong]  Theorem
-      
-      ⊢ ∀M M' f v.
-          M = M' ∧
-          (∀a0 a1 a2.
-             M' = HashmapListCons a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ∧
-          (M' = HashmapListNil ⇒ v = v') ⇒
-          hashmap_list_t_CASE M f v = hashmap_list_t_CASE M' f' v'
-   
-   [hashmap_list_t_case_eq]  Theorem
-      
-      ⊢ hashmap_list_t_CASE x f v = v' ⇔
-        (∃u t h. x = HashmapListCons u t h ∧ f u t h = v') ∨
-        x = HashmapListNil ∧ v = v'
-   
-   [hashmap_list_t_distinct]  Theorem
-      
-      ⊢ ∀a2 a1 a0. HashmapListCons a0 a1 a2 ≠ HashmapListNil
-   
-   [hashmap_list_t_induction]  Theorem
-      
-      ⊢ ∀P. (∀h. P h ⇒ ∀t u. P (HashmapListCons u t h)) ∧ P HashmapListNil ⇒
-            ∀h. P h
-   
-   [hashmap_list_t_nchotomy]  Theorem
-      
-      ⊢ ∀hh. (∃u t h. hh = HashmapListCons u t h) ∨ hh = HashmapListNil
-   
-   
-*)
-end