Regenerate the translated files for Lean

5 files changed, 0 insertions, 1441 deletions

diff --git a/tests/lean/betree/BetreeMain.lean b/tests/lean/betree/BetreeMain.lean
deleted file mode 100644
index 5f307877..00000000
--- a/tests/lean/betree/BetreeMain.lean
+++ /dev/null
@@ -1 +0,0 @@
-import BetreeMain.Funs
diff --git a/tests/lean/betree/BetreeMain/Clauses/Template.lean b/tests/lean/betree/BetreeMain/Clauses/Template.lean
deleted file mode 100644
index 1d18174e..00000000
--- a/tests/lean/betree/BetreeMain/Clauses/Template.lean
+++ /dev/null
@@ -1,185 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: templates for the decreases clauses
-import Base.Primitives
-import BetreeMain.Types
-
-/- [betree_main::betree::List::{1}::len]: termination measure -/
-@[simp]
-def betree_list_len_terminates (T : Type) (self : betree_list_t T) := self
-
-/- [betree_main::betree::List::{1}::len]: decreases_by tactic -/
-syntax "betree_list_len_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_list_len_decreases $self) =>`(tactic| sorry)
-
-/- [betree_main::betree::List::{1}::split_at]: termination measure -/
-@[simp]
-def betree_list_split_at_terminates (T : Type) (self : betree_list_t T)
-  (n : UInt64) :=
-  (self, n)
-
-/- [betree_main::betree::List::{1}::split_at]: decreases_by tactic -/
-syntax "betree_list_split_at_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_list_split_at_decreases $self $n) =>`(tactic| sorry)
-
-/- [betree_main::betree::List::{2}::partition_at_pivot]: termination measure -/
-@[simp]
-def betree_list_partition_at_pivot_terminates (T : Type)
-  (self : betree_list_t (UInt64 × T)) (pivot : UInt64) :=
-  (self, pivot)
-
-/- [betree_main::betree::List::{2}::partition_at_pivot]: decreases_by tactic -/
-syntax "betree_list_partition_at_pivot_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_list_partition_at_pivot_decreases $self $pivot) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: termination measure -/
-@[simp]
-def betree_node_lookup_in_bindings_terminates (key : UInt64)
-  (bindings : betree_list_t (UInt64 × UInt64)) :=
-  (key, bindings)
-
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases_by tactic -/
-syntax "betree_node_lookup_in_bindings_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_in_bindings_decreases $key $bindings) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: termination measure -/
-@[simp]
-def betree_node_lookup_first_message_for_key_terminates (key : UInt64)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (key, msgs)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases_by tactic -/
-syntax "betree_node_lookup_first_message_for_key_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_first_message_for_key_decreases $key $msgs) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_upserts]: termination measure -/
-@[simp]
-def betree_node_apply_upserts_terminates
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64)
-  (key : UInt64) (st : State) :=
-  (msgs, prev, key, st)
-
-/- [betree_main::betree::Node::{5}::apply_upserts]: decreases_by tactic -/
-syntax "betree_node_apply_upserts_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_upserts_decreases $msgs $prev $key $st) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup]: termination measure -/
-@[simp]
-def betree_node_lookup_terminates (self : betree_node_t) (key : UInt64)
-  (st : State) :=
-  (self, key, st)
-
-/- [betree_main::betree::Node::{5}::lookup]: decreases_by tactic -/
-syntax "betree_node_lookup_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_decreases $self $key $st) =>`(tactic| sorry)
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: termination measure -/
-@[simp]
-def betree_internal_lookup_in_children_terminates (self : betree_internal_t)
-  (key : UInt64) (st : State) :=
-  (self, key, st)
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: decreases_by tactic -/
-syntax "betree_internal_lookup_in_children_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_internal_lookup_in_children_decreases $self $key $st) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: termination measure -/
-@[simp]
-def betree_node_lookup_mut_in_bindings_terminates (key : UInt64)
-  (bindings : betree_list_t (UInt64 × UInt64)) :=
-  (key, bindings)
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases_by tactic -/
-syntax "betree_node_lookup_mut_in_bindings_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_mut_in_bindings_decreases $key $bindings) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: termination measure -/
-@[simp]
-def betree_node_apply_messages_to_leaf_terminates
-  (bindings : betree_list_t (UInt64 × UInt64))
-  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (bindings, new_msgs)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases_by tactic -/
-syntax "betree_node_apply_messages_to_leaf_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_messages_to_leaf_decreases $bindings
-$new_msgs) =>`(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::filter_messages_for_key]: termination measure -/
-@[simp]
-def betree_node_filter_messages_for_key_terminates (key : UInt64)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (key, msgs)
-
-/- [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases_by tactic -/
-syntax "betree_node_filter_messages_for_key_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_filter_messages_for_key_decreases $key $msgs) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: termination measure -/
-@[simp]
-def betree_node_lookup_first_message_after_key_terminates (key : UInt64)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (key, msgs)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases_by tactic -/
-syntax "betree_node_lookup_first_message_after_key_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_first_message_after_key_decreases $key $msgs) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: termination measure -/
-@[simp]
-def betree_node_apply_messages_to_internal_terminates
-  (msgs : betree_list_t (UInt64 × betree_message_t))
-  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (msgs, new_msgs)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases_by tactic -/
-syntax "betree_node_apply_messages_to_internal_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_messages_to_internal_decreases $msgs
-$new_msgs) =>`(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_messages]: termination measure -/
-@[simp]
-def betree_node_apply_messages_terminates (self : betree_node_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) :=
-  (self, params, node_id_cnt, msgs, st)
-
-/- [betree_main::betree::Node::{5}::apply_messages]: decreases_by tactic -/
-syntax "betree_node_apply_messages_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_messages_decreases $self $params $node_id_cnt
-$msgs $st) =>`(tactic| sorry)
-
-/- [betree_main::betree::Internal::{4}::flush]: termination measure -/
-@[simp]
-def betree_internal_flush_terminates (self : betree_internal_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (UInt64 × betree_message_t)) (st : State) :=
-  (self, params, node_id_cnt, content, st)
-
-/- [betree_main::betree::Internal::{4}::flush]: decreases_by tactic -/
-syntax "betree_internal_flush_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_internal_flush_decreases $self $params $node_id_cnt $content
-$st) =>`(tactic| sorry)
-
diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean
deleted file mode 100644
index 7177e2ec..00000000
--- a/tests/lean/betree/BetreeMain/Funs.lean
+++ /dev/null
@@ -1,1167 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: function definitions
-import Base.Primitives
-import BetreeMain.Types
-import BetreeMain.Opaque
-import BetreeMain.Clauses.Clauses
-
-section variable (opaque_defs: OpaqueDefs)
-
-/- [betree_main::betree::load_internal_node] -/
-def betree_load_internal_node_fwd
-  (id : UInt64) (st : State) :
-  Result (State × (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  opaque_defs.betree_utils_load_internal_node_fwd id st
-
-/- [betree_main::betree::store_internal_node] -/
-def betree_store_internal_node_fwd
-  (id : UInt64) (content : betree_list_t (UInt64 × betree_message_t))
-  (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      opaque_defs.betree_utils_store_internal_node_fwd id content st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::load_leaf_node] -/
-def betree_load_leaf_node_fwd
-  (id : UInt64) (st : State) :
-  Result (State × (betree_list_t (UInt64 × UInt64)))
-  :=
-  opaque_defs.betree_utils_load_leaf_node_fwd id st
-
-/- [betree_main::betree::store_leaf_node] -/
-def betree_store_leaf_node_fwd
-  (id : UInt64) (content : betree_list_t (UInt64 × UInt64)) (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ← opaque_defs.betree_utils_store_leaf_node_fwd id content st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::fresh_node_id] -/
-def betree_fresh_node_id_fwd (counter : UInt64) : Result UInt64 :=
-  do
-    let _ ← UInt64.checked_add counter (UInt64.ofNatCore 1 (by intlit))
-    Result.ret counter
-
-/- [betree_main::betree::fresh_node_id] -/
-def betree_fresh_node_id_back (counter : UInt64) : Result UInt64 :=
-  UInt64.checked_add counter (UInt64.ofNatCore 1 (by intlit))
-
-/- [betree_main::betree::NodeIdCounter::{0}::new] -/
-def betree_node_id_counter_new_fwd : Result betree_node_id_counter_t :=
-  Result.ret
-  { betree_node_id_counter_next_node_id := (UInt64.ofNatCore 0 (by intlit)) }
-
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id] -/
-def betree_node_id_counter_fresh_id_fwd
-  (self : betree_node_id_counter_t) : Result UInt64 :=
-  do
-    let _ ← UInt64.checked_add self.betree_node_id_counter_next_node_id
-      (UInt64.ofNatCore 1 (by intlit))
-    Result.ret self.betree_node_id_counter_next_node_id
-
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id] -/
-def betree_node_id_counter_fresh_id_back
-  (self : betree_node_id_counter_t) : Result betree_node_id_counter_t :=
-  do
-    let i ← UInt64.checked_add self.betree_node_id_counter_next_node_id
-      (UInt64.ofNatCore 1 (by intlit))
-    Result.ret { betree_node_id_counter_next_node_id := i }
-
-/- [core::num::u64::{10}::MAX] -/
-def core_num_u64_max_body : Result UInt64 :=
-  Result.ret (UInt64.ofNatCore 18446744073709551615 (by intlit))
-def core_num_u64_max_c : UInt64 := eval_global core_num_u64_max_body (by simp)
-
-/- [betree_main::betree::upsert_update] -/
-def betree_upsert_update_fwd
-  (prev : Option UInt64) (st : betree_upsert_fun_state_t) : Result UInt64 :=
-  match h: prev with
-  | Option.none =>
-    match h: st with
-    | betree_upsert_fun_state_t.Add v => Result.ret v
-    | betree_upsert_fun_state_t.Sub i =>
-      Result.ret (UInt64.ofNatCore 0 (by intlit))
-  | Option.some prev0 =>
-    match h: st with
-    | betree_upsert_fun_state_t.Add v =>
-      do
-        let margin ← UInt64.checked_sub core_num_u64_max_c prev0
-        if h: margin >= v
-        then UInt64.checked_add prev0 v
-        else Result.ret core_num_u64_max_c
-    | betree_upsert_fun_state_t.Sub v =>
-      if h: prev0 >= v
-      then UInt64.checked_sub prev0 v
-      else Result.ret (UInt64.ofNatCore 0 (by intlit))
-
-/- [betree_main::betree::List::{1}::len] -/
-def betree_list_len_fwd
-  (T : Type) (self : betree_list_t T) : (Result UInt64) :=
-  match h: self with
-  | betree_list_t.Cons t tl =>
-    do
-      let i ← betree_list_len_fwd T tl
-      UInt64.checked_add (UInt64.ofNatCore 1 (by intlit)) i
-  | betree_list_t.Nil => Result.ret (UInt64.ofNatCore 0 (by intlit))
-termination_by betree_list_len_fwd self => betree_list_len_terminates T self
-decreasing_by betree_list_len_decreases self
-
-/- [betree_main::betree::List::{1}::split_at] -/
-def betree_list_split_at_fwd
-  (T : Type) (self : betree_list_t T) (n : UInt64) :
-  (Result ((betree_list_t T) × (betree_list_t T)))
-  :=
-  if h: n = (UInt64.ofNatCore 0 (by intlit))
-  then Result.ret (betree_list_t.Nil, self)
-  else
-    match h: self with
-    | betree_list_t.Cons hd tl =>
-      do
-        let i ← UInt64.checked_sub n (UInt64.ofNatCore 1 (by intlit))
-        let p ← betree_list_split_at_fwd T tl i
-        let (ls0, ls1) := p
-        let l := ls0
-        Result.ret (betree_list_t.Cons hd l, ls1)
-    | betree_list_t.Nil => Result.fail Error.panic
-termination_by betree_list_split_at_fwd self n =>
-  betree_list_split_at_terminates T self n
-decreasing_by betree_list_split_at_decreases self n
-
-/- [betree_main::betree::List::{1}::push_front] -/
-def betree_list_push_front_fwd_back
-  (T : Type) (self : betree_list_t T) (x : T) : Result (betree_list_t T) :=
-  let tl := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
-  let l := tl
-  Result.ret (betree_list_t.Cons x l)
-
-/- [betree_main::betree::List::{1}::pop_front] -/
-def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T :=
-  let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
-  match h: ls with
-  | betree_list_t.Cons x tl => Result.ret x
-  | betree_list_t.Nil => Result.fail Error.panic
-
-/- [betree_main::betree::List::{1}::pop_front] -/
-def betree_list_pop_front_back
-  (T : Type) (self : betree_list_t T) : Result (betree_list_t T) :=
-  let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
-  match h: ls with
-  | betree_list_t.Cons x tl => Result.ret tl
-  | betree_list_t.Nil => Result.fail Error.panic
-
-/- [betree_main::betree::List::{1}::hd] -/
-def betree_list_hd_fwd (T : Type) (self : betree_list_t T) : Result T :=
-  match h: self with
-  | betree_list_t.Cons hd l => Result.ret hd
-  | betree_list_t.Nil => Result.fail Error.panic
-
-/- [betree_main::betree::List::{2}::head_has_key] -/
-def betree_list_head_has_key_fwd
-  (T : Type) (self : betree_list_t (UInt64 × T)) (key : UInt64) :
-  Result Bool
-  :=
-  match h: self with
-  | betree_list_t.Cons hd l => let (i, _) := hd
-                               Result.ret (i = key)
-  | betree_list_t.Nil => Result.ret false
-
-/- [betree_main::betree::List::{2}::partition_at_pivot] -/
-def betree_list_partition_at_pivot_fwd
-  (T : Type) (self : betree_list_t (UInt64 × T)) (pivot : UInt64) :
-  (Result ((betree_list_t (UInt64 × T)) × (betree_list_t (UInt64 × T))))
-  :=
-  match h: self with
-  | betree_list_t.Cons hd tl =>
-    let (i, t) := hd
-    if h: i >= pivot
-    then Result.ret (betree_list_t.Nil, betree_list_t.Cons (i, t) tl)
-    else
-      do
-        let p ← betree_list_partition_at_pivot_fwd T tl pivot
-        let (ls0, ls1) := p
-        let l := ls0
-        Result.ret (betree_list_t.Cons (i, t) l, ls1)
-  | betree_list_t.Nil => Result.ret (betree_list_t.Nil, betree_list_t.Nil)
-termination_by betree_list_partition_at_pivot_fwd self pivot =>
-  betree_list_partition_at_pivot_terminates T self pivot
-decreasing_by betree_list_partition_at_pivot_decreases self pivot
-
-/- [betree_main::betree::Leaf::{3}::split] -/
-def betree_leaf_split_fwd
-  (self : betree_leaf_t) (content : betree_list_t (UInt64 × UInt64))
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (st : State) :
-  Result (State × betree_internal_t)
-  :=
-  do
-    let p ←
-      betree_list_split_at_fwd (UInt64 × UInt64) content
-        params.betree_params_split_size
-    let (content0, content1) := p
-    let p0 ← betree_list_hd_fwd (UInt64 × UInt64) content1
-    let (pivot, _) := p0
-    let id0 ← betree_node_id_counter_fresh_id_fwd node_id_cnt
-    let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt
-    let id1 ← betree_node_id_counter_fresh_id_fwd node_id_cnt0
-    let (st0, _) ← betree_store_leaf_node_fwd id0 content0 st
-    let (st1, _) ← betree_store_leaf_node_fwd id1 content1 st0
-    let n := betree_node_t.Leaf
-      {
-        betree_leaf_id := id0,
-        betree_leaf_size := params.betree_params_split_size
-      }
-    let n0 := betree_node_t.Leaf
-      {
-        betree_leaf_id := id1,
-        betree_leaf_size := params.betree_params_split_size
-      }
-    Result.ret (st1, mkbetree_internal_t self.betree_leaf_id pivot n n0)
-
-/- [betree_main::betree::Leaf::{3}::split] -/
-def betree_leaf_split_back
-  (self : betree_leaf_t) (content : betree_list_t (UInt64 × UInt64))
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (st : State) :
-  Result betree_node_id_counter_t
-  :=
-  do
-    let p ←
-      betree_list_split_at_fwd (UInt64 × UInt64) content
-        params.betree_params_split_size
-    let (content0, content1) := p
-    let _ ← betree_list_hd_fwd (UInt64 × UInt64) content1
-    let id0 ← betree_node_id_counter_fresh_id_fwd node_id_cnt
-    let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt
-    let id1 ← betree_node_id_counter_fresh_id_fwd node_id_cnt0
-    let (st0, _) ← betree_store_leaf_node_fwd id0 content0 st
-    let _ ← betree_store_leaf_node_fwd id1 content1 st0
-    betree_node_id_counter_fresh_id_back node_id_cnt0
-
-/- [betree_main::betree::Node::{5}::lookup_in_bindings] -/
-def betree_node_lookup_in_bindings_fwd
-  (key : UInt64) (bindings : betree_list_t (UInt64 × UInt64)) :
-  (Result (Option UInt64))
-  :=
-  match h: bindings with
-  | betree_list_t.Cons hd tl =>
-    let (i, i0) := hd
-    if h: i = key
-    then Result.ret (Option.some i0)
-    else
-      if h: i > key
-      then Result.ret Option.none
-      else betree_node_lookup_in_bindings_fwd key tl
-  | betree_list_t.Nil => Result.ret Option.none
-termination_by betree_node_lookup_in_bindings_fwd key bindings =>
-  betree_node_lookup_in_bindings_terminates key bindings
-decreasing_by betree_node_lookup_in_bindings_decreases key bindings
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key] -/
-def betree_node_lookup_first_message_for_key_fwd
-  (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  match h: msgs with
-  | betree_list_t.Cons x next_msgs =>
-    let (i, m) := x
-    if h: i >= key
-    then Result.ret (betree_list_t.Cons (i, m) next_msgs)
-    else betree_node_lookup_first_message_for_key_fwd key next_msgs
-  | betree_list_t.Nil => Result.ret betree_list_t.Nil
-termination_by betree_node_lookup_first_message_for_key_fwd key msgs =>
-  betree_node_lookup_first_message_for_key_terminates key msgs
-decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key] -/
-def betree_node_lookup_first_message_for_key_back
-  (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t))
-  (ret0 : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  match h: msgs with
-  | betree_list_t.Cons x next_msgs =>
-    let (i, m) := x
-    if h: i >= key
-    then Result.ret ret0
-    else
-      do
-        let next_msgs0 ←
-          betree_node_lookup_first_message_for_key_back key next_msgs ret0
-        Result.ret (betree_list_t.Cons (i, m) next_msgs0)
-  | betree_list_t.Nil => Result.ret ret0
-termination_by betree_node_lookup_first_message_for_key_back key msgs ret0 =>
-  betree_node_lookup_first_message_for_key_terminates key msgs
-decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs
-
-/- [betree_main::betree::Node::{5}::apply_upserts] -/
-def betree_node_apply_upserts_fwd
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64)
-  (key : UInt64) (st : State) :
-  (Result (State × UInt64))
-  :=
-  do
-    let b ← betree_list_head_has_key_fwd betree_message_t msgs key
-    if h: b
-    then
-      do
-        let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs
-        let (_, m) := msg
-        match h: m with
-        | betree_message_t.Insert i => Result.fail Error.panic
-        | betree_message_t.Delete => Result.fail Error.panic
-        | betree_message_t.Upsert s =>
-          do
-            let v ← betree_upsert_update_fwd prev s
-            let msgs0 ←
-              betree_list_pop_front_back (UInt64 × betree_message_t) msgs
-            betree_node_apply_upserts_fwd msgs0 (Option.some v) key st
-    else
-      do
-        let (st0, v) ←
-          opaque_defs.core_option_option_unwrap_fwd UInt64 prev st
-        let _ ←
-          betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs
-            (key, betree_message_t.Insert v)
-        Result.ret (st0, v)
-termination_by betree_node_apply_upserts_fwd msgs prev key st =>
-  betree_node_apply_upserts_terminates msgs prev key st
-decreasing_by betree_node_apply_upserts_decreases msgs prev key st
-
-/- [betree_main::betree::Node::{5}::apply_upserts] -/
-def betree_node_apply_upserts_back
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64)
-  (key : UInt64) (st : State) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  do
-    let b ← betree_list_head_has_key_fwd betree_message_t msgs key
-    if h: b
-    then
-      do
-        let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs
-        let (_, m) := msg
-        match h: m with
-        | betree_message_t.Insert i => Result.fail Error.panic
-        | betree_message_t.Delete => Result.fail Error.panic
-        | betree_message_t.Upsert s =>
-          do
-            let v ← betree_upsert_update_fwd prev s
-            let msgs0 ←
-              betree_list_pop_front_back (UInt64 × betree_message_t) msgs
-            betree_node_apply_upserts_back msgs0 (Option.some v) key st
-    else
-      do
-        let (_, v) ← opaque_defs.core_option_option_unwrap_fwd UInt64 prev st
-        betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs (key,
-          betree_message_t.Insert v)
-termination_by betree_node_apply_upserts_back msgs prev key st =>
-  betree_node_apply_upserts_terminates msgs prev key st
-decreasing_by betree_node_apply_upserts_decreases msgs prev key st
-
-/- [betree_main::betree::Node::{5}::lookup] -/
-mutual def betree_node_lookup_fwd
-  (self : betree_node_t) (key : UInt64) (st : State) :
-  (Result (State × (Option UInt64)))
-  :=
-  match h: self with
-  | betree_node_t.Internal node =>
-    do
-      let (mkbetree_internal_t i i0 n n0) := node
-      let (st0, msgs) ← betree_load_internal_node_fwd i st
-      let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
-      match h: pending with
-      | betree_list_t.Cons p l =>
-        let (k, msg) := p
-        if h: k != key
-        then
-          do
-            let (st1, opt) ←
-              betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0
-                n n0) key st0
-            let _ ←
-              betree_node_lookup_first_message_for_key_back key msgs
-                (betree_list_t.Cons (k, msg) l)
-            Result.ret (st1, opt)
-        else
-          match h: msg with
-          | betree_message_t.Insert v =>
-            do
-              let _ ←
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.Cons (k, betree_message_t.Insert v) l)
-              Result.ret (st0, Option.some v)
-          | betree_message_t.Delete =>
-            do
-              let _ ←
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.Cons (k, betree_message_t.Delete) l)
-              Result.ret (st0, Option.none)
-          | betree_message_t.Upsert ufs =>
-            do
-              let (st1, v) ←
-                betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
-                  i0 n n0) key st0
-              let (st2, v0) ←
-                betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
-                  betree_message_t.Upsert ufs) l) v key st1
-              let node0 ←
-                betree_internal_lookup_in_children_back (mkbetree_internal_t i
-                  i0 n n0) key st0
-              let (mkbetree_internal_t i1 _ _ _) := node0
-              let pending0 ←
-                betree_node_apply_upserts_back (betree_list_t.Cons (k,
-                  betree_message_t.Upsert ufs) l) v key st1
-              let msgs0 ←
-                betree_node_lookup_first_message_for_key_back key msgs pending0
-              let (st3, _) ← betree_store_internal_node_fwd i1 msgs0 st2
-              Result.ret (st3, Option.some v0)
-      | betree_list_t.Nil =>
-        do
-          let (st1, opt) ←
-            betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n
-              n0) key st0
-          let _ ←
-            betree_node_lookup_first_message_for_key_back key msgs
-              betree_list_t.Nil
-          Result.ret (st1, opt)
-  | betree_node_t.Leaf node =>
-    do
-      let (st0, bindings) ← betree_load_leaf_node_fwd node.betree_leaf_id st
-      let opt ← betree_node_lookup_in_bindings_fwd key bindings
-      Result.ret (st0, opt)
-termination_by betree_node_lookup_fwd self key st =>
-  betree_node_lookup_terminates self key st
-decreasing_by betree_node_lookup_decreases self key st
-
-/- [betree_main::betree::Node::{5}::lookup] -/
-def betree_node_lookup_back
-  (self : betree_node_t) (key : UInt64) (st : State) :
-  (Result betree_node_t)
-  :=
-  match h: self with
-  | betree_node_t.Internal node =>
-    do
-      let (mkbetree_internal_t i i0 n n0) := node
-      let (st0, msgs) ← betree_load_internal_node_fwd i st
-      let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
-      match h: pending with
-      | betree_list_t.Cons p l =>
-        let (k, msg) := p
-        if h: k != key
-        then
-          do
-            let _ ←
-              betree_node_lookup_first_message_for_key_back key msgs
-                (betree_list_t.Cons (k, msg) l)
-            let node0 ←
-              betree_internal_lookup_in_children_back (mkbetree_internal_t i i0
-                n n0) key st0
-            Result.ret (betree_node_t.Internal node0)
-        else
-          match h: msg with
-          | betree_message_t.Insert v =>
-            do
-              let _ ←
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.Cons (k, betree_message_t.Insert v) l)
-              Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
-                n0))
-          | betree_message_t.Delete =>
-            do
-              let _ ←
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.Cons (k, betree_message_t.Delete) l)
-              Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
-                n0))
-          | betree_message_t.Upsert ufs =>
-            do
-              let (st1, v) ←
-                betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
-                  i0 n n0) key st0
-              let (st2, _) ←
-                betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
-                  betree_message_t.Upsert ufs) l) v key st1
-              let node0 ←
-                betree_internal_lookup_in_children_back (mkbetree_internal_t i
-                  i0 n n0) key st0
-              let (mkbetree_internal_t i1 i2 n1 n2) := node0
-              let pending0 ←
-                betree_node_apply_upserts_back (betree_list_t.Cons (k,
-                  betree_message_t.Upsert ufs) l) v key st1
-              let msgs0 ←
-                betree_node_lookup_first_message_for_key_back key msgs pending0
-              let _ ← betree_store_internal_node_fwd i1 msgs0 st2
-              Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1
-                n2))
-      | betree_list_t.Nil =>
-        do
-          let _ ←
-            betree_node_lookup_first_message_for_key_back key msgs
-              betree_list_t.Nil
-          let node0 ←
-            betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n
-              n0) key st0
-          Result.ret (betree_node_t.Internal node0)
-  | betree_node_t.Leaf node =>
-    do
-      let (_, bindings) ← betree_load_leaf_node_fwd node.betree_leaf_id st
-      let _ ← betree_node_lookup_in_bindings_fwd key bindings
-      Result.ret (betree_node_t.Leaf node)
-termination_by betree_node_lookup_back self key st =>
-  betree_node_lookup_terminates self key st
-decreasing_by betree_node_lookup_decreases self key st
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children] -/
-def betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : UInt64) (st : State) :
-  (Result (State × (Option UInt64)))
-  :=
-  let (mkbetree_internal_t _ i n n0) := self
-  if h: key < i
-  then betree_node_lookup_fwd n key st
-  else betree_node_lookup_fwd n0 key st
-termination_by betree_internal_lookup_in_children_fwd self key st =>
-  betree_internal_lookup_in_children_terminates self key st
-decreasing_by betree_internal_lookup_in_children_decreases self key st
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children] -/
-def betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : UInt64) (st : State) :
-  (Result betree_internal_t)
-  :=
-  let (mkbetree_internal_t i i0 n n0) := self
-  if h: key < i0
-  then
-    do
-      let n1 ← betree_node_lookup_back n key st
-      Result.ret (mkbetree_internal_t i i0 n1 n0)
-  else
-    do
-      let n1 ← betree_node_lookup_back n0 key st
-      Result.ret (mkbetree_internal_t i i0 n n1)
-termination_by betree_internal_lookup_in_children_back self key st =>
-  betree_internal_lookup_in_children_terminates self key st
-decreasing_by betree_internal_lookup_in_children_decreases self key st
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings] -/
-def betree_node_lookup_mut_in_bindings_fwd
-  (key : UInt64) (bindings : betree_list_t (UInt64 × UInt64)) :
-  (Result (betree_list_t (UInt64 × UInt64)))
-  :=
-  match h: bindings with
-  | betree_list_t.Cons hd tl =>
-    let (i, i0) := hd
-    if h: i >= key
-    then Result.ret (betree_list_t.Cons (i, i0) tl)
-    else betree_node_lookup_mut_in_bindings_fwd key tl
-  | betree_list_t.Nil => Result.ret betree_list_t.Nil
-termination_by betree_node_lookup_mut_in_bindings_fwd key bindings =>
-  betree_node_lookup_mut_in_bindings_terminates key bindings
-decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings] -/
-def betree_node_lookup_mut_in_bindings_back
-  (key : UInt64) (bindings : betree_list_t (UInt64 × UInt64))
-  (ret0 : betree_list_t (UInt64 × UInt64)) :
-  (Result (betree_list_t (UInt64 × UInt64)))
-  :=
-  match h: bindings with
-  | betree_list_t.Cons hd tl =>
-    let (i, i0) := hd
-    if h: i >= key
-    then Result.ret ret0
-    else
-      do
-        let tl0 ← betree_node_lookup_mut_in_bindings_back key tl ret0
-        Result.ret (betree_list_t.Cons (i, i0) tl0)
-  | betree_list_t.Nil => Result.ret ret0
-termination_by betree_node_lookup_mut_in_bindings_back key bindings ret0 =>
-  betree_node_lookup_mut_in_bindings_terminates key bindings
-decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings
-
-/- [betree_main::betree::Node::{5}::apply_to_leaf] -/
-def betree_node_apply_to_leaf_fwd_back
-  (bindings : betree_list_t (UInt64 × UInt64)) (key : UInt64)
-  (new_msg : betree_message_t) :
-  Result (betree_list_t (UInt64 × UInt64))
-  :=
-  do
-    let bindings0 ← betree_node_lookup_mut_in_bindings_fwd key bindings
-    let b ← betree_list_head_has_key_fwd UInt64 bindings0 key
-    if h: b
-    then
-      do
-        let hd ← betree_list_pop_front_fwd (UInt64 × UInt64) bindings0
-        match h: new_msg with
-        | betree_message_t.Insert v =>
-          do
-            let bindings1 ←
-              betree_list_pop_front_back (UInt64 × UInt64) bindings0
-            let bindings2 ←
-              betree_list_push_front_fwd_back (UInt64 × UInt64) bindings1
-                (key, v)
-            betree_node_lookup_mut_in_bindings_back key bindings bindings2
-        | betree_message_t.Delete =>
-          do
-            let bindings1 ←
-              betree_list_pop_front_back (UInt64 × UInt64) bindings0
-            betree_node_lookup_mut_in_bindings_back key bindings bindings1
-        | betree_message_t.Upsert s =>
-          do
-            let (_, i) := hd
-            let v ← betree_upsert_update_fwd (Option.some i) s
-            let bindings1 ←
-              betree_list_pop_front_back (UInt64 × UInt64) bindings0
-            let bindings2 ←
-              betree_list_push_front_fwd_back (UInt64 × UInt64) bindings1
-                (key, v)
-            betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    else
-      match h: new_msg with
-      | betree_message_t.Insert v =>
-        do
-          let bindings1 ←
-            betree_list_push_front_fwd_back (UInt64 × UInt64) bindings0 (key,
-              v)
-          betree_node_lookup_mut_in_bindings_back key bindings bindings1
-      | betree_message_t.Delete =>
-        betree_node_lookup_mut_in_bindings_back key bindings bindings0
-      | betree_message_t.Upsert s =>
-        do
-          let v ← betree_upsert_update_fwd Option.none s
-          let bindings1 ←
-            betree_list_push_front_fwd_back (UInt64 × UInt64) bindings0 (key,
-              v)
-          betree_node_lookup_mut_in_bindings_back key bindings bindings1
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf] -/
-def betree_node_apply_messages_to_leaf_fwd_back
-  (bindings : betree_list_t (UInt64 × UInt64))
-  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × UInt64)))
-  :=
-  match h: new_msgs with
-  | betree_list_t.Cons new_msg new_msgs_tl =>
-    do
-      let (i, m) := new_msg
-      let bindings0 ← betree_node_apply_to_leaf_fwd_back bindings i m
-      betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-  | betree_list_t.Nil => Result.ret bindings
-termination_by betree_node_apply_messages_to_leaf_fwd_back bindings new_msgs =>
-  betree_node_apply_messages_to_leaf_terminates bindings new_msgs
-decreasing_by betree_node_apply_messages_to_leaf_decreases bindings new_msgs
-
-/- [betree_main::betree::Node::{5}::filter_messages_for_key] -/
-def betree_node_filter_messages_for_key_fwd_back
-  (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  match h: msgs with
-  | betree_list_t.Cons p l =>
-    let (k, m) := p
-    if h: k = key
-    then
-      do
-        let msgs0 ←
-          betree_list_pop_front_back (UInt64 × betree_message_t)
-            (betree_list_t.Cons (k, m) l)
-        betree_node_filter_messages_for_key_fwd_back key msgs0
-    else Result.ret (betree_list_t.Cons (k, m) l)
-  | betree_list_t.Nil => Result.ret betree_list_t.Nil
-termination_by betree_node_filter_messages_for_key_fwd_back key msgs =>
-  betree_node_filter_messages_for_key_terminates key msgs
-decreasing_by betree_node_filter_messages_for_key_decreases key msgs
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key] -/
-def betree_node_lookup_first_message_after_key_fwd
-  (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  match h: msgs with
-  | betree_list_t.Cons p next_msgs =>
-    let (k, m) := p
-    if h: k = key
-    then betree_node_lookup_first_message_after_key_fwd key next_msgs
-    else Result.ret (betree_list_t.Cons (k, m) next_msgs)
-  | betree_list_t.Nil => Result.ret betree_list_t.Nil
-termination_by betree_node_lookup_first_message_after_key_fwd key msgs =>
-  betree_node_lookup_first_message_after_key_terminates key msgs
-decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key] -/
-def betree_node_lookup_first_message_after_key_back
-  (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t))
-  (ret0 : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  match h: msgs with
-  | betree_list_t.Cons p next_msgs =>
-    let (k, m) := p
-    if h: k = key
-    then
-      do
-        let next_msgs0 ←
-          betree_node_lookup_first_message_after_key_back key next_msgs ret0
-        Result.ret (betree_list_t.Cons (k, m) next_msgs0)
-    else Result.ret ret0
-  | betree_list_t.Nil => Result.ret ret0
-termination_by betree_node_lookup_first_message_after_key_back key msgs ret0 =>
-  betree_node_lookup_first_message_after_key_terminates key msgs
-decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs
-
-/- [betree_main::betree::Node::{5}::apply_to_internal] -/
-def betree_node_apply_to_internal_fwd_back
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (key : UInt64)
-  (new_msg : betree_message_t) :
-  Result (betree_list_t (UInt64 × betree_message_t))
-  :=
-  do
-    let msgs0 ← betree_node_lookup_first_message_for_key_fwd key msgs
-    let b ← betree_list_head_has_key_fwd betree_message_t msgs0 key
-    if h: b
-    then
-      match h: new_msg with
-      | betree_message_t.Insert i =>
-        do
-          let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0
-          let msgs2 ←
-            betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1
-              (key, betree_message_t.Insert i)
-          betree_node_lookup_first_message_for_key_back key msgs msgs2
-      | betree_message_t.Delete =>
-        do
-          let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0
-          let msgs2 ←
-            betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1
-              (key, betree_message_t.Delete)
-          betree_node_lookup_first_message_for_key_back key msgs msgs2
-      | betree_message_t.Upsert s =>
-        do
-          let p ← betree_list_hd_fwd (UInt64 × betree_message_t) msgs0
-          let (_, m) := p
-          match h: m with
-          | betree_message_t.Insert prev =>
-            do
-              let v ← betree_upsert_update_fwd (Option.some prev) s
-              let msgs1 ←
-                betree_list_pop_front_back (UInt64 × betree_message_t) msgs0
-              let msgs2 ←
-                betree_list_push_front_fwd_back (UInt64 × betree_message_t)
-                  msgs1 (key, betree_message_t.Insert v)
-              betree_node_lookup_first_message_for_key_back key msgs msgs2
-          | betree_message_t.Delete =>
-            do
-              let v ← betree_upsert_update_fwd Option.none s
-              let msgs1 ←
-                betree_list_pop_front_back (UInt64 × betree_message_t) msgs0
-              let msgs2 ←
-                betree_list_push_front_fwd_back (UInt64 × betree_message_t)
-                  msgs1 (key, betree_message_t.Insert v)
-              betree_node_lookup_first_message_for_key_back key msgs msgs2
-          | betree_message_t.Upsert ufs =>
-            do
-              let msgs1 ←
-                betree_node_lookup_first_message_after_key_fwd key msgs0
-              let msgs2 ←
-                betree_list_push_front_fwd_back (UInt64 × betree_message_t)
-                  msgs1 (key, betree_message_t.Upsert s)
-              let msgs3 ←
-                betree_node_lookup_first_message_after_key_back key msgs0 msgs2
-              betree_node_lookup_first_message_for_key_back key msgs msgs3
-    else
-      do
-        let msgs1 ←
-          betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs0
-            (key, new_msg)
-        betree_node_lookup_first_message_for_key_back key msgs msgs1
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal] -/
-def betree_node_apply_messages_to_internal_fwd_back
-  (msgs : betree_list_t (UInt64 × betree_message_t))
-  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :
-  (Result (betree_list_t (UInt64 × betree_message_t)))
-  :=
-  match h: new_msgs with
-  | betree_list_t.Cons new_msg new_msgs_tl =>
-    do
-      let (i, m) := new_msg
-      let msgs0 ← betree_node_apply_to_internal_fwd_back msgs i m
-      betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl
-  | betree_list_t.Nil => Result.ret msgs
-termination_by betree_node_apply_messages_to_internal_fwd_back msgs new_msgs =>
-  betree_node_apply_messages_to_internal_terminates msgs new_msgs
-decreasing_by betree_node_apply_messages_to_internal_decreases msgs new_msgs
-
-/- [betree_main::betree::Node::{5}::apply_messages] -/
-mutual def betree_node_apply_messages_fwd
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) :
-  (Result (State × Unit))
-  :=
-  match h: self with
-  | betree_node_t.Internal node =>
-    do
-      let (mkbetree_internal_t i i0 n n0) := node
-      let (st0, content) ← betree_load_internal_node_fwd i st
-      let content0 ←
-        betree_node_apply_messages_to_internal_fwd_back content msgs
-      let num_msgs ←
-        betree_list_len_fwd (UInt64 × betree_message_t) content0
-      if h: num_msgs >= params.betree_params_min_flush_size
-      then
-        do
-          let (st1, content1) ←
-            betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
-              node_id_cnt content0 st0
-          let (node0, _) ←
-            betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
-              node_id_cnt content0 st0
-          let (mkbetree_internal_t i1 _ _ _) := node0
-          let (st2, _) ← betree_store_internal_node_fwd i1 content1 st1
-          Result.ret (st2, ())
-      else
-        do
-          let (st1, _) ← betree_store_internal_node_fwd i content0 st0
-          Result.ret (st1, ())
-  | betree_node_t.Leaf node =>
-    do
-      let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st
-      let content0 ← betree_node_apply_messages_to_leaf_fwd_back content msgs
-      let len ← betree_list_len_fwd (UInt64 × UInt64) content0
-      let i ← UInt64.checked_mul (UInt64.ofNatCore 2 (by intlit))
-        params.betree_params_split_size
-      if h: len >= i
-      then
-        do
-          let (st1, _) ←
-            betree_leaf_split_fwd node content0 params node_id_cnt st0
-          let (st2, _) ←
-            betree_store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil
-              st1
-          Result.ret (st2, ())
-      else
-        do
-          let (st1, _) ←
-            betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
-          Result.ret (st1, ())
-termination_by betree_node_apply_messages_fwd self params node_id_cnt msgs st
-  =>
-  betree_node_apply_messages_terminates self params node_id_cnt msgs st
-decreasing_by
-  betree_node_apply_messages_decreases self params node_id_cnt msgs st
-
-/- [betree_main::betree::Node::{5}::apply_messages] -/
-def betree_node_apply_messages_back
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) :
-  (Result (betree_node_t × betree_node_id_counter_t))
-  :=
-  match h: self with
-  | betree_node_t.Internal node =>
-    do
-      let (mkbetree_internal_t i i0 n n0) := node
-      let (st0, content) ← betree_load_internal_node_fwd i st
-      let content0 ←
-        betree_node_apply_messages_to_internal_fwd_back content msgs
-      let num_msgs ←
-        betree_list_len_fwd (UInt64 × betree_message_t) content0
-      if h: num_msgs >= params.betree_params_min_flush_size
-      then
-        do
-          let (st1, content1) ←
-            betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
-              node_id_cnt content0 st0
-          let (node0, node_id_cnt0) ←
-            betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
-              node_id_cnt content0 st0
-          let (mkbetree_internal_t i1 i2 n1 n2) := node0
-          let _ ← betree_store_internal_node_fwd i1 content1 st1
-          Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1 n2),
-            node_id_cnt0)
-      else
-        do
-          let _ ← betree_store_internal_node_fwd i content0 st0
-          Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n n0),
-            node_id_cnt)
-  | betree_node_t.Leaf node =>
-    do
-      let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st
-      let content0 ← betree_node_apply_messages_to_leaf_fwd_back content msgs
-      let len ← betree_list_len_fwd (UInt64 × UInt64) content0
-      let i ← UInt64.checked_mul (UInt64.ofNatCore 2 (by intlit))
-        params.betree_params_split_size
-      if h: len >= i
-      then
-        do
-          let (st1, new_node) ←
-            betree_leaf_split_fwd node content0 params node_id_cnt st0
-          let _ ←
-            betree_store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil
-              st1
-          let node_id_cnt0 ←
-            betree_leaf_split_back node content0 params node_id_cnt st0
-          Result.ret (betree_node_t.Internal new_node, node_id_cnt0)
-      else
-        do
-          let _ ← betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
-          Result.ret (betree_node_t.Leaf { node with betree_leaf_size := len },
-            node_id_cnt)
-termination_by betree_node_apply_messages_back self params node_id_cnt msgs st
-  =>
-  betree_node_apply_messages_terminates self params node_id_cnt msgs st
-decreasing_by
-  betree_node_apply_messages_decreases self params node_id_cnt msgs st
-
-/- [betree_main::betree::Internal::{4}::flush] -/
-def betree_internal_flush_fwd
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (UInt64 × betree_message_t)) (st : State) :
-  (Result (State × (betree_list_t (UInt64 × betree_message_t))))
-  :=
-  do
-    let (mkbetree_internal_t _ i n n0) := self
-    let p ← betree_list_partition_at_pivot_fwd betree_message_t content i
-    let (msgs_left, msgs_right) := p
-    let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left
-    if h: len_left >= params.betree_params_min_flush_size
-    then
-      do
-        let (st0, _) ←
-          betree_node_apply_messages_fwd n params node_id_cnt msgs_left st
-        let (_, node_id_cnt0) ←
-          betree_node_apply_messages_back n params node_id_cnt msgs_left st
-        let len_right ←
-          betree_list_len_fwd (UInt64 × betree_message_t) msgs_right
-        if h: len_right >= params.betree_params_min_flush_size
-        then
-          do
-            let (st1, _) ←
-              betree_node_apply_messages_fwd n0 params node_id_cnt0 msgs_right
-                st0
-            let _ ←
-              betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
-                st0
-            Result.ret (st1, betree_list_t.Nil)
-        else Result.ret (st0, msgs_right)
-    else
-      do
-        let (st0, _) ←
-          betree_node_apply_messages_fwd n0 params node_id_cnt msgs_right st
-        let _ ←
-          betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
-        Result.ret (st0, msgs_left)
-termination_by betree_internal_flush_fwd self params node_id_cnt content st =>
-  betree_internal_flush_terminates self params node_id_cnt content st
-decreasing_by
-  betree_internal_flush_decreases self params node_id_cnt content st
-
-/- [betree_main::betree::Internal::{4}::flush] -/
-def betree_internal_flush_back
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (UInt64 × betree_message_t)) (st : State) :
-  (Result (betree_internal_t × betree_node_id_counter_t))
-  :=
-  do
-    let (mkbetree_internal_t i i0 n n0) := self
-    let p ← betree_list_partition_at_pivot_fwd betree_message_t content i0
-    let (msgs_left, msgs_right) := p
-    let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left
-    if h: len_left >= params.betree_params_min_flush_size
-    then
-      do
-        let (st0, _) ←
-          betree_node_apply_messages_fwd n params node_id_cnt msgs_left st
-        let (n1, node_id_cnt0) ←
-          betree_node_apply_messages_back n params node_id_cnt msgs_left st
-        let len_right ←
-          betree_list_len_fwd (UInt64 × betree_message_t) msgs_right
-        if h: len_right >= params.betree_params_min_flush_size
-        then
-          do
-            let (n2, node_id_cnt1) ←
-              betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
-                st0
-            Result.ret (mkbetree_internal_t i i0 n1 n2, node_id_cnt1)
-        else Result.ret (mkbetree_internal_t i i0 n1 n0, node_id_cnt0)
-    else
-      do
-        let (n1, node_id_cnt0) ←
-          betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
-        Result.ret (mkbetree_internal_t i i0 n n1, node_id_cnt0)
-termination_by betree_internal_flush_back self params node_id_cnt content st =>
-  betree_internal_flush_terminates self params node_id_cnt content st
-decreasing_by
-  betree_internal_flush_decreases self params node_id_cnt content st
-
-/- [betree_main::betree::Node::{5}::apply] -/
-def betree_node_apply_fwd
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t) (key : UInt64)
-  (new_msg : betree_message_t) (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let l := betree_list_t.Nil
-    let (st0, _) ←
-      betree_node_apply_messages_fwd self params node_id_cnt
-        (betree_list_t.Cons (key, new_msg) l) st
-    let _ ←
-      betree_node_apply_messages_back self params node_id_cnt
-        (betree_list_t.Cons (key, new_msg) l) st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::Node::{5}::apply] -/
-def betree_node_apply_back
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t) (key : UInt64)
-  (new_msg : betree_message_t) (st : State) :
-  Result (betree_node_t × betree_node_id_counter_t)
-  :=
-  let l := betree_list_t.Nil
-  betree_node_apply_messages_back self params node_id_cnt (betree_list_t.Cons
-    (key, new_msg) l) st
-
-/- [betree_main::betree::BeTree::{6}::new] -/
-def betree_be_tree_new_fwd
-  (min_flush_size : UInt64) (split_size : UInt64) (st : State) :
-  Result (State × betree_be_tree_t)
-  :=
-  do
-    let node_id_cnt ← betree_node_id_counter_new_fwd
-    let id ← betree_node_id_counter_fresh_id_fwd node_id_cnt
-    let (st0, _) ← betree_store_leaf_node_fwd id betree_list_t.Nil st
-    let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt
-    Result.ret (st0,
-      {
-        betree_be_tree_params :=
-          {
-            betree_params_min_flush_size := min_flush_size,
-            betree_params_split_size := split_size
-          },
-        betree_be_tree_node_id_cnt := node_id_cnt0,
-        betree_be_tree_root :=
-          (betree_node_t.Leaf
-            {
-              betree_leaf_id := id,
-              betree_leaf_size := (UInt64.ofNatCore 0 (by intlit))
-            })
-      })
-
-/- [betree_main::betree::BeTree::{6}::apply] -/
-def betree_be_tree_apply_fwd
-  (self : betree_be_tree_t) (key : UInt64) (msg : betree_message_t)
-  (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
-        self.betree_be_tree_node_id_cnt key msg st
-    let _ ←
-      betree_node_apply_back self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::BeTree::{6}::apply] -/
-def betree_be_tree_apply_back
-  (self : betree_be_tree_t) (key : UInt64) (msg : betree_message_t)
-  (st : State) :
-  Result betree_be_tree_t
-  :=
-  do
-    let (n, nic) ←
-      betree_node_apply_back self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-    Result.ret
-      { self with betree_be_tree_node_id_cnt := nic, betree_be_tree_root := n }
-
-/- [betree_main::betree::BeTree::{6}::insert] -/
-def betree_be_tree_insert_fwd
-  (self : betree_be_tree_t) (key : UInt64) (value : UInt64) (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      betree_be_tree_apply_fwd self key (betree_message_t.Insert value) st
-    let _ ←
-      betree_be_tree_apply_back self key (betree_message_t.Insert value) st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::BeTree::{6}::insert] -/
-def betree_be_tree_insert_back
-  (self : betree_be_tree_t) (key : UInt64) (value : UInt64) (st : State) :
-  Result betree_be_tree_t
-  :=
-  betree_be_tree_apply_back self key (betree_message_t.Insert value) st
-
-/- [betree_main::betree::BeTree::{6}::delete] -/
-def betree_be_tree_delete_fwd
-  (self : betree_be_tree_t) (key : UInt64) (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      betree_be_tree_apply_fwd self key betree_message_t.Delete st
-    let _ ← betree_be_tree_apply_back self key betree_message_t.Delete st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::BeTree::{6}::delete] -/
-def betree_be_tree_delete_back
-  (self : betree_be_tree_t) (key : UInt64) (st : State) :
-  Result betree_be_tree_t
-  :=
-  betree_be_tree_apply_back self key betree_message_t.Delete st
-
-/- [betree_main::betree::BeTree::{6}::upsert] -/
-def betree_be_tree_upsert_fwd
-  (self : betree_be_tree_t) (key : UInt64) (upd : betree_upsert_fun_state_t)
-  (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      betree_be_tree_apply_fwd self key (betree_message_t.Upsert upd) st
-    let _ ←
-      betree_be_tree_apply_back self key (betree_message_t.Upsert upd) st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::BeTree::{6}::upsert] -/
-def betree_be_tree_upsert_back
-  (self : betree_be_tree_t) (key : UInt64) (upd : betree_upsert_fun_state_t)
-  (st : State) :
-  Result betree_be_tree_t
-  :=
-  betree_be_tree_apply_back self key (betree_message_t.Upsert upd) st
-
-/- [betree_main::betree::BeTree::{6}::lookup] -/
-def betree_be_tree_lookup_fwd
-  (self : betree_be_tree_t) (key : UInt64) (st : State) :
-  Result (State × (Option UInt64))
-  :=
-  betree_node_lookup_fwd self.betree_be_tree_root key st
-
-/- [betree_main::betree::BeTree::{6}::lookup] -/
-def betree_be_tree_lookup_back
-  (self : betree_be_tree_t) (key : UInt64) (st : State) :
-  Result betree_be_tree_t
-  :=
-  do
-    let n ← betree_node_lookup_back self.betree_be_tree_root key st
-    Result.ret { self with betree_be_tree_root := n }
-
-/- [betree_main::main] -/
-def main_fwd : Result Unit :=
-  Result.ret ()
-
-/- Unit test for [betree_main::main] -/
-#assert (main_fwd == .ret ())
-
diff --git a/tests/lean/betree/BetreeMain/Opaque.lean b/tests/lean/betree/BetreeMain/Opaque.lean
deleted file mode 100644
index b3db37c2..00000000
--- a/tests/lean/betree/BetreeMain/Opaque.lean
+++ /dev/null
@@ -1,33 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: opaque function definitions
-import Base.Primitives
-import BetreeMain.Types
-
-structure OpaqueDefs where
-  
-  /- [betree_main::betree_utils::load_internal_node] -/
-  betree_utils_load_internal_node_fwd
-    :
-    UInt64 -> State -> Result (State × (betree_list_t (UInt64 ×
-      betree_message_t)))
-  
-  /- [betree_main::betree_utils::store_internal_node] -/
-  betree_utils_store_internal_node_fwd
-    :
-    UInt64 -> betree_list_t (UInt64 × betree_message_t) -> State -> Result
-      (State × Unit)
-  
-  /- [betree_main::betree_utils::load_leaf_node] -/
-  betree_utils_load_leaf_node_fwd
-    : UInt64 -> State -> Result (State × (betree_list_t (UInt64 × UInt64)))
-  
-  /- [betree_main::betree_utils::store_leaf_node] -/
-  betree_utils_store_leaf_node_fwd
-    :
-    UInt64 -> betree_list_t (UInt64 × UInt64) -> State -> Result (State ×
-      Unit)
-  
-  /- [core::option::Option::{0}::unwrap] -/
-  core_option_option_unwrap_fwd
-    (T : Type) : Option T -> State -> Result (State × T)
-  
diff --git a/tests/lean/betree/BetreeMain/Types.lean b/tests/lean/betree/BetreeMain/Types.lean
deleted file mode 100644
index 32634e30..00000000
--- a/tests/lean/betree/BetreeMain/Types.lean
+++ /dev/null
@@ -1,55 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: type definitions
-import Base.Primitives
-
-/- [betree_main::betree::List] -/
-inductive betree_list_t (T : Type) :=
-| Cons : T -> betree_list_t T -> betree_list_t T
-| Nil : betree_list_t T
-
-/- [betree_main::betree::UpsertFunState] -/
-inductive betree_upsert_fun_state_t :=
-| Add : UInt64 -> betree_upsert_fun_state_t
-| Sub : UInt64 -> betree_upsert_fun_state_t
-
-/- [betree_main::betree::Message] -/
-inductive betree_message_t :=
-| Insert : UInt64 -> betree_message_t
-| Delete : betree_message_t
-| Upsert : betree_upsert_fun_state_t -> betree_message_t
-
-/- [betree_main::betree::Leaf] -/
-structure betree_leaf_t where
-  betree_leaf_id : UInt64
-  betree_leaf_size : UInt64
-
-/- [betree_main::betree::Node] -/
-mutual inductive betree_node_t :=
-| Internal : betree_internal_t -> betree_node_t
-| Leaf : betree_leaf_t -> betree_node_t
-
-/- [betree_main::betree::Internal] -/
-inductive betree_internal_t :=
-  betree_internal_id : UInt64
-  betree_internal_pivot : UInt64
-  betree_internal_left : betree_node_t
-  betree_internal_right : betree_node_t
-
-/- [betree_main::betree::Params] -/
-structure betree_params_t where
-  betree_params_min_flush_size : UInt64
-  betree_params_split_size : UInt64
-
-/- [betree_main::betree::NodeIdCounter] -/
-structure betree_node_id_counter_t where
-  betree_node_id_counter_next_node_id : UInt64
-
-/- [betree_main::betree::BeTree] -/
-structure betree_be_tree_t where
-  betree_be_tree_params : betree_params_t
-  betree_be_tree_node_id_cnt : betree_node_id_counter_t
-  betree_be_tree_root : betree_node_t
-
-/- The state type used in the state-error monad -/
-axiom State : Type
-