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