(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module collections.
  Module btree.
    Module fix_.
      Module Impl_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
        Definition Self (K V : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::node::NodeRef")
            []
            [
              Ty.path "alloc::collections::btree::node::marker::Mut";
              K;
              V;
              Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
            ].
        
        (*
            fn fix_node_through_parent<A: Allocator + Clone>(
                self,
                alloc: A,
            ) -> Result<Option<NodeRef<marker::Mut<'a>, K, V, marker::Internal>>, Self> {
                let len = self.len();
                if len >= MIN_LEN {
                    Ok(None)
                } else {
                    match self.choose_parent_kv() {
                        Ok(Left(mut left_parent_kv)) => {
                            if left_parent_kv.can_merge() {
                                let parent = left_parent_kv.merge_tracking_parent(alloc);
                                Ok(Some(parent))
                            } else {
                                left_parent_kv.bulk_steal_left(MIN_LEN - len);
                                Ok(None)
                            }
                        }
                        Ok(Right(mut right_parent_kv)) => {
                            if right_parent_kv.can_merge() {
                                let parent = right_parent_kv.merge_tracking_parent(alloc);
                                Ok(Some(parent))
                            } else {
                                right_parent_kv.bulk_steal_right(MIN_LEN - len);
                                Ok(None)
                            }
                        }
                        Err(root) => {
                            if len > 0 {
                                Ok(None)
                            } else {
                                Err(root)
                            }
                        }
                    }
                }
            }
        *)
        Definition fix_node_through_parent
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            Ty.path "alloc::collections::btree::node::marker::Mut";
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ],
                        "len",
                        []
                      |),
                      [ self ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.ge (|
                                M.read (| len |),
                                M.read (|
                                  M.get_constant (| "alloc::collections::btree::map::MIN_LEN" |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [ Value.StructTuple "core::option::Option::None" [] ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [
                                    Ty.path "alloc::collections::btree::node::marker::Mut";
                                    K;
                                    V;
                                    Ty.path
                                      "alloc::collections::btree::node::marker::LeafOrInternal"
                                  ],
                                "choose_parent_kv",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::result::Result::Ok",
                                    0
                                  |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "alloc::collections::btree::node::LeftOrRight::Left",
                                    0
                                  |) in
                                let left_parent_kv := M.copy (| γ1_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::node::BalancingContext")
                                                    []
                                                    [ K; V ],
                                                  "can_merge",
                                                  []
                                                |),
                                                [ left_parent_kv ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ parent :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path
                                                    "alloc::collections::btree::node::BalancingContext")
                                                  []
                                                  [ K; V ],
                                                "merge_tracking_parent",
                                                [ A ]
                                              |),
                                              [ M.read (| left_parent_kv |); M.read (| alloc |) ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::result::Result::Ok"
                                            [
                                              Value.StructTuple
                                                "core::option::Option::Some"
                                                [ M.read (| parent |) ]
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path
                                                    "alloc::collections::btree::node::BalancingContext")
                                                  []
                                                  [ K; V ],
                                                "bulk_steal_left",
                                                []
                                              |),
                                              [
                                                left_parent_kv;
                                                BinOp.Wrap.sub (|
                                                  M.read (|
                                                    M.get_constant (|
                                                      "alloc::collections::btree::map::MIN_LEN"
                                                    |)
                                                  |),
                                                  M.read (| len |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::result::Result::Ok"
                                            [ Value.StructTuple "core::option::Option::None" [] ]
                                        |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::result::Result::Ok",
                                    0
                                  |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "alloc::collections::btree::node::LeftOrRight::Right",
                                    0
                                  |) in
                                let right_parent_kv := M.copy (| γ1_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::node::BalancingContext")
                                                    []
                                                    [ K; V ],
                                                  "can_merge",
                                                  []
                                                |),
                                                [ right_parent_kv ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ parent :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path
                                                    "alloc::collections::btree::node::BalancingContext")
                                                  []
                                                  [ K; V ],
                                                "merge_tracking_parent",
                                                [ A ]
                                              |),
                                              [ M.read (| right_parent_kv |); M.read (| alloc |) ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::result::Result::Ok"
                                            [
                                              Value.StructTuple
                                                "core::option::Option::Some"
                                                [ M.read (| parent |) ]
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path
                                                    "alloc::collections::btree::node::BalancingContext")
                                                  []
                                                  [ K; V ],
                                                "bulk_steal_right",
                                                []
                                              |),
                                              [
                                                right_parent_kv;
                                                BinOp.Wrap.sub (|
                                                  M.read (|
                                                    M.get_constant (|
                                                      "alloc::collections::btree::map::MIN_LEN"
                                                    |)
                                                  |),
                                                  M.read (| len |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::result::Result::Ok"
                                            [ Value.StructTuple "core::option::Option::None" [] ]
                                        |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::result::Result::Err",
                                    0
                                  |) in
                                let root := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.gt (|
                                                M.read (| len |),
                                                Value.Integer IntegerKind.Usize 0
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::result::Result::Ok"
                                            [ Value.StructTuple "core::option::Option::None" [] ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [ M.read (| root |) ]
                                        |)))
                                  ]
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_node_through_parent :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "fix_node_through_parent" (fix_node_through_parent K V).
        (*
            pub fn fix_node_and_affected_ancestors<A: Allocator + Clone>(mut self, alloc: A) -> bool {
                loop {
                    match self.fix_node_through_parent(alloc.clone()) {
                        Ok(Some(parent)) => self = parent.forget_type(),
                        Ok(None) => return true,
                        Err(_) => return false,
                    }
                }
            }
        *)
        Definition fix_node_and_affected_ancestors
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::NodeRef")
                                    []
                                    [
                                      Ty.path "alloc::collections::btree::node::marker::Mut";
                                      K;
                                      V;
                                      Ty.path
                                        "alloc::collections::btree::node::marker::LeafOrInternal"
                                    ],
                                  "fix_node_through_parent",
                                  [ A ]
                                |),
                                [
                                  M.read (| self |);
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::clone::Clone",
                                      A,
                                      [],
                                      "clone",
                                      []
                                    |),
                                    [ alloc ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Ok",
                                      0
                                    |) in
                                  let γ1_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ0_0,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let parent := M.copy (| γ1_0 |) in
                                  M.write (|
                                    self,
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path "alloc::collections::btree::node::marker::Mut";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::Internal"
                                          ],
                                        "forget_type",
                                        []
                                      |),
                                      [ M.read (| parent |) ]
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Ok",
                                      0
                                    |) in
                                  let _ :=
                                    M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (| M.return_ (| Value.Bool true |) |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Err",
                                      0
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (| M.return_ (| Value.Bool false |) |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_node_and_affected_ancestors :
          forall (K V : Ty.t),
          M.IsAssociatedFunction
            (Self K V)
            "fix_node_and_affected_ancestors"
            (fix_node_and_affected_ancestors K V).
      End Impl_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
      
      
      Module Impl_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Owned_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
        Definition Self (K V : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::node::NodeRef")
            []
            [
              Ty.path "alloc::collections::btree::node::marker::Owned";
              K;
              V;
              Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
            ].
        
        (*
            pub fn fix_top<A: Allocator + Clone>(&mut self, alloc: A) {
                while self.height() > 0 && self.len() == 0 {
                    self.pop_internal_level(alloc.clone());
                }
            }
        *)
        Definition fix_top (K V : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    BinOp.gt (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::node::NodeRef")
                                            []
                                            [
                                              Ty.path
                                                "alloc::collections::btree::node::marker::Owned";
                                              K;
                                              V;
                                              Ty.path
                                                "alloc::collections::btree::node::marker::LeafOrInternal"
                                            ],
                                          "height",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.eq (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::btree::node::NodeRef")
                                              []
                                              [
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Owned";
                                                K;
                                                V;
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::LeafOrInternal"
                                              ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| self |) ]
                                        |),
                                        Value.Integer IntegerKind.Usize 0
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Owned";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "pop_internal_level",
                                    [ A ]
                                  |),
                                  [
                                    M.read (| self |);
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        A,
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [ alloc ]
                                    |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_top :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "fix_top" (fix_top K V).
        
        (*
            pub fn fix_right_border<A: Allocator + Clone>(&mut self, alloc: A) {
                self.fix_top(alloc.clone());
                if self.len() > 0 {
                    self.borrow_mut().last_kv().fix_right_border_of_right_edge(alloc.clone());
                    self.fix_top(alloc);
                }
            }
        *)
        Definition fix_right_border
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            Ty.path "alloc::collections::btree::node::marker::Owned";
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ],
                        "fix_top",
                        [ A ]
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                          [ alloc ]
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Owned";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::Handle")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ];
                                    Ty.path "alloc::collections::btree::node::marker::KV"
                                  ],
                                "fix_right_border_of_right_edge",
                                [ A ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "last_kv",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path
                                              "alloc::collections::btree::node::marker::Owned";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                          ],
                                        "borrow_mut",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  ]
                                |);
                                M.call_closure (|
                                  M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                                  [ alloc ]
                                |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [
                                    Ty.path "alloc::collections::btree::node::marker::Owned";
                                    K;
                                    V;
                                    Ty.path
                                      "alloc::collections::btree::node::marker::LeafOrInternal"
                                  ],
                                "fix_top",
                                [ A ]
                              |),
                              [ M.read (| self |); M.read (| alloc |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_right_border :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "fix_right_border" (fix_right_border K V).
        
        (*
            pub fn fix_left_border<A: Allocator + Clone>(&mut self, alloc: A) {
                self.fix_top(alloc.clone());
                if self.len() > 0 {
                    self.borrow_mut().first_kv().fix_left_border_of_left_edge(alloc.clone());
                    self.fix_top(alloc);
                }
            }
        *)
        Definition fix_left_border
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            Ty.path "alloc::collections::btree::node::marker::Owned";
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ],
                        "fix_top",
                        [ A ]
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                          [ alloc ]
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Owned";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::Handle")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ];
                                    Ty.path "alloc::collections::btree::node::marker::KV"
                                  ],
                                "fix_left_border_of_left_edge",
                                [ A ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "first_kv",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path
                                              "alloc::collections::btree::node::marker::Owned";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                          ],
                                        "borrow_mut",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  ]
                                |);
                                M.call_closure (|
                                  M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                                  [ alloc ]
                                |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [
                                    Ty.path "alloc::collections::btree::node::marker::Owned";
                                    K;
                                    V;
                                    Ty.path
                                      "alloc::collections::btree::node::marker::LeafOrInternal"
                                  ],
                                "fix_top",
                                [ A ]
                              |),
                              [ M.read (| self |); M.read (| alloc |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_left_border :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "fix_left_border" (fix_left_border K V).
        
        (*
            pub fn fix_right_border_of_plentiful(&mut self) {
                let mut cur_node = self.borrow_mut();
                while let Internal(internal) = cur_node.force() {
                    // Check if right-most child is underfull.
                    let mut last_kv = internal.last_kv().consider_for_balancing();
                    debug_assert!(last_kv.left_child_len() >= MIN_LEN * 2);
                    let right_child_len = last_kv.right_child_len();
                    if right_child_len < MIN_LEN {
                        // We need to steal.
                        last_kv.bulk_steal_left(MIN_LEN - right_child_len);
                    }
        
                    // Go further down.
                    cur_node = last_kv.into_right_child();
                }
            }
        *)
        Definition fix_right_border_of_plentiful
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ cur_node :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            Ty.path "alloc::collections::btree::node::marker::Owned";
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ],
                        "borrow_mut",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "force",
                                    []
                                  |),
                                  [ M.read (| cur_node |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "alloc::collections::btree::node::ForceResult::Internal",
                                0
                              |) in
                            let internal := M.copy (| γ0_0 |) in
                            let~ last_kv :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::Handle")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path "alloc::collections::btree::node::marker::Mut";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::Internal"
                                          ];
                                        Ty.path "alloc::collections::btree::node::marker::KV"
                                      ],
                                    "consider_for_balancing",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path "alloc::collections::btree::node::marker::Mut";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::Internal"
                                          ],
                                        "last_kv",
                                        []
                                      |),
                                      [ M.read (| internal |) ]
                                    |)
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      UnOp.not (|
                                                        BinOp.ge (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloc::collections::btree::node::BalancingContext")
                                                                []
                                                                [ K; V ],
                                                              "left_child_len",
                                                              []
                                                            |),
                                                            [ last_kv ]
                                                          |),
                                                          BinOp.Wrap.mul (|
                                                            M.read (|
                                                              M.get_constant (|
                                                                "alloc::collections::btree::map::MIN_LEN"
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.Usize 2
                                                          |)
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::panicking::panic",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          Value.String
                                                            "assertion failed: last_kv.left_child_len() >= MIN_LEN * 2"
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ right_child_len :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::BalancingContext")
                                      []
                                      [ K; V ],
                                    "right_child_len",
                                    []
                                  |),
                                  [ last_kv ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.lt (|
                                              M.read (| right_child_len |),
                                              M.read (|
                                                M.get_constant (|
                                                  "alloc::collections::btree::map::MIN_LEN"
                                                |)
                                              |)
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path
                                                  "alloc::collections::btree::node::BalancingContext")
                                                []
                                                [ K; V ],
                                              "bulk_steal_left",
                                              []
                                            |),
                                            [
                                              last_kv;
                                              BinOp.Wrap.sub (|
                                                M.read (|
                                                  M.get_constant (|
                                                    "alloc::collections::btree::map::MIN_LEN"
                                                  |)
                                                |),
                                                M.read (| right_child_len |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              M.write (|
                                cur_node,
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::BalancingContext")
                                      []
                                      [ K; V ],
                                    "into_right_child",
                                    []
                                  |),
                                  [ M.read (| last_kv |) ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_right_border_of_plentiful :
          forall (K V : Ty.t),
          M.IsAssociatedFunction
            (Self K V)
            "fix_right_border_of_plentiful"
            (fix_right_border_of_plentiful K V).
      End Impl_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Owned_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
      
      Module Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_LeafOrInternal_alloc_collections_btree_node_marker_KV.
        Definition Self (K V : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::node::Handle")
            []
            [
              Ty.apply
                (Ty.path "alloc::collections::btree::node::NodeRef")
                []
                [
                  Ty.path "alloc::collections::btree::node::marker::Mut";
                  K;
                  V;
                  Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                ];
              Ty.path "alloc::collections::btree::node::marker::KV"
            ].
        
        (*
            fn fix_left_border_of_left_edge<A: Allocator + Clone>(mut self, alloc: A) {
                while let Internal(internal_kv) = self.force() {
                    self = internal_kv.fix_left_child(alloc.clone()).first_kv();
                    debug_assert!(self.reborrow().into_node().len() > MIN_LEN);
                }
            }
        *)
        Definition fix_left_border_of_left_edge
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::Handle")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path "alloc::collections::btree::node::marker::Mut";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                          ];
                                        Ty.path "alloc::collections::btree::node::marker::KV"
                                      ],
                                    "force",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "alloc::collections::btree::node::ForceResult::Internal",
                                0
                              |) in
                            let internal_kv := M.copy (| γ0_0 |) in
                            let~ _ :=
                              M.write (|
                                self,
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "first_kv",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::Handle")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "alloc::collections::btree::node::NodeRef")
                                              []
                                              [
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Mut";
                                                K;
                                                V;
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Internal"
                                              ];
                                            Ty.path "alloc::collections::btree::node::marker::KV"
                                          ],
                                        "fix_left_child",
                                        [ A ]
                                      |),
                                      [
                                        M.read (| internal_kv |);
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::clone::Clone",
                                            A,
                                            [],
                                            "clone",
                                            []
                                          |),
                                          [ alloc ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      UnOp.not (|
                                                        BinOp.gt (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloc::collections::btree::node::NodeRef")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "alloc::collections::btree::node::marker::Immut";
                                                                  K;
                                                                  V;
                                                                  Ty.path
                                                                    "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                ],
                                                              "len",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "alloc::collections::btree::node::Handle")
                                                                      []
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::collections::btree::node::NodeRef")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::Immut";
                                                                            K;
                                                                            V;
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                          ];
                                                                        Ty.path
                                                                          "alloc::collections::btree::node::marker::KV"
                                                                      ],
                                                                    "into_node",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::collections::btree::node::Handle")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "alloc::collections::btree::node::NodeRef")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "alloc::collections::btree::node::marker::Mut";
                                                                                K;
                                                                                V;
                                                                                Ty.path
                                                                                  "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                              ];
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::KV"
                                                                          ],
                                                                        "reborrow",
                                                                        []
                                                                      |),
                                                                      [ self ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            ]
                                                          |),
                                                          M.read (|
                                                            M.get_constant (|
                                                              "alloc::collections::btree::map::MIN_LEN"
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::panicking::panic",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          Value.String
                                                            "assertion failed: self.reborrow().into_node().len() > MIN_LEN"
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_left_border_of_left_edge :
          forall (K V : Ty.t),
          M.IsAssociatedFunction
            (Self K V)
            "fix_left_border_of_left_edge"
            (fix_left_border_of_left_edge K V).
        
        (*
            fn fix_right_border_of_right_edge<A: Allocator + Clone>(mut self, alloc: A) {
                while let Internal(internal_kv) = self.force() {
                    self = internal_kv.fix_right_child(alloc.clone()).last_kv();
                    debug_assert!(self.reborrow().into_node().len() > MIN_LEN);
                }
            }
        *)
        Definition fix_right_border_of_right_edge
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::Handle")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::NodeRef")
                                          []
                                          [
                                            Ty.path "alloc::collections::btree::node::marker::Mut";
                                            K;
                                            V;
                                            Ty.path
                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                          ];
                                        Ty.path "alloc::collections::btree::node::marker::KV"
                                      ],
                                    "force",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "alloc::collections::btree::node::ForceResult::Internal",
                                0
                              |) in
                            let internal_kv := M.copy (| γ0_0 |) in
                            let~ _ :=
                              M.write (|
                                self,
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::node::NodeRef")
                                      []
                                      [
                                        Ty.path "alloc::collections::btree::node::marker::Mut";
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ],
                                    "last_kv",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::node::Handle")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "alloc::collections::btree::node::NodeRef")
                                              []
                                              [
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Mut";
                                                K;
                                                V;
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Internal"
                                              ];
                                            Ty.path "alloc::collections::btree::node::marker::KV"
                                          ],
                                        "fix_right_child",
                                        [ A ]
                                      |),
                                      [
                                        M.read (| internal_kv |);
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::clone::Clone",
                                            A,
                                            [],
                                            "clone",
                                            []
                                          |),
                                          [ alloc ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      UnOp.not (|
                                                        BinOp.gt (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloc::collections::btree::node::NodeRef")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "alloc::collections::btree::node::marker::Immut";
                                                                  K;
                                                                  V;
                                                                  Ty.path
                                                                    "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                ],
                                                              "len",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "alloc::collections::btree::node::Handle")
                                                                      []
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::collections::btree::node::NodeRef")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::Immut";
                                                                            K;
                                                                            V;
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                          ];
                                                                        Ty.path
                                                                          "alloc::collections::btree::node::marker::KV"
                                                                      ],
                                                                    "into_node",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::collections::btree::node::Handle")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "alloc::collections::btree::node::NodeRef")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "alloc::collections::btree::node::marker::Mut";
                                                                                K;
                                                                                V;
                                                                                Ty.path
                                                                                  "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                              ];
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::KV"
                                                                          ],
                                                                        "reborrow",
                                                                        []
                                                                      |),
                                                                      [ self ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            ]
                                                          |),
                                                          M.read (|
                                                            M.get_constant (|
                                                              "alloc::collections::btree::map::MIN_LEN"
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::panicking::panic",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          Value.String
                                                            "assertion failed: self.reborrow().into_node().len() > MIN_LEN"
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_right_border_of_right_edge :
          forall (K V : Ty.t),
          M.IsAssociatedFunction
            (Self K V)
            "fix_right_border_of_right_edge"
            (fix_right_border_of_right_edge K V).
      End Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_LeafOrInternal_alloc_collections_btree_node_marker_KV.
      
      Module Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_Internal_alloc_collections_btree_node_marker_KV.
        Definition Self (K V : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::node::Handle")
            []
            [
              Ty.apply
                (Ty.path "alloc::collections::btree::node::NodeRef")
                []
                [
                  Ty.path "alloc::collections::btree::node::marker::Mut";
                  K;
                  V;
                  Ty.path "alloc::collections::btree::node::marker::Internal"
                ];
              Ty.path "alloc::collections::btree::node::marker::KV"
            ].
        
        (*
            fn fix_left_child<A: Allocator + Clone>(
                self,
                alloc: A,
            ) -> NodeRef<marker::Mut<'a>, K, V, marker::LeafOrInternal> {
                let mut internal_kv = self.consider_for_balancing();
                let left_len = internal_kv.left_child_len();
                debug_assert!(internal_kv.right_child_len() >= MIN_LEN);
                if internal_kv.can_merge() {
                    internal_kv.merge_tracking_child(alloc)
                } else {
                    // `MIN_LEN + 1` to avoid readjust if merge happens on the next level.
                    let count = (MIN_LEN + 1).saturating_sub(left_len);
                    if count > 0 {
                        internal_kv.bulk_steal_right(count);
                    }
                    internal_kv.into_left_child()
                }
            }
        *)
        Definition fix_left_child
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ internal_kv :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::Handle")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::collections::btree::node::NodeRef")
                              []
                              [
                                Ty.path "alloc::collections::btree::node::marker::Mut";
                                K;
                                V;
                                Ty.path "alloc::collections::btree::node::marker::Internal"
                              ];
                            Ty.path "alloc::collections::btree::node::marker::KV"
                          ],
                        "consider_for_balancing",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ left_len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::BalancingContext")
                          []
                          [ K; V ],
                        "left_child_len",
                        []
                      |),
                      [ internal_kv ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            BinOp.ge (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::node::BalancingContext")
                                                    []
                                                    [ K; V ],
                                                  "right_child_len",
                                                  []
                                                |),
                                                [ internal_kv ]
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "alloc::collections::btree::map::MIN_LEN"
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "assertion failed: internal_kv.right_child_len() >= MIN_LEN"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::BalancingContext")
                                    []
                                    [ K; V ],
                                  "can_merge",
                                  []
                                |),
                                [ internal_kv ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::BalancingContext")
                                []
                                [ K; V ],
                              "merge_tracking_child",
                              [ A ]
                            |),
                            [ M.read (| internal_kv |); M.read (| alloc |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ count :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "saturating_sub", [] |),
                              [
                                BinOp.Wrap.add (|
                                  M.read (|
                                    M.get_constant (| "alloc::collections::btree::map::MIN_LEN" |)
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |);
                                M.read (| left_len |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| count |),
                                          Value.Integer IntegerKind.Usize 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path
                                              "alloc::collections::btree::node::BalancingContext")
                                            []
                                            [ K; V ],
                                          "bulk_steal_right",
                                          []
                                        |),
                                        [ internal_kv; M.read (| count |) ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::BalancingContext")
                                []
                                [ K; V ],
                              "into_left_child",
                              []
                            |),
                            [ M.read (| internal_kv |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_left_child :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "fix_left_child" (fix_left_child K V).
        
        (*
            fn fix_right_child<A: Allocator + Clone>(
                self,
                alloc: A,
            ) -> NodeRef<marker::Mut<'a>, K, V, marker::LeafOrInternal> {
                let mut internal_kv = self.consider_for_balancing();
                let right_len = internal_kv.right_child_len();
                debug_assert!(internal_kv.left_child_len() >= MIN_LEN);
                if internal_kv.can_merge() {
                    internal_kv.merge_tracking_child(alloc)
                } else {
                    // `MIN_LEN + 1` to avoid readjust if merge happens on the next level.
                    let count = (MIN_LEN + 1).saturating_sub(right_len);
                    if count > 0 {
                        internal_kv.bulk_steal_left(count);
                    }
                    internal_kv.into_right_child()
                }
            }
        *)
        Definition fix_right_child
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ A ], [ self; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ internal_kv :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::Handle")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::collections::btree::node::NodeRef")
                              []
                              [
                                Ty.path "alloc::collections::btree::node::marker::Mut";
                                K;
                                V;
                                Ty.path "alloc::collections::btree::node::marker::Internal"
                              ];
                            Ty.path "alloc::collections::btree::node::marker::KV"
                          ],
                        "consider_for_balancing",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ right_len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::BalancingContext")
                          []
                          [ K; V ],
                        "right_child_len",
                        []
                      |),
                      [ internal_kv ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            BinOp.ge (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::node::BalancingContext")
                                                    []
                                                    [ K; V ],
                                                  "left_child_len",
                                                  []
                                                |),
                                                [ internal_kv ]
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "alloc::collections::btree::map::MIN_LEN"
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "assertion failed: internal_kv.left_child_len() >= MIN_LEN"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::BalancingContext")
                                    []
                                    [ K; V ],
                                  "can_merge",
                                  []
                                |),
                                [ internal_kv ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::BalancingContext")
                                []
                                [ K; V ],
                              "merge_tracking_child",
                              [ A ]
                            |),
                            [ M.read (| internal_kv |); M.read (| alloc |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ count :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "saturating_sub", [] |),
                              [
                                BinOp.Wrap.add (|
                                  M.read (|
                                    M.get_constant (| "alloc::collections::btree::map::MIN_LEN" |)
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |);
                                M.read (| right_len |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| count |),
                                          Value.Integer IntegerKind.Usize 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path
                                              "alloc::collections::btree::node::BalancingContext")
                                            []
                                            [ K; V ],
                                          "bulk_steal_left",
                                          []
                                        |),
                                        [ internal_kv; M.read (| count |) ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::BalancingContext")
                                []
                                [ K; V ],
                              "into_right_child",
                              []
                            |),
                            [ M.read (| internal_kv |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_fix_right_child :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "fix_right_child" (fix_right_child K V).
      End Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_Internal_alloc_collections_btree_node_marker_KV.
    End fix_.
  End btree.
End collections.
