Merge branch 'main' into son/loops2

5 files changed, 1598 insertions, 0 deletions

diff --git a/tests/hol4/loops/Holmakefile b/tests/hol4/loops/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/loops/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES =  ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/loops/loops_FunsScript.sml b/tests/hol4/loops/loops_FunsScript.sml
new file mode 100644
index 00000000..65cf77d4
--- /dev/null
+++ b/tests/hol4/loops/loops_FunsScript.sml
@@ -0,0 +1,755 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: function definitions *)
+open primitivesLib divDefLib
+open loops_TypesTheory
+
+val _ = new_theory "loops_Funs"
+
+
+val [sum_loop_fwd_def] = DefineDiv ‘
+  (** [loops::sum]: loop 0: forward function *)
+  sum_loop_fwd (max : u32) (i : u32) (s : u32) : u32 result =
+    if u32_lt i max
+    then (
+      do
+      s0 <- u32_add s i;
+      i0 <- u32_add i (int_to_u32 1);
+      sum_loop_fwd max i0 s0
+      od)
+    else u32_mul s (int_to_u32 2)
+’
+
+val sum_fwd_def = Define ‘
+  (** [loops::sum]: forward function *)
+  sum_fwd (max : u32) : u32 result =
+    sum_loop_fwd max (int_to_u32 0) (int_to_u32 0)
+’
+
+val [sum_with_mut_borrows_loop_fwd_def] = DefineDiv ‘
+  (** [loops::sum_with_mut_borrows]: loop 0: forward function *)
+  sum_with_mut_borrows_loop_fwd
+    (max : u32) (mi : u32) (ms : u32) : u32 result =
+    if u32_lt mi max
+    then (
+      do
+      ms0 <- u32_add ms mi;
+      mi0 <- u32_add mi (int_to_u32 1);
+      sum_with_mut_borrows_loop_fwd max mi0 ms0
+      od)
+    else u32_mul ms (int_to_u32 2)
+’
+
+val sum_with_mut_borrows_fwd_def = Define ‘
+  (** [loops::sum_with_mut_borrows]: forward function *)
+  sum_with_mut_borrows_fwd (max : u32) : u32 result =
+    sum_with_mut_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
+’
+
+val [sum_with_shared_borrows_loop_fwd_def] = DefineDiv ‘
+  (** [loops::sum_with_shared_borrows]: loop 0: forward function *)
+  sum_with_shared_borrows_loop_fwd
+    (max : u32) (i : u32) (s : u32) : u32 result =
+    if u32_lt i max
+    then (
+      do
+      i0 <- u32_add i (int_to_u32 1);
+      s0 <- u32_add s i0;
+      sum_with_shared_borrows_loop_fwd max i0 s0
+      od)
+    else u32_mul s (int_to_u32 2)
+’
+
+val sum_with_shared_borrows_fwd_def = Define ‘
+  (** [loops::sum_with_shared_borrows]: forward function *)
+  sum_with_shared_borrows_fwd (max : u32) : u32 result =
+    sum_with_shared_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
+’
+
+val [clear_loop_fwd_back_def] = DefineDiv ‘
+  (** [loops::clear]: loop 0: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
+  clear_loop_fwd_back (v : u32 vec) (i : usize) : u32 vec result =
+    let i0 = vec_len v in
+    if usize_lt i i0
+    then (
+      do
+      i1 <- usize_add i (int_to_usize 1);
+      v0 <- vec_index_mut_back v i (int_to_u32 0);
+      clear_loop_fwd_back v0 i1
+      od)
+    else Return v
+’
+
+val clear_fwd_back_def = Define ‘
+  (** [loops::clear]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
+  clear_fwd_back (v : u32 vec) : u32 vec result =
+    clear_loop_fwd_back v (int_to_usize 0)
+’
+
+val [list_mem_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_mem]: loop 0: forward function *)
+  list_mem_loop_fwd (x : u32) (ls : u32 list_t) : bool result =
+    (case ls of
+    | ListCons y tl => if y = x then Return T else list_mem_loop_fwd x tl
+    | ListNil => Return F)
+’
+
+val list_mem_fwd_def = Define ‘
+  (** [loops::list_mem]: forward function *)
+  list_mem_fwd (x : u32) (ls : u32 list_t) : bool result =
+    list_mem_loop_fwd x ls
+’
+
+val [list_nth_mut_loop_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop]: loop 0: forward function *)
+  list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
+    (case ls of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return x
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        list_nth_mut_loop_loop_fwd tl i0
+        od)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_fwd_def = Define ‘
+  (** [loops::list_nth_mut_loop]: forward function *)
+  list_nth_mut_loop_fwd (ls : 't list_t) (i : u32) : 't result =
+    list_nth_mut_loop_loop_fwd ls i
+’
+
+val [list_nth_mut_loop_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
+  list_nth_mut_loop_loop_back
+    (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
+    (case ls of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return (ListCons ret tl)
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        tl0 <- list_nth_mut_loop_loop_back tl i0 ret;
+        Return (ListCons x tl0)
+        od)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_back_def = Define ‘
+  (** [loops::list_nth_mut_loop]: backward function 0 *)
+  list_nth_mut_loop_back
+    (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
+    list_nth_mut_loop_loop_back ls i ret
+’
+
+val [list_nth_shared_loop_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_loop]: loop 0: forward function *)
+  list_nth_shared_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
+    (case ls of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return x
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        list_nth_shared_loop_loop_fwd tl i0
+        od)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_loop_fwd_def = Define ‘
+  (** [loops::list_nth_shared_loop]: forward function *)
+  list_nth_shared_loop_fwd (ls : 't list_t) (i : u32) : 't result =
+    list_nth_shared_loop_loop_fwd ls i
+’
+
+val [get_elem_mut_loop_fwd_def] = DefineDiv ‘
+  (** [loops::get_elem_mut]: loop 0: forward function *)
+  get_elem_mut_loop_fwd (x : usize) (ls : usize list_t) : usize result =
+    (case ls of
+    | ListCons y tl => if y = x then Return y else get_elem_mut_loop_fwd x tl
+    | ListNil => Fail Failure)
+’
+
+val get_elem_mut_fwd_def = Define ‘
+  (** [loops::get_elem_mut]: forward function *)
+  get_elem_mut_fwd (slots : usize list_t vec) (x : usize) : usize result =
+    do
+    l <- vec_index_mut_fwd slots (int_to_usize 0);
+    get_elem_mut_loop_fwd x l
+    od
+’
+
+val [get_elem_mut_loop_back_def] = DefineDiv ‘
+  (** [loops::get_elem_mut]: loop 0: backward function 0 *)
+  get_elem_mut_loop_back
+    (x : usize) (ls : usize list_t) (ret : usize) : usize list_t result =
+    (case ls of
+    | ListCons y tl =>
+      if y = x
+      then Return (ListCons ret tl)
+      else (
+        do
+        tl0 <- get_elem_mut_loop_back x tl ret;
+        Return (ListCons y tl0)
+        od)
+    | ListNil => Fail Failure)
+’
+
+val get_elem_mut_back_def = Define ‘
+  (** [loops::get_elem_mut]: backward function 0 *)
+  get_elem_mut_back
+    (slots : usize list_t vec) (x : usize) (ret : usize) :
+    usize list_t vec result
+    =
+    do
+    l <- vec_index_mut_fwd slots (int_to_usize 0);
+    l0 <- get_elem_mut_loop_back x l ret;
+    vec_index_mut_back slots (int_to_usize 0) l0
+    od
+’
+
+val [get_elem_shared_loop_fwd_def] = DefineDiv ‘
+  (** [loops::get_elem_shared]: loop 0: forward function *)
+  get_elem_shared_loop_fwd (x : usize) (ls : usize list_t) : usize result =
+    (case ls of
+    | ListCons y tl =>
+      if y = x then Return y else get_elem_shared_loop_fwd x tl
+    | ListNil => Fail Failure)
+’
+
+val get_elem_shared_fwd_def = Define ‘
+  (** [loops::get_elem_shared]: forward function *)
+  get_elem_shared_fwd (slots : usize list_t vec) (x : usize) : usize result =
+    do
+    l <- vec_index_fwd slots (int_to_usize 0);
+    get_elem_shared_loop_fwd x l
+    od
+’
+
+val id_mut_fwd_def = Define ‘
+  (** [loops::id_mut]: forward function *)
+  id_mut_fwd (ls : 't list_t) : 't list_t result =
+    Return ls
+’
+
+val id_mut_back_def = Define ‘
+  (** [loops::id_mut]: backward function 0 *)
+  id_mut_back (ls : 't list_t) (ret : 't list_t) : 't list_t result =
+    Return ret
+’
+
+val id_shared_fwd_def = Define ‘
+  (** [loops::id_shared]: forward function *)
+  id_shared_fwd (ls : 't list_t) : 't list_t result =
+    Return ls
+’
+
+val [list_nth_mut_loop_with_id_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
+  list_nth_mut_loop_with_id_loop_fwd (i : u32) (ls : 't list_t) : 't result =
+    (case ls of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return x
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        list_nth_mut_loop_with_id_loop_fwd i0 tl
+        od)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_with_id_fwd_def = Define ‘
+  (** [loops::list_nth_mut_loop_with_id]: forward function *)
+  list_nth_mut_loop_with_id_fwd (ls : 't list_t) (i : u32) : 't result =
+    do
+    ls0 <- id_mut_fwd ls;
+    list_nth_mut_loop_with_id_loop_fwd i ls0
+    od
+’
+
+val [list_nth_mut_loop_with_id_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
+  list_nth_mut_loop_with_id_loop_back
+    (i : u32) (ls : 't list_t) (ret : 't) : 't list_t result =
+    (case ls of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return (ListCons ret tl)
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        tl0 <- list_nth_mut_loop_with_id_loop_back i0 tl ret;
+        Return (ListCons x tl0)
+        od)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_with_id_back_def = Define ‘
+  (** [loops::list_nth_mut_loop_with_id]: backward function 0 *)
+  list_nth_mut_loop_with_id_back
+    (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
+    do
+    ls0 <- id_mut_fwd ls;
+    l <- list_nth_mut_loop_with_id_loop_back i ls0 ret;
+    id_mut_back ls l
+    od
+’
+
+val [list_nth_shared_loop_with_id_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
+  list_nth_shared_loop_with_id_loop_fwd
+    (i : u32) (ls : 't list_t) : 't result =
+    (case ls of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return x
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        list_nth_shared_loop_with_id_loop_fwd i0 tl
+        od)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_loop_with_id_fwd_def = Define ‘
+  (** [loops::list_nth_shared_loop_with_id]: forward function *)
+  list_nth_shared_loop_with_id_fwd (ls : 't list_t) (i : u32) : 't result =
+    do
+    ls0 <- id_shared_fwd ls;
+    list_nth_shared_loop_with_id_loop_fwd i ls0
+    od
+’
+
+val [list_nth_mut_loop_pair_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
+  list_nth_mut_loop_pair_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_mut_loop_pair_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_pair_fwd_def = Define ‘
+  (** [loops::list_nth_mut_loop_pair]: forward function *)
+  list_nth_mut_loop_pair_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_mut_loop_pair_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_mut_loop_pair_loop_back'a_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
+  list_nth_mut_loop_pair_loop_back'a
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (ListCons ret tl0)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          tl00 <- list_nth_mut_loop_pair_loop_back'a tl0 tl1 i0 ret;
+          Return (ListCons x0 tl00)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_pair_back'a_def = Define ‘
+  (** [loops::list_nth_mut_loop_pair]: backward function 0 *)
+  list_nth_mut_loop_pair_back'a
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret
+’
+
+val [list_nth_mut_loop_pair_loop_back'b_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *)
+  list_nth_mut_loop_pair_loop_back'b
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (ListCons ret tl1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          tl10 <- list_nth_mut_loop_pair_loop_back'b tl0 tl1 i0 ret;
+          Return (ListCons x1 tl10)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_pair_back'b_def = Define ‘
+  (** [loops::list_nth_mut_loop_pair]: backward function 1 *)
+  list_nth_mut_loop_pair_back'b
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret
+’
+
+val [list_nth_shared_loop_pair_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
+  list_nth_shared_loop_pair_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_shared_loop_pair_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_loop_pair_fwd_def = Define ‘
+  (** [loops::list_nth_shared_loop_pair]: forward function *)
+  list_nth_shared_loop_pair_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_shared_loop_pair_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_mut_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
+  list_nth_mut_loop_pair_merge_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_pair_merge_fwd_def = Define ‘
+  (** [loops::list_nth_mut_loop_pair_merge]: forward function *)
+  list_nth_mut_loop_pair_merge_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_mut_loop_pair_merge_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
+  list_nth_mut_loop_pair_merge_loop_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : ('t # 't)) :
+    ('t list_t # 't list_t) result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then let (t, t0) = ret in Return (ListCons t tl0, ListCons t0 tl1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          (tl00, tl10) <-
+            list_nth_mut_loop_pair_merge_loop_back tl0 tl1 i0 ret;
+          Return (ListCons x0 tl00, ListCons x1 tl10)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_loop_pair_merge_back_def = Define ‘
+  (** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *)
+  list_nth_mut_loop_pair_merge_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : ('t # 't)) :
+    ('t list_t # 't list_t) result
+    =
+    list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret
+’
+
+val [list_nth_shared_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
+  list_nth_shared_loop_pair_merge_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_loop_pair_merge_fwd_def = Define ‘
+  (** [loops::list_nth_shared_loop_pair_merge]: forward function *)
+  list_nth_shared_loop_pair_merge_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_mut_shared_loop_pair_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
+  list_nth_mut_shared_loop_pair_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_mut_shared_loop_pair_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_shared_loop_pair_fwd_def = Define ‘
+  (** [loops::list_nth_mut_shared_loop_pair]: forward function *)
+  list_nth_mut_shared_loop_pair_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_mut_shared_loop_pair_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
+  list_nth_mut_shared_loop_pair_loop_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (ListCons ret tl0)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          tl00 <- list_nth_mut_shared_loop_pair_loop_back tl0 tl1 i0 ret;
+          Return (ListCons x0 tl00)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_shared_loop_pair_back_def = Define ‘
+  (** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *)
+  list_nth_mut_shared_loop_pair_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret
+’
+
+val [list_nth_mut_shared_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
+  list_nth_mut_shared_loop_pair_merge_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_mut_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_shared_loop_pair_merge_fwd_def = Define ‘
+  (** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
+  list_nth_mut_shared_loop_pair_merge_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_mut_shared_loop_pair_merge_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
+  list_nth_mut_shared_loop_pair_merge_loop_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (ListCons ret tl0)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          tl00 <- list_nth_mut_shared_loop_pair_merge_loop_back tl0 tl1 i0 ret;
+          Return (ListCons x0 tl00)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_mut_shared_loop_pair_merge_back_def = Define ‘
+  (** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *)
+  list_nth_mut_shared_loop_pair_merge_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret
+’
+
+val [list_nth_shared_mut_loop_pair_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
+  list_nth_shared_mut_loop_pair_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_shared_mut_loop_pair_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_mut_loop_pair_fwd_def = Define ‘
+  (** [loops::list_nth_shared_mut_loop_pair]: forward function *)
+  list_nth_shared_mut_loop_pair_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_shared_mut_loop_pair_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *)
+  list_nth_shared_mut_loop_pair_loop_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (ListCons ret tl1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          tl10 <- list_nth_shared_mut_loop_pair_loop_back tl0 tl1 i0 ret;
+          Return (ListCons x1 tl10)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_mut_loop_pair_back_def = Define ‘
+  (** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *)
+  list_nth_shared_mut_loop_pair_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret
+’
+
+val [list_nth_shared_mut_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
+  list_nth_shared_mut_loop_pair_merge_loop_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (x0, x1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          list_nth_shared_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_mut_loop_pair_merge_fwd_def = Define ‘
+  (** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
+  list_nth_shared_mut_loop_pair_merge_fwd
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
+    list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i
+’
+
+val [list_nth_shared_mut_loop_pair_merge_loop_back_def] = DefineDiv ‘
+  (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
+  list_nth_shared_mut_loop_pair_merge_loop_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    (case ls0 of
+    | ListCons x0 tl0 =>
+      (case ls1 of
+      | ListCons x1 tl1 =>
+        if i = int_to_u32 0
+        then Return (ListCons ret tl1)
+        else (
+          do
+          i0 <- u32_sub i (int_to_u32 1);
+          tl10 <- list_nth_shared_mut_loop_pair_merge_loop_back tl0 tl1 i0 ret;
+          Return (ListCons x1 tl10)
+          od)
+      | ListNil => Fail Failure)
+    | ListNil => Fail Failure)
+’
+
+val list_nth_shared_mut_loop_pair_merge_back_def = Define ‘
+  (** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *)
+  list_nth_shared_mut_loop_pair_merge_back
+    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
+    't list_t result
+    =
+    list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret
+’
+
+val _ = export_theory ()
diff --git a/tests/hol4/loops/loops_FunsTheory.sig b/tests/hol4/loops/loops_FunsTheory.sig
new file mode 100644
index 00000000..63fe56c9
--- /dev/null
+++ b/tests/hol4/loops/loops_FunsTheory.sig
@@ -0,0 +1,731 @@
+signature loops_FunsTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val clear_fwd_back_def : thm
+    val clear_loop_fwd_back_def : thm
+    val get_elem_mut_back_def : thm
+    val get_elem_mut_fwd_def : thm
+    val get_elem_mut_loop_back_def : thm
+    val get_elem_mut_loop_fwd_def : thm
+    val get_elem_shared_fwd_def : thm
+    val get_elem_shared_loop_fwd_def : thm
+    val id_mut_back_def : thm
+    val id_mut_fwd_def : thm
+    val id_shared_fwd_def : thm
+    val list_mem_fwd_def : thm
+    val list_mem_loop_fwd_def : thm
+    val list_nth_mut_loop_back_def : thm
+    val list_nth_mut_loop_fwd_def : thm
+    val list_nth_mut_loop_loop_back_def : thm
+    val list_nth_mut_loop_loop_fwd_def : thm
+    val list_nth_mut_loop_pair_back'a_def : thm
+    val list_nth_mut_loop_pair_back'b_def : thm
+    val list_nth_mut_loop_pair_fwd_def : thm
+    val list_nth_mut_loop_pair_loop_back'a_def : thm
+    val list_nth_mut_loop_pair_loop_back'b_def : thm
+    val list_nth_mut_loop_pair_loop_fwd_def : thm
+    val list_nth_mut_loop_pair_merge_back_def : thm
+    val list_nth_mut_loop_pair_merge_fwd_def : thm
+    val list_nth_mut_loop_pair_merge_loop_back_def : thm
+    val list_nth_mut_loop_pair_merge_loop_fwd_def : thm
+    val list_nth_mut_loop_with_id_back_def : thm
+    val list_nth_mut_loop_with_id_fwd_def : thm
+    val list_nth_mut_loop_with_id_loop_back_def : thm
+    val list_nth_mut_loop_with_id_loop_fwd_def : thm
+    val list_nth_mut_shared_loop_pair_back_def : thm
+    val list_nth_mut_shared_loop_pair_fwd_def : thm
+    val list_nth_mut_shared_loop_pair_loop_back_def : thm
+    val list_nth_mut_shared_loop_pair_loop_fwd_def : thm
+    val list_nth_mut_shared_loop_pair_merge_back_def : thm
+    val list_nth_mut_shared_loop_pair_merge_fwd_def : thm
+    val list_nth_mut_shared_loop_pair_merge_loop_back_def : thm
+    val list_nth_mut_shared_loop_pair_merge_loop_fwd_def : thm
+    val list_nth_shared_loop_fwd_def : thm
+    val list_nth_shared_loop_loop_fwd_def : thm
+    val list_nth_shared_loop_pair_fwd_def : thm
+    val list_nth_shared_loop_pair_loop_fwd_def : thm
+    val list_nth_shared_loop_pair_merge_fwd_def : thm
+    val list_nth_shared_loop_pair_merge_loop_fwd_def : thm
+    val list_nth_shared_loop_with_id_fwd_def : thm
+    val list_nth_shared_loop_with_id_loop_fwd_def : thm
+    val list_nth_shared_mut_loop_pair_back_def : thm
+    val list_nth_shared_mut_loop_pair_fwd_def : thm
+    val list_nth_shared_mut_loop_pair_loop_back_def : thm
+    val list_nth_shared_mut_loop_pair_loop_fwd_def : thm
+    val list_nth_shared_mut_loop_pair_merge_back_def : thm
+    val list_nth_shared_mut_loop_pair_merge_fwd_def : thm
+    val list_nth_shared_mut_loop_pair_merge_loop_back_def : thm
+    val list_nth_shared_mut_loop_pair_merge_loop_fwd_def : thm
+    val sum_fwd_def : thm
+    val sum_loop_fwd_def : thm
+    val sum_with_mut_borrows_fwd_def : thm
+    val sum_with_mut_borrows_loop_fwd_def : thm
+    val sum_with_shared_borrows_fwd_def : thm
+    val sum_with_shared_borrows_loop_fwd_def : thm
+  
+  val loops_Funs_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [loops_Types] Parent theory of "loops_Funs"
+   
+   [clear_fwd_back_def]  Definition
+      
+      ⊢ ∀v. clear_fwd_back v = clear_loop_fwd_back v (int_to_usize 0)
+   
+   [clear_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀v i.
+          clear_loop_fwd_back v i =
+          (let
+             i0 = vec_len v
+           in
+             if usize_lt i i0 then
+               do
+                 i1 <- usize_add i (int_to_usize 1);
+                 v0 <- vec_index_mut_back v i (int_to_u32 0);
+                 clear_loop_fwd_back v0 i1
+               od
+             else Return v)
+   
+   [get_elem_mut_back_def]  Definition
+      
+      ⊢ ∀slots x ret.
+          get_elem_mut_back slots x ret =
+          do
+            l <- vec_index_mut_fwd slots (int_to_usize 0);
+            l0 <- get_elem_mut_loop_back x l ret;
+            vec_index_mut_back slots (int_to_usize 0) l0
+          od
+   
+   [get_elem_mut_fwd_def]  Definition
+      
+      ⊢ ∀slots x.
+          get_elem_mut_fwd slots x =
+          do
+            l <- vec_index_mut_fwd slots (int_to_usize 0);
+            get_elem_mut_loop_fwd x l
+          od
+   
+   [get_elem_mut_loop_back_def]  Definition
+      
+      ⊢ ∀x ls ret.
+          get_elem_mut_loop_back x ls ret =
+          case ls of
+            ListCons y tl =>
+              if y = x then Return (ListCons ret tl)
+              else
+                do
+                  tl0 <- get_elem_mut_loop_back x tl ret;
+                  Return (ListCons y tl0)
+                od
+          | ListNil => Fail Failure
+   
+   [get_elem_mut_loop_fwd_def]  Definition
+      
+      ⊢ ∀x ls.
+          get_elem_mut_loop_fwd x ls =
+          case ls of
+            ListCons y tl =>
+              if y = x then Return y else get_elem_mut_loop_fwd x tl
+          | ListNil => Fail Failure
+   
+   [get_elem_shared_fwd_def]  Definition
+      
+      ⊢ ∀slots x.
+          get_elem_shared_fwd slots x =
+          do
+            l <- vec_index_fwd slots (int_to_usize 0);
+            get_elem_shared_loop_fwd x l
+          od
+   
+   [get_elem_shared_loop_fwd_def]  Definition
+      
+      ⊢ ∀x ls.
+          get_elem_shared_loop_fwd x ls =
+          case ls of
+            ListCons y tl =>
+              if y = x then Return y else get_elem_shared_loop_fwd x tl
+          | ListNil => Fail Failure
+   
+   [id_mut_back_def]  Definition
+      
+      ⊢ ∀ls ret. id_mut_back ls ret = Return ret
+   
+   [id_mut_fwd_def]  Definition
+      
+      ⊢ ∀ls. id_mut_fwd ls = Return ls
+   
+   [id_shared_fwd_def]  Definition
+      
+      ⊢ ∀ls. id_shared_fwd ls = Return ls
+   
+   [list_mem_fwd_def]  Definition
+      
+      ⊢ ∀x ls. list_mem_fwd x ls = list_mem_loop_fwd x ls
+   
+   [list_mem_loop_fwd_def]  Definition
+      
+      ⊢ ∀x ls.
+          list_mem_loop_fwd x ls =
+          case ls of
+            ListCons y tl =>
+              if y = x then Return T else list_mem_loop_fwd x tl
+          | ListNil => Return F
+   
+   [list_nth_mut_loop_back_def]  Definition
+      
+      ⊢ ∀ls i ret.
+          list_nth_mut_loop_back ls i ret =
+          list_nth_mut_loop_loop_back ls i ret
+   
+   [list_nth_mut_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls i. list_nth_mut_loop_fwd ls i = list_nth_mut_loop_loop_fwd ls i
+   
+   [list_nth_mut_loop_loop_back_def]  Definition
+      
+      ⊢ ∀ls i ret.
+          list_nth_mut_loop_loop_back ls i ret =
+          case ls of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return (ListCons ret tl)
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  tl0 <- list_nth_mut_loop_loop_back tl i0 ret;
+                  Return (ListCons x tl0)
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls i.
+          list_nth_mut_loop_loop_fwd ls i =
+          case ls of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_mut_loop_loop_fwd tl i0
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_pair_back'a_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_loop_pair_back'a ls0 ls1 i ret =
+          list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret
+   
+   [list_nth_mut_loop_pair_back'b_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_loop_pair_back'b ls0 ls1 i ret =
+          list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret
+   
+   [list_nth_mut_loop_pair_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_loop_pair_fwd ls0 ls1 i =
+          list_nth_mut_loop_pair_loop_fwd ls0 ls1 i
+   
+   [list_nth_mut_loop_pair_loop_back'a_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (ListCons ret tl0)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       tl00 <-
+                         list_nth_mut_loop_pair_loop_back'a tl0 tl1 i0 ret;
+                       Return (ListCons x0 tl00)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_pair_loop_back'b_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (ListCons ret tl1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       tl10 <-
+                         list_nth_mut_loop_pair_loop_back'b tl0 tl1 i0 ret;
+                       Return (ListCons x1 tl10)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_pair_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_mut_loop_pair_loop_fwd tl0 tl1 i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_pair_merge_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_loop_pair_merge_back ls0 ls1 i ret =
+          list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret
+   
+   [list_nth_mut_loop_pair_merge_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_loop_pair_merge_fwd ls0 ls1 i =
+          list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i
+   
+   [list_nth_mut_loop_pair_merge_loop_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then
+                     (let
+                        (t,t0) = ret
+                      in
+                        Return (ListCons t tl0,ListCons t0 tl1))
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       (tl00,tl10) <-
+                         list_nth_mut_loop_pair_merge_loop_back tl0 tl1 i0
+                           ret;
+                       Return (ListCons x0 tl00,ListCons x1 tl10)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_pair_merge_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_with_id_back_def]  Definition
+      
+      ⊢ ∀ls i ret.
+          list_nth_mut_loop_with_id_back ls i ret =
+          do
+            ls0 <- id_mut_fwd ls;
+            l <- list_nth_mut_loop_with_id_loop_back i ls0 ret;
+            id_mut_back ls l
+          od
+   
+   [list_nth_mut_loop_with_id_fwd_def]  Definition
+      
+      ⊢ ∀ls i.
+          list_nth_mut_loop_with_id_fwd ls i =
+          do
+            ls0 <- id_mut_fwd ls;
+            list_nth_mut_loop_with_id_loop_fwd i ls0
+          od
+   
+   [list_nth_mut_loop_with_id_loop_back_def]  Definition
+      
+      ⊢ ∀i ls ret.
+          list_nth_mut_loop_with_id_loop_back i ls ret =
+          case ls of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return (ListCons ret tl)
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  tl0 <- list_nth_mut_loop_with_id_loop_back i0 tl ret;
+                  Return (ListCons x tl0)
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_loop_with_id_loop_fwd_def]  Definition
+      
+      ⊢ ∀i ls.
+          list_nth_mut_loop_with_id_loop_fwd i ls =
+          case ls of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_mut_loop_with_id_loop_fwd i0 tl
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_shared_loop_pair_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_shared_loop_pair_back ls0 ls1 i ret =
+          list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret
+   
+   [list_nth_mut_shared_loop_pair_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_shared_loop_pair_fwd ls0 ls1 i =
+          list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i
+   
+   [list_nth_mut_shared_loop_pair_loop_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (ListCons ret tl0)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       tl00 <-
+                         list_nth_mut_shared_loop_pair_loop_back tl0 tl1 i0
+                           ret;
+                       Return (ListCons x0 tl00)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_shared_loop_pair_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_mut_shared_loop_pair_loop_fwd tl0 tl1 i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_shared_loop_pair_merge_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_shared_loop_pair_merge_back ls0 ls1 i ret =
+          list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret
+   
+   [list_nth_mut_shared_loop_pair_merge_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_shared_loop_pair_merge_fwd ls0 ls1 i =
+          list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i
+   
+   [list_nth_mut_shared_loop_pair_merge_loop_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (ListCons ret tl0)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       tl00 <-
+                         list_nth_mut_shared_loop_pair_merge_loop_back tl0
+                           tl1 i0 ret;
+                       Return (ListCons x0 tl00)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_shared_loop_pair_merge_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_mut_shared_loop_pair_merge_loop_fwd tl0 tl1
+                         i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls i.
+          list_nth_shared_loop_fwd ls i =
+          list_nth_shared_loop_loop_fwd ls i
+   
+   [list_nth_shared_loop_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls i.
+          list_nth_shared_loop_loop_fwd ls i =
+          case ls of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_shared_loop_loop_fwd tl i0
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_loop_pair_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_loop_pair_fwd ls0 ls1 i =
+          list_nth_shared_loop_pair_loop_fwd ls0 ls1 i
+   
+   [list_nth_shared_loop_pair_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_shared_loop_pair_loop_fwd tl0 tl1 i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_loop_pair_merge_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_loop_pair_merge_fwd ls0 ls1 i =
+          list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i
+   
+   [list_nth_shared_loop_pair_merge_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_loop_with_id_fwd_def]  Definition
+      
+      ⊢ ∀ls i.
+          list_nth_shared_loop_with_id_fwd ls i =
+          do
+            ls0 <- id_shared_fwd ls;
+            list_nth_shared_loop_with_id_loop_fwd i ls0
+          od
+   
+   [list_nth_shared_loop_with_id_loop_fwd_def]  Definition
+      
+      ⊢ ∀i ls.
+          list_nth_shared_loop_with_id_loop_fwd i ls =
+          case ls of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_shared_loop_with_id_loop_fwd i0 tl
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_mut_loop_pair_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_shared_mut_loop_pair_back ls0 ls1 i ret =
+          list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret
+   
+   [list_nth_shared_mut_loop_pair_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_mut_loop_pair_fwd ls0 ls1 i =
+          list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i
+   
+   [list_nth_shared_mut_loop_pair_loop_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (ListCons ret tl1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       tl10 <-
+                         list_nth_shared_mut_loop_pair_loop_back tl0 tl1 i0
+                           ret;
+                       Return (ListCons x1 tl10)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_mut_loop_pair_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_shared_mut_loop_pair_loop_fwd tl0 tl1 i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_mut_loop_pair_merge_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_shared_mut_loop_pair_merge_back ls0 ls1 i ret =
+          list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret
+   
+   [list_nth_shared_mut_loop_pair_merge_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_mut_loop_pair_merge_fwd ls0 ls1 i =
+          list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i
+   
+   [list_nth_shared_mut_loop_pair_merge_loop_back_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i ret.
+          list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (ListCons ret tl1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       tl10 <-
+                         list_nth_shared_mut_loop_pair_merge_loop_back tl0
+                           tl1 i0 ret;
+                       Return (ListCons x1 tl10)
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_mut_loop_pair_merge_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls0 ls1 i.
+          list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =
+          case ls0 of
+            ListCons x0 tl0 =>
+              (case ls1 of
+                 ListCons x1 tl1 =>
+                   if i = int_to_u32 0 then Return (x0,x1)
+                   else
+                     do
+                       i0 <- u32_sub i (int_to_u32 1);
+                       list_nth_shared_mut_loop_pair_merge_loop_fwd tl0 tl1
+                         i0
+                     od
+               | ListNil => Fail Failure)
+          | ListNil => Fail Failure
+   
+   [sum_fwd_def]  Definition
+      
+      ⊢ ∀max. sum_fwd max = sum_loop_fwd max (int_to_u32 0) (int_to_u32 0)
+   
+   [sum_loop_fwd_def]  Definition
+      
+      ⊢ ∀max i s.
+          sum_loop_fwd max i s =
+          if u32_lt i max then
+            do
+              s0 <- u32_add s i;
+              i0 <- u32_add i (int_to_u32 1);
+              sum_loop_fwd max i0 s0
+            od
+          else u32_mul s (int_to_u32 2)
+   
+   [sum_with_mut_borrows_fwd_def]  Definition
+      
+      ⊢ ∀max.
+          sum_with_mut_borrows_fwd max =
+          sum_with_mut_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
+   
+   [sum_with_mut_borrows_loop_fwd_def]  Definition
+      
+      ⊢ ∀max mi ms.
+          sum_with_mut_borrows_loop_fwd max mi ms =
+          if u32_lt mi max then
+            do
+              ms0 <- u32_add ms mi;
+              mi0 <- u32_add mi (int_to_u32 1);
+              sum_with_mut_borrows_loop_fwd max mi0 ms0
+            od
+          else u32_mul ms (int_to_u32 2)
+   
+   [sum_with_shared_borrows_fwd_def]  Definition
+      
+      ⊢ ∀max.
+          sum_with_shared_borrows_fwd max =
+          sum_with_shared_borrows_loop_fwd max (int_to_u32 0)
+            (int_to_u32 0)
+   
+   [sum_with_shared_borrows_loop_fwd_def]  Definition
+      
+      ⊢ ∀max i s.
+          sum_with_shared_borrows_loop_fwd max i s =
+          if u32_lt i max then
+            do
+              i0 <- u32_add i (int_to_u32 1);
+              s0 <- u32_add s i0;
+              sum_with_shared_borrows_loop_fwd max i0 s0
+            od
+          else u32_mul s (int_to_u32 2)
+   
+   
+*)
+end
diff --git a/tests/hol4/loops/loops_TypesScript.sml b/tests/hol4/loops/loops_TypesScript.sml
new file mode 100644
index 00000000..e3e5b8d1
--- /dev/null
+++ b/tests/hol4/loops/loops_TypesScript.sml
@@ -0,0 +1,13 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: type definitions *)
+open primitivesLib divDefLib
+
+val _ = new_theory "loops_Types"
+
+
+Datatype:
+  (** [loops::List] *)
+  list_t = | ListCons 't list_t | ListNil
+End
+
+val _ = export_theory ()
diff --git a/tests/hol4/loops/loops_TypesTheory.sig b/tests/hol4/loops/loops_TypesTheory.sig
new file mode 100644
index 00000000..c3e638d8
--- /dev/null
+++ b/tests/hol4/loops/loops_TypesTheory.sig
@@ -0,0 +1,94 @@
+signature loops_TypesTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+  
+  (*  Theorems  *)
+    val datatype_list_t : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+  
+  val loops_Types_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [divDef] Parent theory of "loops_Types"
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   
+*)
+end