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

Module collections.
  Module btree.
    Module split.
      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 calc_split_length(
                total_num: usize,
                root_a: &Root<K, V>,
                root_b: &Root<K, V>,
            ) -> (usize, usize) {
                let (length_a, length_b);
                if root_a.height() < root_b.height() {
                    length_a = root_a.reborrow().calc_length();
                    length_b = total_num - length_a;
                    debug_assert_eq!(length_b, root_b.reborrow().calc_length());
                } else {
                    length_b = root_b.reborrow().calc_length();
                    length_a = total_num - length_b;
                    debug_assert_eq!(length_a, root_a.reborrow().calc_length());
                }
                (length_a, length_b)
            }
        *)
        Definition calc_split_length
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [], [ total_num; root_a; root_b ] =>
            ltac:(M.monadic
              (let total_num := M.alloc (| total_num |) in
              let root_a := M.alloc (| root_a |) in
              let root_b := M.alloc (| root_b |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    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 length_a := M.copy (| γ0_0 |) in
                        let length_b := M.copy (| γ0_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::Owned";
                                                  K;
                                                  V;
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::LeafOrInternal"
                                                ],
                                              "height",
                                              []
                                            |),
                                            [ M.read (| root_a |) ]
                                          |),
                                          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 (| root_b |) ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      length_a,
                                      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"
                                            ],
                                          "calc_length",
                                          []
                                        |),
                                        [
                                          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"
                                                ],
                                              "reborrow",
                                              []
                                            |),
                                            [ M.read (| root_a |) ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      length_b,
                                      BinOp.Wrap.sub (|
                                        M.read (| total_num |),
                                        M.read (| length_a |)
                                      |)
                                    |) 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
                                                    [
                                                      length_b;
                                                      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::Immut";
                                                                K;
                                                                V;
                                                                Ty.path
                                                                  "alloc::collections::btree::node::marker::LeafOrInternal"
                                                              ],
                                                            "calc_length",
                                                            []
                                                          |),
                                                          [
                                                            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"
                                                                  ],
                                                                "reborrow",
                                                                []
                                                              |),
                                                              [ M.read (| root_b |) ]
                                                            |)
                                                          ]
                                                        |)
                                                      |)
                                                    ]
                                                |),
                                                [
                                                  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 left_val := M.copy (| γ0_0 |) in
                                                      let right_val := M.copy (| γ0_1 |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    UnOp.not (|
                                                                      BinOp.eq (|
                                                                        M.read (|
                                                                          M.read (| left_val |)
                                                                        |),
                                                                        M.read (|
                                                                          M.read (| right_val |)
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    let~ kind :=
                                                                      M.alloc (|
                                                                        Value.StructTuple
                                                                          "core::panicking::AssertKind::Eq"
                                                                          []
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "core::panicking::assert_failed",
                                                                          [
                                                                            Ty.path "usize";
                                                                            Ty.path "usize"
                                                                          ]
                                                                        |),
                                                                        [
                                                                          M.read (| kind |);
                                                                          M.read (| left_val |);
                                                                          M.read (| right_val |);
                                                                          Value.StructTuple
                                                                            "core::option::Option::None"
                                                                            []
                                                                        ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          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
                                  (let~ _ :=
                                    M.write (|
                                      length_b,
                                      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"
                                            ],
                                          "calc_length",
                                          []
                                        |),
                                        [
                                          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"
                                                ],
                                              "reborrow",
                                              []
                                            |),
                                            [ M.read (| root_b |) ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      length_a,
                                      BinOp.Wrap.sub (|
                                        M.read (| total_num |),
                                        M.read (| length_b |)
                                      |)
                                    |) 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
                                                    [
                                                      length_a;
                                                      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::Immut";
                                                                K;
                                                                V;
                                                                Ty.path
                                                                  "alloc::collections::btree::node::marker::LeafOrInternal"
                                                              ],
                                                            "calc_length",
                                                            []
                                                          |),
                                                          [
                                                            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"
                                                                  ],
                                                                "reborrow",
                                                                []
                                                              |),
                                                              [ M.read (| root_a |) ]
                                                            |)
                                                          ]
                                                        |)
                                                      |)
                                                    ]
                                                |),
                                                [
                                                  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 left_val := M.copy (| γ0_0 |) in
                                                      let right_val := M.copy (| γ0_1 |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    UnOp.not (|
                                                                      BinOp.eq (|
                                                                        M.read (|
                                                                          M.read (| left_val |)
                                                                        |),
                                                                        M.read (|
                                                                          M.read (| right_val |)
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    let~ kind :=
                                                                      M.alloc (|
                                                                        Value.StructTuple
                                                                          "core::panicking::AssertKind::Eq"
                                                                          []
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "core::panicking::assert_failed",
                                                                          [
                                                                            Ty.path "usize";
                                                                            Ty.path "usize"
                                                                          ]
                                                                        |),
                                                                        [
                                                                          M.read (| kind |);
                                                                          M.read (| left_val |);
                                                                          M.read (| right_val |);
                                                                          Value.StructTuple
                                                                            "core::option::Option::None"
                                                                            []
                                                                        ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          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 [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [ M.read (| length_a |); M.read (| length_b |) ] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_calc_split_length :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "calc_split_length" (calc_split_length K V).
        
        (*
            pub fn split_off<Q: ?Sized + Ord, A: Allocator + Clone>(&mut self, key: &Q, alloc: A) -> Self
            where
                K: Borrow<Q>,
            {
                let left_root = self;
                let mut right_root = Root::new_pillar(left_root.height(), alloc.clone());
                let mut left_node = left_root.borrow_mut();
                let mut right_node = right_root.borrow_mut();
        
                loop {
                    let mut split_edge = match left_node.search_node(key) {
                        // key is going to the right tree
                        Found(kv) => kv.left_edge(),
                        GoDown(edge) => edge,
                    };
        
                    split_edge.move_suffix(&mut right_node);
        
                    match (split_edge.force(), right_node.force()) {
                        (Internal(edge), Internal(node)) => {
                            left_node = edge.descend();
                            right_node = node.first_edge().descend();
                        }
                        (Leaf(_), Leaf(_)) => break,
                        _ => unreachable!(),
                    }
                }
        
                left_root.fix_right_border(alloc.clone());
                right_root.fix_left_border(alloc);
                right_root
            }
        *)
        Definition split_off
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ Q; A ], [ self; key; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let key := M.alloc (| key |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ left_root := M.copy (| self |) in
                let~ right_root :=
                  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_pillar",
                        [ A ]
                      |),
                      [
                        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 (| left_root |) ]
                        |);
                        M.call_closure (|
                          M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                          [ alloc ]
                        |)
                      ]
                    |)
                  |) in
                let~ left_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 (| left_root |) ]
                    |)
                  |) in
                let~ right_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",
                        []
                      |),
                      [ right_root ]
                    |)
                  |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (let~ split_edge :=
                        M.copy (|
                          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"
                                    ],
                                  "search_node",
                                  [ Q ]
                                |),
                                [ M.read (| left_node |); M.read (| key |) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "alloc::collections::btree::search::SearchResult::Found",
                                      0
                                    |) in
                                  let kv := M.copy (| γ0_0 |) in
                                  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"
                                          ],
                                        "left_edge",
                                        []
                                      |),
                                      [ M.read (| kv |) ]
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "alloc::collections::btree::search::SearchResult::GoDown",
                                      0
                                    |) in
                                  let edge := M.copy (| γ0_0 |) in
                                  edge))
                            ]
                          |)
                        |) 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::Edge"
                                ],
                              "move_suffix",
                              []
                            |),
                            [ split_edge; right_node ]
                          |)
                        |) in
                      M.match_operator (|
                        M.alloc (|
                          Value.Tuple
                            [
                              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::Edge"
                                    ],
                                  "force",
                                  []
                                |),
                                [ M.read (| split_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::LeafOrInternal"
                                    ],
                                  "force",
                                  []
                                |),
                                [ M.read (| right_node |) ]
                              |)
                            ]
                        |),
                        [
                          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 γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "alloc::collections::btree::node::ForceResult::Internal",
                                  0
                                |) in
                              let edge := M.copy (| γ1_0 |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "alloc::collections::btree::node::ForceResult::Internal",
                                  0
                                |) in
                              let node := M.copy (| γ1_0 |) in
                              let~ _ :=
                                M.write (|
                                  left_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::Internal"
                                            ];
                                          Ty.path "alloc::collections::btree::node::marker::Edge"
                                        ],
                                      "descend",
                                      []
                                    |),
                                    [ M.read (| edge |) ]
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  right_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::Internal"
                                            ];
                                          Ty.path "alloc::collections::btree::node::marker::Edge"
                                        ],
                                      "descend",
                                      []
                                    |),
                                    [
                                      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"
                                            ],
                                          "first_edge",
                                          []
                                        |),
                                        [ M.read (| node |) ]
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          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 γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "alloc::collections::btree::node::ForceResult::Leaf",
                                  0
                                |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "alloc::collections::btree::node::ForceResult::Leaf",
                                  0
                                |) in
                              M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::panicking::panic", [] |),
                                    [
                                      M.read (|
                                        Value.String "internal error: entered unreachable code"
                                      |)
                                    ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) 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",
                        [ A ]
                      |),
                      [
                        M.read (| left_root |);
                        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_left_border",
                        [ A ]
                      |),
                      [ right_root; M.read (| alloc |) ]
                    |)
                  |) in
                right_root
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_split_off :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "split_off" (split_off K V).
        
        (*
            fn new_pillar<A: Allocator + Clone>(height: usize, alloc: A) -> Self {
                let mut root = Root::new(alloc.clone());
                for _ in 0..height {
                    root.push_internal_level(alloc.clone());
                }
                root
            }
        *)
        Definition new_pillar
            (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 ], [ height; alloc ] =>
            ltac:(M.monadic
              (let height := M.alloc (| height |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ root :=
                  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 (| 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 ]
                                                |),
                                                [
                                                  root;
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::clone::Clone",
                                                      A,
                                                      [],
                                                      "clone",
                                                      []
                                                    |),
                                                    [ alloc ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                root
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_pillar :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "new_pillar" (new_pillar K V).
      End Impl_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Owned_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
    End split.
  End btree.
End collections.
