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

Module collections.
  Module btree.
    Module append.
      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 append_from_sorted_iters<I, A: Allocator + Clone>(
                &mut self,
                left: I,
                right: I,
                length: &mut usize,
                alloc: A,
            ) where
                K: Ord,
                I: Iterator<Item = (K, V)> + FusedIterator,
            {
                // We prepare to merge `left` and `right` into a sorted sequence in linear time.
                let iter = MergeIter(MergeIterInner::new(left, right));
        
                // Meanwhile, we build a tree from the sorted sequence in linear time.
                self.bulk_push(iter, length, alloc)
            }
        *)
        Definition append_from_sorted_iters
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ _ as I; A ], [ self; _ as left; _ as right; length; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let left := M.alloc (| left |) in
              let right := M.alloc (| right |) in
              let length := M.alloc (| length |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ iter :=
                  M.alloc (|
                    Value.StructTuple
                      "alloc::collections::btree::append::MergeIter"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::merge_iter::MergeIterInner")
                              []
                              [ I ],
                            "new",
                            []
                          |),
                          [ M.read (| left |); M.read (| right |) ]
                        |)
                      ]
                  |) in
                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"
                        ],
                      "bulk_push",
                      [
                        Ty.apply
                          (Ty.path "alloc::collections::btree::append::MergeIter")
                          []
                          [ K; V; I ];
                        A
                      ]
                    |),
                    [ M.read (| self |); M.read (| iter |); M.read (| length |); M.read (| alloc |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_append_from_sorted_iters :
          forall (K V : Ty.t),
          M.IsAssociatedFunction
            (Self K V)
            "append_from_sorted_iters"
            (append_from_sorted_iters K V).
        
        (*
            pub fn bulk_push<I, A: Allocator + Clone>(&mut self, iter: I, length: &mut usize, alloc: A)
            where
                I: Iterator<Item = (K, V)>,
            {
                let mut cur_node = self.borrow_mut().last_leaf_edge().into_node();
                // Iterate through all key-value pairs, pushing them into nodes at the right level.
                for (key, value) in iter {
                    // Try to push key-value pair into the current leaf node.
                    if cur_node.len() < node::CAPACITY {
                        cur_node.push(key, value);
                    } else {
                        // No space left, go up and push there.
                        let mut open_node;
                        let mut test_node = cur_node.forget_type();
                        loop {
                            match test_node.ascend() {
                                Ok(parent) => {
                                    let parent = parent.into_node();
                                    if parent.len() < node::CAPACITY {
                                        // Found a node with space left, push here.
                                        open_node = parent;
                                        break;
                                    } else {
                                        // Go up again.
                                        test_node = parent.forget_type();
                                    }
                                }
                                Err(_) => {
                                    // We are at the top, create a new root node and push there.
                                    open_node = self.push_internal_level(alloc.clone());
                                    break;
                                }
                            }
                        }
        
                        // Push key-value pair and new right subtree.
                        let tree_height = open_node.height() - 1;
                        let mut right_tree = Root::new(alloc.clone());
                        for _ in 0..tree_height {
                            right_tree.push_internal_level(alloc.clone());
                        }
                        open_node.push(key, value, right_tree);
        
                        // Go down to the right-most leaf again.
                        cur_node = open_node.forget_type().last_leaf_edge().into_node();
                    }
        
                    // Increment length every iteration, to make sure the map drops
                    // the appended elements even if advancing the iterator panicks.
                    *length += 1;
                }
                self.fix_right_border_of_plentiful();
            }
        *)
        Definition bulk_push
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ _ as I; A ], [ self; iter; length; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let iter := M.alloc (| iter |) in
              let length := M.alloc (| length |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ cur_node :=
                  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::Leaf"
                              ];
                            Ty.path "alloc::collections::btree::node::marker::Edge"
                          ],
                        "into_node",
                        []
                      |),
                      [
                        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_leaf_edge",
                            []
                          |),
                          [
                            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
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            I,
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| iter |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          I,
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let key := M.copy (| γ1_0 |) in
                                          let value := M.copy (| γ1_1 |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.lt (|
                                                            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::Leaf"
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ cur_node ]
                                                            |),
                                                            M.read (|
                                                              M.get_constant (|
                                                                "alloc::collections::btree::node::CAPACITY"
                                                              |)
                                                            |)
                                                          |)
                                                        |)) 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::Mut";
                                                                K;
                                                                V;
                                                                Ty.path
                                                                  "alloc::collections::btree::node::marker::Leaf"
                                                              ],
                                                            "push",
                                                            []
                                                          |),
                                                          [
                                                            cur_node;
                                                            M.read (| key |);
                                                            M.read (| value |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let~ open_node :=
                                                      M.copy (| Value.DeclaredButUndefined |) in
                                                    let~ test_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::Mut";
                                                                K;
                                                                V;
                                                                Ty.path
                                                                  "alloc::collections::btree::node::marker::Leaf"
                                                              ],
                                                            "forget_type",
                                                            []
                                                          |),
                                                          [ M.read (| cur_node |) ]
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      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"
                                                                    ],
                                                                  "ascend",
                                                                  []
                                                                |),
                                                                [ M.read (| test_node |) ]
                                                              |)
                                                            |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ0_0 :=
                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                      γ,
                                                                      "core::result::Result::Ok",
                                                                      0
                                                                    |) in
                                                                  let parent := M.copy (| γ0_0 |) in
                                                                  let~ parent :=
                                                                    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::Edge"
                                                                            ],
                                                                          "into_node",
                                                                          []
                                                                        |),
                                                                        [ M.read (| parent |) ]
                                                                      |)
                                                                    |) in
                                                                  M.match_operator (|
                                                                    M.alloc (| Value.Tuple [] |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ :=
                                                                            M.use
                                                                              (M.alloc (|
                                                                                BinOp.lt (|
                                                                                  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"
                                                                                        ],
                                                                                      "len",
                                                                                      []
                                                                                    |),
                                                                                    [ parent ]
                                                                                  |),
                                                                                  M.read (|
                                                                                    M.get_constant (|
                                                                                      "alloc::collections::btree::node::CAPACITY"
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)) in
                                                                          let _ :=
                                                                            M.is_constant_or_break_match (|
                                                                              M.read (| γ |),
                                                                              Value.Bool true
                                                                            |) in
                                                                          M.alloc (|
                                                                            M.never_to_any (|
                                                                              M.read (|
                                                                                let~ _ :=
                                                                                  M.write (|
                                                                                    open_node,
                                                                                    M.read (|
                                                                                      parent
                                                                                    |)
                                                                                  |) in
                                                                                M.break (||)
                                                                              |)
                                                                            |)
                                                                          |)));
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let~ _ :=
                                                                            M.write (|
                                                                              test_node,
                                                                              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
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |) in
                                                                          M.alloc (|
                                                                            Value.Tuple []
                                                                          |)))
                                                                    ]
                                                                  |)));
                                                              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 (|
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            open_node,
                                                                            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"
                                                                                  ],
                                                                                "push_internal_level",
                                                                                [ A ]
                                                                              |),
                                                                              [
                                                                                M.read (| self |);
                                                                                M.call_closure (|
                                                                                  M.get_trait_method (|
                                                                                    "core::clone::Clone",
                                                                                    A,
                                                                                    [],
                                                                                    "clone",
                                                                                    []
                                                                                  |),
                                                                                  [ alloc ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        M.break (||)
                                                                      |)
                                                                    |)
                                                                  |)))
                                                            ]
                                                          |)))
                                                      |) in
                                                    let~ tree_height :=
                                                      M.alloc (|
                                                        BinOp.Wrap.sub (|
                                                          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"
                                                                ],
                                                              "height",
                                                              []
                                                            |),
                                                            [ open_node ]
                                                          |),
                                                          Value.Integer IntegerKind.Usize 1
                                                        |)
                                                      |) in
                                                    let~ right_tree :=
                                                      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"
                                                              ],
                                                            "new",
                                                            [ A ]
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::clone::Clone",
                                                                A,
                                                                [],
                                                                "clone",
                                                                []
                                                              |),
                                                              [ alloc ]
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.use
                                                        (M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::iter::traits::collect::IntoIterator",
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "core::ops::range::Range")
                                                                  []
                                                                  [ Ty.path "usize" ],
                                                                [],
                                                                "into_iter",
                                                                []
                                                              |),
                                                              [
                                                                Value.StructRecord
                                                                  "core::ops::range::Range"
                                                                  [
                                                                    ("start",
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        0);
                                                                    ("end_",
                                                                      M.read (| tree_height |))
                                                                  ]
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let iter := M.copy (| γ |) in
                                                                M.loop (|
                                                                  ltac:(M.monadic
                                                                    (let~ _ :=
                                                                      M.match_operator (|
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::iter::traits::iterator::Iterator",
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::ops::range::Range")
                                                                                []
                                                                                [ Ty.path "usize" ],
                                                                              [],
                                                                              "next",
                                                                              []
                                                                            |),
                                                                            [ iter ]
                                                                          |)
                                                                        |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let _ :=
                                                                                M.is_struct_tuple (|
                                                                                  γ,
                                                                                  "core::option::Option::None"
                                                                                |) in
                                                                              M.alloc (|
                                                                                M.never_to_any (|
                                                                                  M.read (|
                                                                                    M.break (||)
                                                                                  |)
                                                                                |)
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ0_0 :=
                                                                                M.SubPointer.get_struct_tuple_field (|
                                                                                  γ,
                                                                                  "core::option::Option::Some",
                                                                                  0
                                                                                |) 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"
                                                                                        ],
                                                                                      "push_internal_level",
                                                                                      [ A ]
                                                                                    |),
                                                                                    [
                                                                                      right_tree;
                                                                                      M.call_closure (|
                                                                                        M.get_trait_method (|
                                                                                          "core::clone::Clone",
                                                                                          A,
                                                                                          [],
                                                                                          "clone",
                                                                                          []
                                                                                        |),
                                                                                        [ alloc ]
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                |) in
                                                                              M.alloc (|
                                                                                Value.Tuple []
                                                                              |)))
                                                                        ]
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                                |)))
                                                          ]
                                                        |)) 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::Mut";
                                                                K;
                                                                V;
                                                                Ty.path
                                                                  "alloc::collections::btree::node::marker::Internal"
                                                              ],
                                                            "push",
                                                            []
                                                          |),
                                                          [
                                                            open_node;
                                                            M.read (| key |);
                                                            M.read (| value |);
                                                            M.read (| right_tree |)
                                                          ]
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        cur_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::Leaf"
                                                                  ];
                                                                Ty.path
                                                                  "alloc::collections::btree::node::marker::Edge"
                                                              ],
                                                            "into_node",
                                                            []
                                                          |),
                                                          [
                                                            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_leaf_edge",
                                                                []
                                                              |),
                                                              [
                                                                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 (| open_node |) ]
                                                                |)
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          let~ _ :=
                                            let β := M.read (| length |) in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.add (|
                                                M.read (| β |),
                                                Value.Integer IntegerKind.Usize 1
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) 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_right_border_of_plentiful",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_bulk_push :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "bulk_push" (bulk_push K V).
      End Impl_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Owned_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
      
      (* StructTuple
        {
          name := "MergeIter";
          const_params := [];
          ty_params := [ "K"; "V"; "I" ];
          fields :=
            [ Ty.apply (Ty.path "alloc::collections::btree::merge_iter::MergeIterInner") [] [ I ] ];
        } *)
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_cmp_Ord_K_where_core_iter_traits_iterator_Iterator_I_where_core_iter_traits_marker_FusedIterator_I_for_alloc_collections_btree_append_MergeIter_K_V_I.
        Definition Self (K V I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::btree::append::MergeIter") [] [ K; V; I ].
        
        (*     type Item = (K, V); *)
        Definition _Item (K V I : Ty.t) : Ty.t := Ty.tuple [ K; V ].
        
        (*
            fn next(&mut self) -> Option<(K, V)> {
                let (a_next, b_next) = self.0.nexts(|a: &(K, V), b: &(K, V)| K::cmp(&a.0, &b.0));
                b_next.or(a_next)
            }
        *)
        Definition next (K V I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self K V I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::merge_iter::MergeIterInner")
                          []
                          [ I ],
                        "nexts",
                        [
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply (Ty.path "&") [] [ Ty.tuple [ K; V ] ];
                                  Ty.apply (Ty.path "&") [] [ Ty.tuple [ K; V ] ]
                                ]
                            ]
                            (Ty.path "core::cmp::Ordering")
                        ]
                      |),
                      [
                        M.SubPointer.get_struct_tuple_field (|
                          M.read (| self |),
                          "alloc::collections::btree::append::MergeIter",
                          0
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0; α1 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let a := M.copy (| γ |) in
                                          M.match_operator (|
                                            M.alloc (| α1 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let b := M.copy (| γ |) in
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::cmp::Ord",
                                                      K,
                                                      [],
                                                      "cmp",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_tuple_field (|
                                                        M.read (| a |),
                                                        0
                                                      |);
                                                      M.SubPointer.get_tuple_field (|
                                                        M.read (| b |),
                                                        0
                                                      |)
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let a_next := M.copy (| γ0_0 |) in
                        let b_next := M.copy (| γ0_1 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.tuple [ K; V ] ],
                              "or",
                              []
                            |),
                            [ M.read (| b_next |); M.read (| a_next |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (K V I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self K V I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("Item", InstanceField.Ty (_Item K V I)); ("next", InstanceField.Method (next K V I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_cmp_Ord_K_where_core_iter_traits_iterator_Iterator_I_where_core_iter_traits_marker_FusedIterator_I_for_alloc_collections_btree_append_MergeIter_K_V_I.
    End append.
  End btree.
End collections.
