-- 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)