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

Module collections.
  Module btree.
    Module search.
      (*
      Enum SearchBound
      {
        const_params := [];
        ty_params := [ "T" ];
        variants :=
          [
            {
              name := "Included";
              item := StructTuple [ T ];
              discriminant := None;
            };
            {
              name := "Excluded";
              item := StructTuple [ T ];
              discriminant := None;
            };
            {
              name := "AllIncluded";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "AllExcluded";
              item := StructTuple [];
              discriminant := None;
            }
          ];
      }
      *)
      
      Module Impl_alloc_collections_btree_search_SearchBound_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::btree::search::SearchBound") [] [ T ].
        
        (*
            pub fn from_range(range_bound: Bound<T>) -> Self {
                match range_bound {
                    Bound::Included(t) => Included(t),
                    Bound::Excluded(t) => Excluded(t),
                    Bound::Unbounded => AllIncluded,
                }
            }
        *)
        Definition from_range
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ range_bound ] =>
            ltac:(M.monadic
              (let range_bound := M.alloc (| range_bound |) in
              M.read (|
                M.match_operator (|
                  range_bound,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::range::Bound::Included",
                            0
                          |) in
                        let t := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "alloc::collections::btree::search::SearchBound::Included"
                            [ M.read (| t |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::range::Bound::Excluded",
                            0
                          |) in
                        let t := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "alloc::collections::btree::search::SearchBound::Excluded"
                            [ M.read (| t |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::ops::range::Bound::Unbounded" |) in
                        M.alloc (|
                          Value.StructTuple
                            "alloc::collections::btree::search::SearchBound::AllIncluded"
                            []
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_from_range :
          forall (T : Ty.t),
          M.IsAssociatedFunction (Self T) "from_range" (from_range T).
      End Impl_alloc_collections_btree_search_SearchBound_T.
      
      (*
      Enum SearchResult
      {
        const_params := [];
        ty_params := [ "BorrowType"; "K"; "V"; "FoundType"; "GoDownType" ];
        variants :=
          [
            {
              name := "Found";
              item :=
                StructTuple
                  [
                    Ty.apply
                      (Ty.path "alloc::collections::btree::node::Handle")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [ BorrowType; K; V; FoundType ];
                        Ty.path "alloc::collections::btree::node::marker::KV"
                      ]
                  ];
              discriminant := None;
            };
            {
              name := "GoDown";
              item :=
                StructTuple
                  [
                    Ty.apply
                      (Ty.path "alloc::collections::btree::node::Handle")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [ BorrowType; K; V; GoDownType ];
                        Ty.path "alloc::collections::btree::node::marker::Edge"
                      ]
                  ];
              discriminant := None;
            }
          ];
      }
      *)
      
      (*
      Enum IndexResult
      {
        const_params := [];
        ty_params := [];
        variants :=
          [
            {
              name := "KV";
              item := StructTuple [ Ty.path "usize" ];
              discriminant := None;
            };
            {
              name := "Edge";
              item := StructTuple [ Ty.path "usize" ];
              discriminant := None;
            }
          ];
      }
      *)
      
      Module Impl_alloc_collections_btree_node_NodeRef_BorrowType_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
        Definition Self (BorrowType K V : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::node::NodeRef")
            []
            [ BorrowType; K; V; Ty.path "alloc::collections::btree::node::marker::LeafOrInternal" ].
        
        (*
            pub fn search_tree<Q: ?Sized>(
                mut self,
                key: &Q,
            ) -> SearchResult<BorrowType, K, V, marker::LeafOrInternal, marker::Leaf>
            where
                Q: Ord,
                K: Borrow<Q>,
            {
                loop {
                    self = match self.search_node(key) {
                        Found(handle) => return Found(handle),
                        GoDown(handle) => match handle.force() {
                            Leaf(leaf) => return GoDown(leaf),
                            Internal(internal) => internal.descend(),
                        },
                    }
                }
            }
        *)
        Definition search_tree
            (BorrowType K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V in
          match ε, τ, α with
          | [], [ Q ], [ self; key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let key := M.alloc (| key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      M.loop (|
                        ltac:(M.monadic
                          (M.write (|
                            self,
                            M.read (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::node::NodeRef")
                                        []
                                        [
                                          BorrowType;
                                          K;
                                          V;
                                          Ty.path
                                            "alloc::collections::btree::node::marker::LeafOrInternal"
                                        ],
                                      "search_node",
                                      [ Q ]
                                    |),
                                    [ M.read (| self |); 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 handle := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.StructTuple
                                                "alloc::collections::btree::search::SearchResult::Found"
                                                [ M.read (| handle |) ]
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "alloc::collections::btree::search::SearchResult::GoDown",
                                          0
                                        |) in
                                      let handle := M.copy (| γ0_0 |) in
                                      M.match_operator (|
                                        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")
                                                    []
                                                    [
                                                      BorrowType;
                                                      K;
                                                      V;
                                                      Ty.path
                                                        "alloc::collections::btree::node::marker::LeafOrInternal"
                                                    ];
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::Edge"
                                                ],
                                              "force",
                                              []
                                            |),
                                            [ M.read (| handle |) ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "alloc::collections::btree::node::ForceResult::Leaf",
                                                  0
                                                |) in
                                              let leaf := M.copy (| γ0_0 |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    M.return_ (|
                                                      Value.StructTuple
                                                        "alloc::collections::btree::search::SearchResult::GoDown"
                                                        [ M.read (| leaf |) ]
                                                    |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "alloc::collections::btree::node::ForceResult::Internal",
                                                  0
                                                |) in
                                              let internal := 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")
                                                          []
                                                          [
                                                            BorrowType;
                                                            K;
                                                            V;
                                                            Ty.path
                                                              "alloc::collections::btree::node::marker::Internal"
                                                          ];
                                                        Ty.path
                                                          "alloc::collections::btree::node::marker::Edge"
                                                      ],
                                                    "descend",
                                                    []
                                                  |),
                                                  [ M.read (| internal |) ]
                                                |)
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)
                            |)
                          |)))
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_search_tree :
          forall (BorrowType K V : Ty.t),
          M.IsAssociatedFunction (Self BorrowType K V) "search_tree" (search_tree BorrowType K V).
        
        (*
            pub fn search_tree_for_bifurcation<'r, Q: ?Sized, R>(
                mut self,
                range: &'r R,
            ) -> Result<
                (
                    NodeRef<BorrowType, K, V, marker::LeafOrInternal>,
                    usize,
                    usize,
                    SearchBound<&'r Q>,
                    SearchBound<&'r Q>,
                ),
                Handle<NodeRef<BorrowType, K, V, marker::Leaf>, marker::Edge>,
            >
            where
                Q: Ord,
                K: Borrow<Q>,
                R: RangeBounds<Q>,
            {
                // Determine if map or set is being searched
                let is_set = <V as super::set_val::IsSetVal>::is_set_val();
        
                // Inlining these variables should be avoided. We assume the bounds reported by `range`
                // remain the same, but an adversarial implementation could change between calls (#81138).
                let (start, end) = (range.start_bound(), range.end_bound());
                match (start, end) {
                    (Bound::Excluded(s), Bound::Excluded(e)) if s == e => {
                        if is_set {
                            panic!("range start and end are equal and excluded in BTreeSet")
                        } else {
                            panic!("range start and end are equal and excluded in BTreeMap")
                        }
                    }
                    (Bound::Included(s) | Bound::Excluded(s), Bound::Included(e) | Bound::Excluded(e))
                        if s > e =>
                    {
                        if is_set {
                            panic!("range start is greater than range end in BTreeSet")
                        } else {
                            panic!("range start is greater than range end in BTreeMap")
                        }
                    }
                    _ => {}
                }
                let mut lower_bound = SearchBound::from_range(start);
                let mut upper_bound = SearchBound::from_range(end);
                loop {
                    let (lower_edge_idx, lower_child_bound) = self.find_lower_bound_index(lower_bound);
                    let (upper_edge_idx, upper_child_bound) =
                        unsafe { self.find_upper_bound_index(upper_bound, lower_edge_idx) };
                    if lower_edge_idx < upper_edge_idx {
                        return Ok((
                            self,
                            lower_edge_idx,
                            upper_edge_idx,
                            lower_child_bound,
                            upper_child_bound,
                        ));
                    }
                    debug_assert_eq!(lower_edge_idx, upper_edge_idx);
                    let common_edge = unsafe { Handle::new_edge(self, lower_edge_idx) };
                    match common_edge.force() {
                        Leaf(common_edge) => return Err(common_edge),
                        Internal(common_edge) => {
                            self = common_edge.descend();
                            lower_bound = lower_child_bound;
                            upper_bound = upper_child_bound;
                        }
                    }
                }
            }
        *)
        Definition search_tree_for_bifurcation
            (BorrowType K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V in
          match ε, τ, α with
          | [], [ Q; R ], [ self; range ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let range := M.alloc (| range |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ is_set :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "alloc::collections::btree::set_val::IsSetVal",
                            V,
                            [],
                            "is_set_val",
                            []
                          |),
                          []
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        Value.Tuple
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::range::RangeBounds",
                                R,
                                [ Q ],
                                "start_bound",
                                []
                              |),
                              [ M.read (| range |) ]
                            |);
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::range::RangeBounds",
                                R,
                                [ Q ],
                                "end_bound",
                                []
                              |),
                              [ M.read (| range |) ]
                            |)
                          ]
                      |),
                      [
                        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 start := M.copy (| γ0_0 |) in
                            let end_ := M.copy (| γ0_1 |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [ M.read (| start |); M.read (| 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 γ1_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ0_0,
                                          "core::ops::range::Bound::Excluded",
                                          0
                                        |) in
                                      let s := M.copy (| γ1_0 |) in
                                      let γ1_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ0_1,
                                          "core::ops::range::Bound::Excluded",
                                          0
                                        |) in
                                      let e := M.copy (| γ1_0 |) in
                                      let γ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialEq",
                                              Ty.apply (Ty.path "&") [] [ Q ],
                                              [ Ty.apply (Ty.path "&") [] [ Q ] ],
                                              "eq",
                                              []
                                            |),
                                            [ s; e ]
                                          |)
                                        |) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ := M.use is_set in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::panicking::panic_fmt",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::Arguments",
                                                          "new_const",
                                                          []
                                                        |),
                                                        [
                                                          M.alloc (|
                                                            Value.Array
                                                              [
                                                                M.read (|
                                                                  Value.String
                                                                    "range start and end are equal and excluded in BTreeSet"
                                                                |)
                                                              ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.alloc (|
                                                M.never_to_any (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::panicking::panic_fmt",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::Arguments",
                                                          "new_const",
                                                          []
                                                        |),
                                                        [
                                                          M.alloc (|
                                                            Value.Array
                                                              [
                                                                M.read (|
                                                                  Value.String
                                                                    "range start and end are equal and excluded in BTreeMap"
                                                                |)
                                                              ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |)
                                              |)))
                                        ]
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                      M.find_or_pattern (|
                                        γ0_0,
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::ops::range::Bound::Included",
                                                  0
                                                |) in
                                              let s := M.copy (| γ0_0 |) in
                                              Value.Tuple [ s ]));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::ops::range::Bound::Excluded",
                                                  0
                                                |) in
                                              let s := M.copy (| γ0_0 |) in
                                              Value.Tuple [ s ]))
                                        ],
                                        M.closure
                                          (fun γ =>
                                            ltac:(M.monadic
                                              match γ with
                                              | [ s ] =>
                                                ltac:(M.monadic
                                                  (M.find_or_pattern (|
                                                    γ0_1,
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::range::Bound::Included",
                                                              0
                                                            |) in
                                                          let e := M.copy (| γ0_0 |) in
                                                          Value.Tuple [ e ]));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::range::Bound::Excluded",
                                                              0
                                                            |) in
                                                          let e := M.copy (| γ0_0 |) in
                                                          Value.Tuple [ e ]))
                                                    ],
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ e ] =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::cmp::PartialOrd",
                                                                      Ty.apply
                                                                        (Ty.path "&")
                                                                        []
                                                                        [ Q ],
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Q ]
                                                                      ],
                                                                      "gt",
                                                                      []
                                                                    |),
                                                                    [
                                                                      s;
                                                                      M.alloc (| M.read (| e |) |)
                                                                    ]
                                                                  |)
                                                                |) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.match_operator (|
                                                                M.alloc (| Value.Tuple [] |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ := M.use is_set in
                                                                      let _ :=
                                                                        M.is_constant_or_break_match (|
                                                                          M.read (| γ |),
                                                                          Value.Bool true
                                                                        |) in
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::panicking::panic_fmt",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.path
                                                                                    "core::fmt::Arguments",
                                                                                  "new_const",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.alloc (|
                                                                                    Value.Array
                                                                                      [
                                                                                        M.read (|
                                                                                          Value.String
                                                                                            "range start is greater than range end in BTreeSet"
                                                                                        |)
                                                                                      ]
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::panicking::panic_fmt",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.path
                                                                                    "core::fmt::Arguments",
                                                                                  "new_const",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.alloc (|
                                                                                    Value.Array
                                                                                      [
                                                                                        M.read (|
                                                                                          Value.String
                                                                                            "range start is greater than range end in BTreeMap"
                                                                                        |)
                                                                                      ]
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  |)))
                                              | _ => M.impossible "wrong number of arguments"
                                              end))
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ lower_bound :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::search::SearchBound")
                                      []
                                      [ Ty.apply (Ty.path "&") [] [ Q ] ],
                                    "from_range",
                                    []
                                  |),
                                  [ M.read (| start |) ]
                                |)
                              |) in
                            let~ upper_bound :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::search::SearchBound")
                                      []
                                      [ Ty.apply (Ty.path "&") [] [ Q ] ],
                                    "from_range",
                                    []
                                  |),
                                  [ M.read (| end_ |) ]
                                |)
                              |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.loop (|
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                                []
                                                [
                                                  BorrowType;
                                                  K;
                                                  V;
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::LeafOrInternal"
                                                ],
                                              "find_lower_bound_index",
                                              [ Q ]
                                            |),
                                            [ self; M.read (| lower_bound |) ]
                                          |)
                                        |),
                                        [
                                          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 lower_edge_idx := M.copy (| γ0_0 |) in
                                              let lower_child_bound := M.copy (| γ0_1 |) in
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path
                                                          "alloc::collections::btree::node::NodeRef")
                                                        []
                                                        [
                                                          BorrowType;
                                                          K;
                                                          V;
                                                          Ty.path
                                                            "alloc::collections::btree::node::marker::LeafOrInternal"
                                                        ],
                                                      "find_upper_bound_index",
                                                      [ Q ]
                                                    |),
                                                    [
                                                      self;
                                                      M.read (| upper_bound |);
                                                      M.read (| lower_edge_idx |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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 upper_edge_idx := M.copy (| γ0_0 |) in
                                                      let upper_child_bound := 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.read (| lower_edge_idx |),
                                                                        M.read (| upper_edge_idx |)
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                M.alloc (|
                                                                  M.never_to_any (|
                                                                    M.read (|
                                                                      M.return_ (|
                                                                        Value.StructTuple
                                                                          "core::result::Result::Ok"
                                                                          [
                                                                            Value.Tuple
                                                                              [
                                                                                M.read (| self |);
                                                                                M.read (|
                                                                                  lower_edge_idx
                                                                                |);
                                                                                M.read (|
                                                                                  upper_edge_idx
                                                                                |);
                                                                                M.read (|
                                                                                  lower_child_bound
                                                                                |);
                                                                                M.read (|
                                                                                  upper_child_bound
                                                                                |)
                                                                              ]
                                                                          ]
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) 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
                                                                        [
                                                                          lower_edge_idx;
                                                                          upper_edge_idx
                                                                        ]
                                                                    |),
                                                                    [
                                                                      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
                                                      let~ common_edge :=
                                                        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")
                                                                    []
                                                                    [
                                                                      BorrowType;
                                                                      K;
                                                                      V;
                                                                      Ty.path
                                                                        "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                    ];
                                                                  Ty.path
                                                                    "alloc::collections::btree::node::marker::Edge"
                                                                ],
                                                              "new_edge",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| self |);
                                                              M.read (| lower_edge_idx |)
                                                            ]
                                                          |)
                                                        |) in
                                                      M.match_operator (|
                                                        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")
                                                                    []
                                                                    [
                                                                      BorrowType;
                                                                      K;
                                                                      V;
                                                                      Ty.path
                                                                        "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                    ];
                                                                  Ty.path
                                                                    "alloc::collections::btree::node::marker::Edge"
                                                                ],
                                                              "force",
                                                              []
                                                            |),
                                                            [ M.read (| common_edge |) ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "alloc::collections::btree::node::ForceResult::Leaf",
                                                                  0
                                                                |) in
                                                              let common_edge :=
                                                                M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      Value.StructTuple
                                                                        "core::result::Result::Err"
                                                                        [ M.read (| common_edge |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "alloc::collections::btree::node::ForceResult::Internal",
                                                                  0
                                                                |) in
                                                              let common_edge :=
                                                                M.copy (| γ0_0 |) in
                                                              let~ _ :=
                                                                M.write (|
                                                                  self,
                                                                  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")
                                                                            []
                                                                            [
                                                                              BorrowType;
                                                                              K;
                                                                              V;
                                                                              Ty.path
                                                                                "alloc::collections::btree::node::marker::Internal"
                                                                            ];
                                                                          Ty.path
                                                                            "alloc::collections::btree::node::marker::Edge"
                                                                        ],
                                                                      "descend",
                                                                      []
                                                                    |),
                                                                    [ M.read (| common_edge |) ]
                                                                  |)
                                                                |) in
                                                              let~ _ :=
                                                                M.write (|
                                                                  lower_bound,
                                                                  M.read (| lower_child_bound |)
                                                                |) in
                                                              let~ _ :=
                                                                M.write (|
                                                                  upper_bound,
                                                                  M.read (| upper_child_bound |)
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |)))
                                                ]
                                              |)))
                                        ]
                                      |)))
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_search_tree_for_bifurcation :
          forall (BorrowType K V : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V)
            "search_tree_for_bifurcation"
            (search_tree_for_bifurcation BorrowType K V).
        
        (*
            pub fn find_lower_bound_edge<'r, Q>(
                self,
                bound: SearchBound<&'r Q>,
            ) -> (Handle<Self, marker::Edge>, SearchBound<&'r Q>)
            where
                Q: ?Sized + Ord,
                K: Borrow<Q>,
            {
                let (edge_idx, bound) = self.find_lower_bound_index(bound);
                let edge = unsafe { Handle::new_edge(self, edge_idx) };
                (edge, bound)
            }
        *)
        Definition find_lower_bound_edge
            (BorrowType K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V in
          match ε, τ, α with
          | [], [ Q ], [ self; bound ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let bound := M.alloc (| bound |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            BorrowType;
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ],
                        "find_lower_bound_index",
                        [ Q ]
                      |),
                      [ self; M.read (| bound |) ]
                    |)
                  |),
                  [
                    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 edge_idx := M.copy (| γ0_0 |) in
                        let bound := M.copy (| γ0_1 |) in
                        let~ edge :=
                          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")
                                      []
                                      [
                                        BorrowType;
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ];
                                    Ty.path "alloc::collections::btree::node::marker::Edge"
                                  ],
                                "new_edge",
                                []
                              |),
                              [ M.read (| self |); M.read (| edge_idx |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [ M.read (| edge |); M.read (| bound |) ] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_find_lower_bound_edge :
          forall (BorrowType K V : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V)
            "find_lower_bound_edge"
            (find_lower_bound_edge BorrowType K V).
        
        (*
            pub fn find_upper_bound_edge<'r, Q>(
                self,
                bound: SearchBound<&'r Q>,
            ) -> (Handle<Self, marker::Edge>, SearchBound<&'r Q>)
            where
                Q: ?Sized + Ord,
                K: Borrow<Q>,
            {
                let (edge_idx, bound) = unsafe { self.find_upper_bound_index(bound, 0) };
                let edge = unsafe { Handle::new_edge(self, edge_idx) };
                (edge, bound)
            }
        *)
        Definition find_upper_bound_edge
            (BorrowType K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V in
          match ε, τ, α with
          | [], [ Q ], [ self; bound ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let bound := M.alloc (| bound |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            BorrowType;
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ],
                        "find_upper_bound_index",
                        [ Q ]
                      |),
                      [ self; M.read (| bound |); Value.Integer IntegerKind.Usize 0 ]
                    |)
                  |),
                  [
                    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 edge_idx := M.copy (| γ0_0 |) in
                        let bound := M.copy (| γ0_1 |) in
                        let~ edge :=
                          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")
                                      []
                                      [
                                        BorrowType;
                                        K;
                                        V;
                                        Ty.path
                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                      ];
                                    Ty.path "alloc::collections::btree::node::marker::Edge"
                                  ],
                                "new_edge",
                                []
                              |),
                              [ M.read (| self |); M.read (| edge_idx |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [ M.read (| edge |); M.read (| bound |) ] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_find_upper_bound_edge :
          forall (BorrowType K V : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V)
            "find_upper_bound_edge"
            (find_upper_bound_edge BorrowType K V).
      End Impl_alloc_collections_btree_node_NodeRef_BorrowType_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
      
      Module Impl_alloc_collections_btree_node_NodeRef_BorrowType_K_V_Type_.
        Definition Self (BorrowType K V Type_ : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::node::NodeRef")
            []
            [ BorrowType; K; V; Type_ ].
        
        (*
            pub fn search_node<Q: ?Sized>(self, key: &Q) -> SearchResult<BorrowType, K, V, Type, Type>
            where
                Q: Ord,
                K: Borrow<Q>,
            {
                match unsafe { self.find_key_index(key, 0) } {
                    IndexResult::KV(idx) => Found(unsafe { Handle::new_kv(self, idx) }),
                    IndexResult::Edge(idx) => GoDown(unsafe { Handle::new_edge(self, idx) }),
                }
            }
        *)
        Definition search_node
            (BorrowType K V Type_ : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V Type_ in
          match ε, τ, α with
          | [], [ Q ], [ self; key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let key := M.alloc (| key |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [ BorrowType; K; V; Type_ ],
                        "find_key_index",
                        [ Q ]
                      |),
                      [ self; M.read (| key |); Value.Integer IntegerKind.Usize 0 ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::search::IndexResult::KV",
                            0
                          |) in
                        let idx := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "alloc::collections::btree::search::SearchResult::Found"
                            [
                              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")
                                        []
                                        [ BorrowType; K; V; Type_ ];
                                      Ty.path "alloc::collections::btree::node::marker::KV"
                                    ],
                                  "new_kv",
                                  []
                                |),
                                [ M.read (| self |); M.read (| idx |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::search::IndexResult::Edge",
                            0
                          |) in
                        let idx := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "alloc::collections::btree::search::SearchResult::GoDown"
                            [
                              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")
                                        []
                                        [ BorrowType; K; V; Type_ ];
                                      Ty.path "alloc::collections::btree::node::marker::Edge"
                                    ],
                                  "new_edge",
                                  []
                                |),
                                [ M.read (| self |); M.read (| idx |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_search_node :
          forall (BorrowType K V Type_ : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V Type_)
            "search_node"
            (search_node BorrowType K V Type_).
        
        (*
            unsafe fn find_key_index<Q: ?Sized>(&self, key: &Q, start_index: usize) -> IndexResult
            where
                Q: Ord,
                K: Borrow<Q>,
            {
                let node = self.reborrow();
                let keys = node.keys();
                debug_assert!(start_index <= keys.len());
                for (offset, k) in unsafe { keys.get_unchecked(start_index..) }.iter().enumerate() {
                    match key.cmp(k.borrow()) {
                        Ordering::Greater => {}
                        Ordering::Equal => return IndexResult::KV(start_index + offset),
                        Ordering::Less => return IndexResult::Edge(start_index + offset),
                    }
                }
                IndexResult::Edge(keys.len())
            }
        *)
        Definition find_key_index
            (BorrowType K V Type_ : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V Type_ in
          match ε, τ, α with
          | [], [ Q ], [ self; key; start_index ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let key := M.alloc (| key |) in
              let start_index := M.alloc (| start_index |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ node :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::node::NodeRef")
                              []
                              [ BorrowType; K; V; Type_ ],
                            "reborrow",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |) in
                    let~ keys :=
                      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;
                                Type_
                              ],
                            "keys",
                            []
                          |),
                          [ node ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.use (M.alloc (| Value.Bool true |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              UnOp.not (|
                                                BinOp.le (|
                                                  M.read (| start_index |),
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "slice") [] [ K ],
                                                      "len",
                                                      []
                                                    |),
                                                    [ M.read (| keys |) ]
                                                  |)
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.call_closure (|
                                              M.get_function (| "core::panicking::panic", [] |),
                                              [
                                                M.read (|
                                                  Value.String
                                                    "assertion failed: start_index <= keys.len()"
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) 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::iter::adapters::enumerate::Enumerate")
                                  []
                                  [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ K ] ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ K ],
                                    [],
                                    "enumerate",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ K ],
                                        "iter",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ K ],
                                            "get_unchecked",
                                            [
                                              Ty.apply
                                                (Ty.path "core::ops::range::RangeFrom")
                                                []
                                                [ Ty.path "usize" ]
                                            ]
                                          |),
                                          [
                                            M.read (| keys |);
                                            Value.StructRecord
                                              "core::ops::range::RangeFrom"
                                              [ ("start", M.read (| start_index |)) ]
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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::iter::adapters::enumerate::Enumerate")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [ K ]
                                                ],
                                              [],
                                              "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 offset := M.copy (| γ1_0 |) in
                                              let k := M.copy (| γ1_1 |) in
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::cmp::Ord",
                                                      Q,
                                                      [],
                                                      "cmp",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| key |);
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::borrow::Borrow",
                                                          K,
                                                          [ Q ],
                                                          "borrow",
                                                          []
                                                        |),
                                                        [ M.read (| k |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::cmp::Ordering::Greater"
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::cmp::Ordering::Equal"
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              Value.StructTuple
                                                                "alloc::collections::btree::search::IndexResult::KV"
                                                                [
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| start_index |),
                                                                    M.read (| offset |)
                                                                  |)
                                                                ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::cmp::Ordering::Less"
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              Value.StructTuple
                                                                "alloc::collections::btree::search::IndexResult::Edge"
                                                                [
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| start_index |),
                                                                    M.read (| offset |)
                                                                  |)
                                                                ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)))
                                                ]
                                              |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    M.alloc (|
                      Value.StructTuple
                        "alloc::collections::btree::search::IndexResult::Edge"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ K ],
                              "len",
                              []
                            |),
                            [ M.read (| keys |) ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_find_key_index :
          forall (BorrowType K V Type_ : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V Type_)
            "find_key_index"
            (find_key_index BorrowType K V Type_).
        
        (*
            fn find_lower_bound_index<'r, Q>(
                &self,
                bound: SearchBound<&'r Q>,
            ) -> (usize, SearchBound<&'r Q>)
            where
                Q: ?Sized + Ord,
                K: Borrow<Q>,
            {
                match bound {
                    Included(key) => match unsafe { self.find_key_index(key, 0) } {
                        IndexResult::KV(idx) => (idx, AllExcluded),
                        IndexResult::Edge(idx) => (idx, bound),
                    },
                    Excluded(key) => match unsafe { self.find_key_index(key, 0) } {
                        IndexResult::KV(idx) => (idx + 1, AllIncluded),
                        IndexResult::Edge(idx) => (idx, bound),
                    },
                    AllIncluded => (0, AllIncluded),
                    AllExcluded => (self.len(), AllExcluded),
                }
            }
        *)
        Definition find_lower_bound_index
            (BorrowType K V Type_ : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V Type_ in
          match ε, τ, α with
          | [], [ Q ], [ self; bound ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let bound := M.alloc (| bound |) in
              M.read (|
                M.match_operator (|
                  bound,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::Included",
                            0
                          |) in
                        let key := M.copy (| γ0_0 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [ BorrowType; K; V; Type_ ],
                                "find_key_index",
                                [ Q ]
                              |),
                              [
                                M.read (| self |);
                                M.read (| key |);
                                Value.Integer IntegerKind.Usize 0
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::KV",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      M.read (| idx |);
                                      Value.StructTuple
                                        "alloc::collections::btree::search::SearchBound::AllExcluded"
                                        []
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::Edge",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (| Value.Tuple [ M.read (| idx |); M.read (| bound |) ] |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::Excluded",
                            0
                          |) in
                        let key := M.copy (| γ0_0 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [ BorrowType; K; V; Type_ ],
                                "find_key_index",
                                [ Q ]
                              |),
                              [
                                M.read (| self |);
                                M.read (| key |);
                                Value.Integer IntegerKind.Usize 0
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::KV",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      BinOp.Wrap.add (|
                                        M.read (| idx |),
                                        Value.Integer IntegerKind.Usize 1
                                      |);
                                      Value.StructTuple
                                        "alloc::collections::btree::search::SearchBound::AllIncluded"
                                        []
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::Edge",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (| Value.Tuple [ M.read (| idx |); M.read (| bound |) ] |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::AllIncluded"
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              Value.Integer IntegerKind.Usize 0;
                              Value.StructTuple
                                "alloc::collections::btree::search::SearchBound::AllIncluded"
                                []
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::AllExcluded"
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::NodeRef")
                                    []
                                    [ BorrowType; K; V; Type_ ],
                                  "len",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |);
                              Value.StructTuple
                                "alloc::collections::btree::search::SearchBound::AllExcluded"
                                []
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_find_lower_bound_index :
          forall (BorrowType K V Type_ : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V Type_)
            "find_lower_bound_index"
            (find_lower_bound_index BorrowType K V Type_).
        
        (*
            unsafe fn find_upper_bound_index<'r, Q>(
                &self,
                bound: SearchBound<&'r Q>,
                start_index: usize,
            ) -> (usize, SearchBound<&'r Q>)
            where
                Q: ?Sized + Ord,
                K: Borrow<Q>,
            {
                match bound {
                    Included(key) => match unsafe { self.find_key_index(key, start_index) } {
                        IndexResult::KV(idx) => (idx + 1, AllExcluded),
                        IndexResult::Edge(idx) => (idx, bound),
                    },
                    Excluded(key) => match unsafe { self.find_key_index(key, start_index) } {
                        IndexResult::KV(idx) => (idx, AllIncluded),
                        IndexResult::Edge(idx) => (idx, bound),
                    },
                    AllIncluded => (self.len(), AllIncluded),
                    AllExcluded => (start_index, AllExcluded),
                }
            }
        *)
        Definition find_upper_bound_index
            (BorrowType K V Type_ : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self BorrowType K V Type_ in
          match ε, τ, α with
          | [], [ Q ], [ self; bound; start_index ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let bound := M.alloc (| bound |) in
              let start_index := M.alloc (| start_index |) in
              M.read (|
                M.match_operator (|
                  bound,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::Included",
                            0
                          |) in
                        let key := M.copy (| γ0_0 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [ BorrowType; K; V; Type_ ],
                                "find_key_index",
                                [ Q ]
                              |),
                              [ M.read (| self |); M.read (| key |); M.read (| start_index |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::KV",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      BinOp.Wrap.add (|
                                        M.read (| idx |),
                                        Value.Integer IntegerKind.Usize 1
                                      |);
                                      Value.StructTuple
                                        "alloc::collections::btree::search::SearchBound::AllExcluded"
                                        []
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::Edge",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (| Value.Tuple [ M.read (| idx |); M.read (| bound |) ] |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::Excluded",
                            0
                          |) in
                        let key := M.copy (| γ0_0 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::node::NodeRef")
                                  []
                                  [ BorrowType; K; V; Type_ ],
                                "find_key_index",
                                [ Q ]
                              |),
                              [ M.read (| self |); M.read (| key |); M.read (| start_index |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::KV",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      M.read (| idx |);
                                      Value.StructTuple
                                        "alloc::collections::btree::search::SearchBound::AllIncluded"
                                        []
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "alloc::collections::btree::search::IndexResult::Edge",
                                    0
                                  |) in
                                let idx := M.copy (| γ0_0 |) in
                                M.alloc (| Value.Tuple [ M.read (| idx |); M.read (| bound |) ] |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::AllIncluded"
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::NodeRef")
                                    []
                                    [ BorrowType; K; V; Type_ ],
                                  "len",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |);
                              Value.StructTuple
                                "alloc::collections::btree::search::SearchBound::AllIncluded"
                                []
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "alloc::collections::btree::search::SearchBound::AllExcluded"
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.read (| start_index |);
                              Value.StructTuple
                                "alloc::collections::btree::search::SearchBound::AllExcluded"
                                []
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_find_upper_bound_index :
          forall (BorrowType K V Type_ : Ty.t),
          M.IsAssociatedFunction
            (Self BorrowType K V Type_)
            "find_upper_bound_index"
            (find_upper_bound_index BorrowType K V Type_).
      End Impl_alloc_collections_btree_node_NodeRef_BorrowType_K_V_Type_.
    End search.
  End btree.
End collections.
