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

Module slice.
  Module sort.
    Module select.
      (*
      pub(crate) fn partition_at_index<T, F>(
          v: &mut [T],
          index: usize,
          mut is_less: F,
      ) -> (&mut [T], &mut T, &mut [T])
      where
          F: FnMut(&T, &T) -> bool,
      {
          let len = v.len();
      
          // Puts a lower limit of 1 on `len`.
          if index >= len {
              panic!("partition_at_index index {} greater than length of slice {}", index, len);
          }
      
          if T::IS_ZST {
              // Sorting has no meaningful behavior on zero-sized types. Do nothing.
          } else if index == len - 1 {
              // Find max element and place it in the last position of the array. We're free to use
              // `unwrap()` here because we checked that `v` is not empty.
              let max_idx = max_index(v, &mut is_less).unwrap();
              v.swap(max_idx, index);
          } else if index == 0 {
              // Find min element and place it in the first position of the array. We're free to use
              // `unwrap()` here because we checked that `v` is not empty.
              let min_idx = min_index(v, &mut is_less).unwrap();
              v.swap(min_idx, index);
          } else {
              cfg_if! {
                  if #[cfg(feature = "optimize_for_size")] {
                      median_of_medians(v, &mut is_less, index);
                  } else {
                      partition_at_index_loop(v, index, None, &mut is_less);
                  }
              }
          }
      
          let (left, right) = v.split_at_mut(index);
          let (pivot, right) = right.split_at_mut(1);
          let pivot = &mut pivot[0];
          (left, pivot, right)
      }
      *)
      Definition partition_at_index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ v; index; is_less ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let index := M.alloc (| index |) in
            let is_less := M.alloc (| is_less |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "len", [] |),
                    [ M.read (| v |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (| BinOp.ge (| M.read (| index |), M.read (| len |) |) |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic_fmt", [] |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::Arguments",
                                    "new_v1",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      Value.Array
                                        [
                                          M.read (| Value.String "partition_at_index index " |);
                                          M.read (| Value.String " greater than length of slice " |)
                                        ]
                                    |);
                                    M.alloc (|
                                      Value.Array
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::fmt::rt::Argument",
                                              "new_display",
                                              [ Ty.path "usize" ]
                                            |),
                                            [ index ]
                                          |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::fmt::rt::Argument",
                                              "new_display",
                                              [ Ty.path "usize" ]
                                            |),
                                            [ len ]
                                          |)
                                        ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |)
                        |)));
                    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.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.eq (|
                                        M.read (| index |),
                                        BinOp.Wrap.sub (|
                                          M.read (| len |),
                                          Value.Integer IntegerKind.Usize 1
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ max_idx :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "usize" ],
                                        "unwrap",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::slice::sort::select::max_index",
                                            [ T; F ]
                                          |),
                                          [ M.read (| v |); is_less ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ T ],
                                        "swap",
                                        []
                                      |),
                                      [ M.read (| v |); M.read (| max_idx |); M.read (| index |) ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.eq (|
                                                M.read (| index |),
                                                Value.Integer IntegerKind.Usize 0
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ min_idx :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "usize" ],
                                                "unwrap",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::slice::sort::select::min_index",
                                                    [ T; F ]
                                                  |),
                                                  [ M.read (| v |); is_less ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "swap",
                                                []
                                              |),
                                              [
                                                M.read (| v |);
                                                M.read (| min_idx |);
                                                M.read (| index |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::sort::select::partition_at_index_loop",
                                                [ T; F ]
                                              |),
                                              [
                                                M.read (| v |);
                                                M.read (| index |);
                                                Value.StructTuple "core::option::Option::None" [];
                                                is_less
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)))
                          ]
                        |)))
                  ]
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ T ],
                      "split_at_mut",
                      []
                    |),
                    [ M.read (| v |); M.read (| index |) ]
                  |)
                |),
                [
                  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 := M.copy (| γ0_0 |) in
                      let right := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ T ],
                              "split_at_mut",
                              []
                            |),
                            [ M.read (| right |); Value.Integer IntegerKind.Usize 1 ]
                          |)
                        |),
                        [
                          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 pivot := M.copy (| γ0_0 |) in
                              let right := M.copy (| γ0_1 |) in
                              let~ pivot :=
                                M.alloc (|
                                  M.SubPointer.get_array_field (|
                                    M.read (| pivot |),
                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                  |)
                                |) in
                              M.alloc (|
                                Value.Tuple
                                  [ M.read (| left |); M.read (| pivot |); M.read (| right |) ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_partition_at_index :
        M.IsFunction "core::slice::sort::select::partition_at_index" partition_at_index.
      
      Definition value_INSERTION_SORT_THRESHOLD : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 16 |))).
      
      (*
      fn partition_at_index_loop<'a, T, F>(
          mut v: &'a mut [T],
          mut index: usize,
          mut ancestor_pivot: Option<&'a T>,
          is_less: &mut F,
      ) where
          F: FnMut(&T, &T) -> bool,
      {
          // Limit the amount of iterations and fall back to fast deterministic selection to ensure O(n)
          // worst case running time. This limit needs to be constant, because using `ilog2(len)` like in
          // `sort` would result in O(n log n) time complexity. The exact value of the limit is chosen
          // somewhat arbitrarily, but for most inputs bad pivot selections should be relatively rare, so
          // the limit is reached for sub-slices len / (2^limit or less). Which makes the remaining work
          // with the fallback minimal in relative terms.
          let mut limit = 16;
      
          loop {
              if v.len() <= INSERTION_SORT_THRESHOLD {
                  if v.len() >= 2 {
                      insertion_sort_shift_left(v, 1, is_less);
                  }
                  return;
              }
      
              if limit == 0 {
                  median_of_medians(v, is_less, index);
                  return;
              }
      
              limit -= 1;
      
              // Choose a pivot
              let pivot_pos = choose_pivot(v, is_less);
      
              // If the chosen pivot is equal to the predecessor, then it's the smallest element in the
              // slice. Partition the slice into elements equal to and elements greater than the pivot.
              // This case is usually hit when the slice contains many duplicate elements.
              if let Some(p) = ancestor_pivot {
                  // SAFETY: choose_pivot promises to return a valid pivot position.
                  let pivot = unsafe { v.get_unchecked(pivot_pos) };
      
                  if !is_less(p, pivot) {
                      let num_lt = partition(v, pivot_pos, &mut |a, b| !is_less(b, a));
      
                      // Continue sorting elements greater than the pivot. We know that `mid` contains
                      // the pivot. So we can continue after `mid`.
                      let mid = num_lt + 1;
      
                      // If we've passed our index, then we're good.
                      if mid > index {
                          return;
                      }
      
                      v = &mut v[mid..];
                      index = index - mid;
                      ancestor_pivot = None;
                      continue;
                  }
              }
      
              let mid = partition(v, pivot_pos, is_less);
      
              // Split the slice into `left`, `pivot`, and `right`.
              let (left, right) = v.split_at_mut(mid);
              let (pivot, right) = right.split_at_mut(1);
              let pivot = &pivot[0];
      
              if mid < index {
                  v = right;
                  index = index - mid - 1;
                  ancestor_pivot = Some(pivot);
              } else if mid > index {
                  v = left;
              } else {
                  // If mid == index, then we're done, since partition() guaranteed that all elements
                  // after mid are greater than or equal to mid.
                  return;
              }
          }
      }
      *)
      Definition partition_at_index_loop
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [ T; F ], [ v; index; ancestor_pivot; is_less ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let index := M.alloc (| index |) in
            let ancestor_pivot := M.alloc (| ancestor_pivot |) in
            let is_less := M.alloc (| is_less |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ limit := M.alloc (| Value.Integer IntegerKind.I32 16 |) in
                  M.alloc (|
                    M.never_to_any (|
                      M.read (|
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.le (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "slice") [] [ T ],
                                                  "len",
                                                  []
                                                |),
                                                [ M.read (| v |) ]
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "core::slice::sort::select::INSERTION_SORT_THRESHOLD"
                                                |)
                                              |)
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.ge (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [ T ],
                                                                  "len",
                                                                  []
                                                                |),
                                                                [ M.read (| v |) ]
                                                              |),
                                                              Value.Integer IntegerKind.Usize 2
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "core::slice::sort::shared::smallsort::insertion_sort_shift_left",
                                                              [ T; F ]
                                                            |),
                                                            [
                                                              M.read (| v |);
                                                              Value.Integer IntegerKind.Usize 1;
                                                              M.read (| is_less |)
                                                            ]
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  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 (|
                                            BinOp.eq (|
                                              M.read (| limit |),
                                              Value.Integer IntegerKind.I32 0
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::slice::sort::select::median_of_medians",
                                                    [ T; F ]
                                                  |),
                                                  [
                                                    M.read (| v |);
                                                    M.read (| is_less |);
                                                    M.read (| index |)
                                                  ]
                                                |)
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              let β := limit in
                              M.write (|
                                β,
                                BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.I32 1 |)
                              |) in
                            let~ pivot_pos :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::slice::sort::shared::pivot::choose_pivot",
                                    [ T; F ]
                                  |),
                                  [ M.read (| v |); M.read (| is_less |) ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := ancestor_pivot in
                                      let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let p := M.copy (| γ0_0 |) in
                                      let~ pivot :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply (Ty.path "slice") [] [ T ],
                                              "get_unchecked",
                                              [ Ty.path "usize" ]
                                            |),
                                            [ M.read (| v |); M.read (| pivot_pos |) ]
                                          |)
                                        |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    UnOp.not (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::FnMut",
                                                          F,
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply (Ty.path "&") [] [ T ];
                                                                Ty.apply (Ty.path "&") [] [ T ]
                                                              ]
                                                          ],
                                                          "call_mut",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| is_less |);
                                                          Value.Tuple
                                                            [ M.read (| p |); M.read (| pivot |) ]
                                                        ]
                                                      |)
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    let~ num_lt :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::slice::sort::unstable::quicksort::partition",
                                                            [
                                                              T;
                                                              Ty.function
                                                                [
                                                                  Ty.tuple
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "&")
                                                                        []
                                                                        [ T ];
                                                                      Ty.apply
                                                                        (Ty.path "&")
                                                                        []
                                                                        [ T ]
                                                                    ]
                                                                ]
                                                                (Ty.path "bool")
                                                            ]
                                                          |),
                                                          [
                                                            M.read (| v |);
                                                            M.read (| pivot_pos |);
                                                            M.alloc (|
                                                              M.closure
                                                                (fun γ =>
                                                                  ltac:(M.monadic
                                                                    match γ with
                                                                    | [ α0; α1 ] =>
                                                                      ltac:(M.monadic
                                                                        (M.match_operator (|
                                                                          M.alloc (| α0 |),
                                                                          [
                                                                            fun γ =>
                                                                              ltac:(M.monadic
                                                                                (let a :=
                                                                                  M.copy (| γ |) in
                                                                                M.match_operator (|
                                                                                  M.alloc (| α1 |),
                                                                                  [
                                                                                    fun γ =>
                                                                                      ltac:(M.monadic
                                                                                        (let b :=
                                                                                          M.copy (|
                                                                                            γ
                                                                                          |) in
                                                                                        UnOp.not (|
                                                                                          M.call_closure (|
                                                                                            M.get_trait_method (|
                                                                                              "core::ops::function::FnMut",
                                                                                              F,
                                                                                              [
                                                                                                Ty.tuple
                                                                                                  [
                                                                                                    Ty.apply
                                                                                                      (Ty.path
                                                                                                        "&")
                                                                                                      []
                                                                                                      [
                                                                                                        T
                                                                                                      ];
                                                                                                    Ty.apply
                                                                                                      (Ty.path
                                                                                                        "&")
                                                                                                      []
                                                                                                      [
                                                                                                        T
                                                                                                      ]
                                                                                                  ]
                                                                                              ],
                                                                                              "call_mut",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                is_less
                                                                                              |);
                                                                                              Value.Tuple
                                                                                                [
                                                                                                  M.read (|
                                                                                                    b
                                                                                                  |);
                                                                                                  M.read (|
                                                                                                    a
                                                                                                  |)
                                                                                                ]
                                                                                            ]
                                                                                          |)
                                                                                        |)))
                                                                                  ]
                                                                                |)))
                                                                          ]
                                                                        |)))
                                                                    | _ =>
                                                                      M.impossible
                                                                        "wrong number of arguments"
                                                                    end))
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    let~ mid :=
                                                      M.alloc (|
                                                        BinOp.Wrap.add (|
                                                          M.read (| num_lt |),
                                                          Value.Integer IntegerKind.Usize 1
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    BinOp.gt (|
                                                                      M.read (| mid |),
                                                                      M.read (| index |)
                                                                    |)
                                                                  |)) 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.Tuple [] |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        v,
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::index::IndexMut",
                                                            Ty.apply (Ty.path "slice") [] [ T ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::ops::range::RangeFrom")
                                                                []
                                                                [ Ty.path "usize" ]
                                                            ],
                                                            "index_mut",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| v |);
                                                            Value.StructRecord
                                                              "core::ops::range::RangeFrom"
                                                              [ ("start", M.read (| mid |)) ]
                                                          ]
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        index,
                                                        BinOp.Wrap.sub (|
                                                          M.read (| index |),
                                                          M.read (| mid |)
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        ancestor_pivot,
                                                        Value.StructTuple
                                                          "core::option::Option::None"
                                                          []
                                                      |) in
                                                    M.continue (||)
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ mid :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::slice::sort::unstable::quicksort::partition",
                                    [ T; F ]
                                  |),
                                  [ M.read (| v |); M.read (| pivot_pos |); M.read (| is_less |) ]
                                |)
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ T ],
                                    "split_at_mut",
                                    []
                                  |),
                                  [ M.read (| v |); M.read (| mid |) ]
                                |)
                              |),
                              [
                                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 := M.copy (| γ0_0 |) in
                                    let right := M.copy (| γ0_1 |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "split_at_mut",
                                            []
                                          |),
                                          [ M.read (| right |); Value.Integer IntegerKind.Usize 1 ]
                                        |)
                                      |),
                                      [
                                        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 pivot := M.copy (| γ0_0 |) in
                                            let right := M.copy (| γ0_1 |) in
                                            let~ pivot :=
                                              M.alloc (|
                                                M.SubPointer.get_array_field (|
                                                  M.read (| pivot |),
                                                  M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                |)
                                              |) in
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.lt (|
                                                            M.read (| mid |),
                                                            M.read (| index |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    let~ _ := M.write (| v, M.read (| right |) |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        index,
                                                        BinOp.Wrap.sub (|
                                                          BinOp.Wrap.sub (|
                                                            M.read (| index |),
                                                            M.read (| mid |)
                                                          |),
                                                          Value.Integer IntegerKind.Usize 1
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        ancestor_pivot,
                                                        Value.StructTuple
                                                          "core::option::Option::Some"
                                                          [ M.read (| pivot |) ]
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.gt (|
                                                                    M.read (| mid |),
                                                                    M.read (| index |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            let~ _ :=
                                                              M.write (| v, M.read (| left |) |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (| Value.Tuple [] |)
                                                                |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |)))
                                              ]
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        |)
                      |)
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_partition_at_index_loop :
        M.IsFunction "core::slice::sort::select::partition_at_index_loop" partition_at_index_loop.
      
      (*
      fn min_index<T, F: FnMut(&T, &T) -> bool>(slice: &[T], is_less: &mut F) -> Option<usize> {
          slice
              .iter()
              .enumerate()
              .reduce(|acc, t| if is_less(t.1, acc.1) { t } else { acc })
              .map(|(i, _)| i)
      }
      *)
      Definition min_index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ slice; is_less ] =>
          ltac:(M.monadic
            (let slice := M.alloc (| slice |) in
            let is_less := M.alloc (| is_less |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ] ],
                "map",
                [
                  Ty.path "usize";
                  Ty.function
                    [ Ty.tuple [ Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ] ] ]
                    (Ty.path "usize")
                ]
              |),
              [
                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") [] [ T ] ],
                    [],
                    "reduce",
                    [
                      Ty.function
                        [
                          Ty.tuple
                            [
                              Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ];
                              Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ]
                            ]
                        ]
                        (Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                        [],
                        "enumerate",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "iter",
                            []
                          |),
                          [ M.read (| slice |) ]
                        |)
                      ]
                    |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let acc := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let t := M.copy (| γ |) in
                                              M.read (|
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::function::FnMut",
                                                                  F,
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ T ];
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ T ]
                                                                      ]
                                                                  ],
                                                                  "call_mut",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| is_less |);
                                                                  Value.Tuple
                                                                    [
                                                                      M.read (|
                                                                        M.SubPointer.get_tuple_field (|
                                                                          t,
                                                                          1
                                                                        |)
                                                                      |);
                                                                      M.read (|
                                                                        M.SubPointer.get_tuple_field (|
                                                                          acc,
                                                                          1
                                                                        |)
                                                                      |)
                                                                    ]
                                                                ]
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        t));
                                                    fun γ => ltac:(M.monadic acc)
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α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 i := M.copy (| γ0_0 |) in
                                  M.read (| i |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_min_index : M.IsFunction "core::slice::sort::select::min_index" min_index.
      
      (*
      fn max_index<T, F: FnMut(&T, &T) -> bool>(slice: &[T], is_less: &mut F) -> Option<usize> {
          slice
              .iter()
              .enumerate()
              .reduce(|acc, t| if is_less(acc.1, t.1) { t } else { acc })
              .map(|(i, _)| i)
      }
      *)
      Definition max_index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ slice; is_less ] =>
          ltac:(M.monadic
            (let slice := M.alloc (| slice |) in
            let is_less := M.alloc (| is_less |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ] ],
                "map",
                [
                  Ty.path "usize";
                  Ty.function
                    [ Ty.tuple [ Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ] ] ]
                    (Ty.path "usize")
                ]
              |),
              [
                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") [] [ T ] ],
                    [],
                    "reduce",
                    [
                      Ty.function
                        [
                          Ty.tuple
                            [
                              Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ];
                              Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ]
                            ]
                        ]
                        (Ty.tuple [ Ty.path "usize"; Ty.apply (Ty.path "&") [] [ T ] ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                        [],
                        "enumerate",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "iter",
                            []
                          |),
                          [ M.read (| slice |) ]
                        |)
                      ]
                    |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let acc := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let t := M.copy (| γ |) in
                                              M.read (|
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::function::FnMut",
                                                                  F,
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ T ];
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ T ]
                                                                      ]
                                                                  ],
                                                                  "call_mut",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| is_less |);
                                                                  Value.Tuple
                                                                    [
                                                                      M.read (|
                                                                        M.SubPointer.get_tuple_field (|
                                                                          acc,
                                                                          1
                                                                        |)
                                                                      |);
                                                                      M.read (|
                                                                        M.SubPointer.get_tuple_field (|
                                                                          t,
                                                                          1
                                                                        |)
                                                                      |)
                                                                    ]
                                                                ]
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        t));
                                                    fun γ => ltac:(M.monadic acc)
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α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 i := M.copy (| γ0_0 |) in
                                  M.read (| i |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_max_index : M.IsFunction "core::slice::sort::select::max_index" max_index.
      
      (*
      fn median_of_medians<T, F: FnMut(&T, &T) -> bool>(mut v: &mut [T], is_less: &mut F, mut k: usize) {
          // Since this function isn't public, it should never be called with an out-of-bounds index.
          debug_assert!(k < v.len());
      
          // If T is as ZST, `partition_at_index` will already return early.
          debug_assert!(!T::IS_ZST);
      
          // We now know that `k < v.len() <= isize::MAX`
          loop {
              if v.len() <= INSERTION_SORT_THRESHOLD {
                  if v.len() >= 2 {
                      insertion_sort_shift_left(v, 1, is_less);
                  }
      
                  return;
              }
      
              // `median_of_{minima,maxima}` can't handle the extreme cases of the first/last element,
              // so we catch them here and just do a linear search.
              if k == v.len() - 1 {
                  // Find max element and place it in the last position of the array. We're free to use
                  // `unwrap()` here because we know v must not be empty.
                  let max_idx = max_index(v, is_less).unwrap();
                  v.swap(max_idx, k);
                  return;
              } else if k == 0 {
                  // Find min element and place it in the first position of the array. We're free to use
                  // `unwrap()` here because we know v must not be empty.
                  let min_idx = min_index(v, is_less).unwrap();
                  v.swap(min_idx, k);
                  return;
              }
      
              let p = median_of_ninthers(v, is_less);
      
              if p == k {
                  return;
              } else if p > k {
                  v = &mut v[..p];
              } else {
                  // Since `p < k < v.len()`, `p + 1` doesn't overflow and is
                  // a valid index into the slice.
                  v = &mut v[p + 1..];
                  k -= p + 1;
              }
          }
      }
      *)
      Definition median_of_medians (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ v; is_less; k ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let is_less := M.alloc (| is_less |) in
            let k := M.alloc (| k |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  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.lt (|
                                                M.read (| k |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| v |) ]
                                                |)
                                              |)
                                            |)
                                          |)) 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: k < v.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.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 (|
                                              UnOp.not (|
                                                M.read (|
                                                  M.get_constant (|
                                                    "core::mem::SizedTypeProperties::IS_ZST"
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)) 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: !T::IS_ZST"
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    M.never_to_any (|
                      M.read (|
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.le (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "slice") [] [ T ],
                                                  "len",
                                                  []
                                                |),
                                                [ M.read (| v |) ]
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "core::slice::sort::select::INSERTION_SORT_THRESHOLD"
                                                |)
                                              |)
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.ge (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [ T ],
                                                                  "len",
                                                                  []
                                                                |),
                                                                [ M.read (| v |) ]
                                                              |),
                                                              Value.Integer IntegerKind.Usize 2
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "core::slice::sort::shared::smallsort::insertion_sort_shift_left",
                                                              [ T; F ]
                                                            |),
                                                            [
                                                              M.read (| v |);
                                                              Value.Integer IntegerKind.Usize 1;
                                                              M.read (| is_less |)
                                                            ]
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  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 (|
                                            BinOp.eq (|
                                              M.read (| k |),
                                              BinOp.Wrap.sub (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| v |) ]
                                                |),
                                                Value.Integer IntegerKind.Usize 1
                                              |)
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ max_idx :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [ Ty.path "usize" ],
                                                    "unwrap",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::slice::sort::select::max_index",
                                                        [ T; F ]
                                                      |),
                                                      [ M.read (| v |); M.read (| is_less |) ]
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    "swap",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| v |);
                                                    M.read (| max_idx |);
                                                    M.read (| k |)
                                                  ]
                                                |)
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    BinOp.eq (|
                                                      M.read (| k |),
                                                      Value.Integer IntegerKind.Usize 0
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    let~ min_idx :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "usize" ],
                                                            "unwrap",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_function (|
                                                                "core::slice::sort::select::min_index",
                                                                [ T; F ]
                                                              |),
                                                              [ M.read (| v |); M.read (| is_less |)
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    let~ _ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply (Ty.path "slice") [] [ T ],
                                                            "swap",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| v |);
                                                            M.read (| min_idx |);
                                                            M.read (| k |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.return_ (| Value.Tuple [] |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |)))
                                ]
                              |) in
                            let~ p :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::slice::sort::select::median_of_ninthers",
                                    [ T; F ]
                                  |),
                                  [ M.read (| v |); M.read (| is_less |) ]
                                |)
                              |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (| M.read (| p |), M.read (| k |) |)
                                        |)) 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.Tuple [] |) |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.gt (| M.read (| p |), M.read (| k |) |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                v,
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::index::IndexMut",
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ops::range::RangeTo")
                                                        []
                                                        [ Ty.path "usize" ]
                                                    ],
                                                    "index_mut",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| v |);
                                                    Value.StructRecord
                                                      "core::ops::range::RangeTo"
                                                      [ ("end_", M.read (| p |)) ]
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let~ _ :=
                                              M.write (|
                                                v,
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::index::IndexMut",
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ops::range::RangeFrom")
                                                        []
                                                        [ Ty.path "usize" ]
                                                    ],
                                                    "index_mut",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| v |);
                                                    Value.StructRecord
                                                      "core::ops::range::RangeFrom"
                                                      [
                                                        ("start",
                                                          BinOp.Wrap.add (|
                                                            M.read (| p |),
                                                            Value.Integer IntegerKind.Usize 1
                                                          |))
                                                      ]
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              let β := k in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.sub (|
                                                  M.read (| β |),
                                                  BinOp.Wrap.add (|
                                                    M.read (| p |),
                                                    Value.Integer IntegerKind.Usize 1
                                                  |)
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        |)
                      |)
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_median_of_medians :
        M.IsFunction "core::slice::sort::select::median_of_medians" median_of_medians.
      
      (*
      fn median_of_ninthers<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) -> usize {
          // use `saturating_mul` so the multiplication doesn't overflow on 16-bit platforms.
          let frac = if v.len() <= 1024 {
              v.len() / 12
          } else if v.len() <= 128_usize.saturating_mul(1024) {
              v.len() / 64
          } else {
              v.len() / 1024
          };
      
          let pivot = frac / 2;
          let lo = v.len() / 2 - pivot;
          let hi = frac + lo;
          let gap = (v.len() - 9 * frac) / 4;
          let mut a = lo - 4 * frac - gap;
          let mut b = hi + gap;
          for i in lo..hi {
              ninther(v, is_less, a, i - frac, b, a + 1, i, b + 1, a + 2, i + frac, b + 2);
              a += 3;
              b += 3;
          }
      
          median_of_medians(&mut v[lo..lo + frac], is_less, pivot);
      
          partition(v, lo + pivot, is_less)
      }
      *)
      Definition median_of_ninthers (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ v; is_less ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let is_less := M.alloc (| is_less |) in
            M.read (|
              let~ frac :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.le (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| v |) ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1024
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            BinOp.Wrap.div (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "len",
                                  []
                                |),
                                [ M.read (| v |) ]
                              |),
                              Value.Integer IntegerKind.Usize 12
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.le (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply (Ty.path "slice") [] [ T ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| v |) ]
                                          |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "usize",
                                              "saturating_mul",
                                              []
                                            |),
                                            [
                                              Value.Integer IntegerKind.Usize 128;
                                              Value.Integer IntegerKind.Usize 1024
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    BinOp.Wrap.div (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ T ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| v |) ]
                                      |),
                                      Value.Integer IntegerKind.Usize 64
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    BinOp.Wrap.div (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ T ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| v |) ]
                                      |),
                                      Value.Integer IntegerKind.Usize 1024
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |) in
              let~ pivot :=
                M.alloc (|
                  BinOp.Wrap.div (| M.read (| frac |), Value.Integer IntegerKind.Usize 2 |)
                |) in
              let~ lo :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    BinOp.Wrap.div (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "len",
                          []
                        |),
                        [ M.read (| v |) ]
                      |),
                      Value.Integer IntegerKind.Usize 2
                    |),
                    M.read (| pivot |)
                  |)
                |) in
              let~ hi := M.alloc (| BinOp.Wrap.add (| M.read (| frac |), M.read (| lo |) |) |) in
              let~ gap :=
                M.alloc (|
                  BinOp.Wrap.div (|
                    BinOp.Wrap.sub (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "len",
                          []
                        |),
                        [ M.read (| v |) ]
                      |),
                      BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 9, M.read (| frac |) |)
                    |),
                    Value.Integer IntegerKind.Usize 4
                  |)
                |) in
              let~ a :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    BinOp.Wrap.sub (|
                      M.read (| lo |),
                      BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 4, M.read (| frac |) |)
                    |),
                    M.read (| gap |)
                  |)
                |) in
              let~ b := M.alloc (| BinOp.Wrap.add (| M.read (| hi |), M.read (| gap |) |) |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          Value.StructRecord
                            "core::ops::range::Range"
                            [ ("start", M.read (| lo |)); ("end_", M.read (| hi |)) ]
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let i := M.copy (| γ0_0 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::sort::select::ninther",
                                                [ T; F ]
                                              |),
                                              [
                                                M.read (| v |);
                                                M.read (| is_less |);
                                                M.read (| a |);
                                                BinOp.Wrap.sub (|
                                                  M.read (| i |),
                                                  M.read (| frac |)
                                                |);
                                                M.read (| b |);
                                                BinOp.Wrap.add (|
                                                  M.read (| a |),
                                                  Value.Integer IntegerKind.Usize 1
                                                |);
                                                M.read (| i |);
                                                BinOp.Wrap.add (|
                                                  M.read (| b |),
                                                  Value.Integer IntegerKind.Usize 1
                                                |);
                                                BinOp.Wrap.add (|
                                                  M.read (| a |),
                                                  Value.Integer IntegerKind.Usize 2
                                                |);
                                                BinOp.Wrap.add (|
                                                  M.read (| i |),
                                                  M.read (| frac |)
                                                |);
                                                BinOp.Wrap.add (|
                                                  M.read (| b |),
                                                  Value.Integer IntegerKind.Usize 2
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          let β := a in
                                          M.write (|
                                            β,
                                            BinOp.Wrap.add (|
                                              M.read (| β |),
                                              Value.Integer IntegerKind.Usize 3
                                            |)
                                          |) in
                                        let~ _ :=
                                          let β := b in
                                          M.write (|
                                            β,
                                            BinOp.Wrap.add (|
                                              M.read (| β |),
                                              Value.Integer IntegerKind.Usize 3
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::sort::select::median_of_medians", [ T; F ] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::IndexMut",
                          Ty.apply (Ty.path "slice") [] [ T ],
                          [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                          "index_mut",
                          []
                        |),
                        [
                          M.read (| v |);
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start", M.read (| lo |));
                              ("end_", BinOp.Wrap.add (| M.read (| lo |), M.read (| frac |) |))
                            ]
                        ]
                      |);
                      M.read (| is_less |);
                      M.read (| pivot |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::slice::sort::unstable::quicksort::partition",
                    [ T; F ]
                  |),
                  [
                    M.read (| v |);
                    BinOp.Wrap.add (| M.read (| lo |), M.read (| pivot |) |);
                    M.read (| is_less |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_median_of_ninthers :
        M.IsFunction "core::slice::sort::select::median_of_ninthers" median_of_ninthers.
      
      (*
      fn ninther<T, F: FnMut(&T, &T) -> bool>(
          v: &mut [T],
          is_less: &mut F,
          a: usize,
          mut b: usize,
          c: usize,
          mut d: usize,
          e: usize,
          mut f: usize,
          g: usize,
          mut h: usize,
          i: usize,
      ) {
          b = median_idx(v, is_less, a, b, c);
          h = median_idx(v, is_less, g, h, i);
          if is_less(&v[h], &v[b]) {
              mem::swap(&mut b, &mut h);
          }
          if is_less(&v[f], &v[d]) {
              mem::swap(&mut d, &mut f);
          }
          if is_less(&v[e], &v[d]) {
              // do nothing
          } else if is_less(&v[f], &v[e]) {
              d = f;
          } else {
              if is_less(&v[e], &v[b]) {
                  v.swap(e, b);
              } else if is_less(&v[h], &v[e]) {
                  v.swap(e, h);
              }
              return;
          }
          if is_less(&v[d], &v[b]) {
              d = b;
          } else if is_less(&v[h], &v[d]) {
              d = h;
          }
      
          v.swap(d, e);
      }
      *)
      Definition ninther (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ v; is_less; a; b; c; d; e; f; g; h; i ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let is_less := M.alloc (| is_less |) in
            let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            let c := M.alloc (| c |) in
            let d := M.alloc (| d |) in
            let e := M.alloc (| e |) in
            let f := M.alloc (| f |) in
            let g := M.alloc (| g |) in
            let h := M.alloc (| h |) in
            let i := M.alloc (| i |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.write (|
                      b,
                      M.call_closure (|
                        M.get_function (| "core::slice::sort::select::median_idx", [ T; F ] |),
                        [
                          M.read (| v |);
                          M.read (| is_less |);
                          M.read (| a |);
                          M.read (| b |);
                          M.read (| c |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      h,
                      M.call_closure (|
                        M.get_function (| "core::slice::sort::select::median_idx", [ T; F ] |),
                        [
                          M.read (| v |);
                          M.read (| is_less |);
                          M.read (| g |);
                          M.read (| h |);
                          M.read (| i |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), h |);
                                          M.SubPointer.get_array_field (| M.read (| v |), b |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (| "core::mem::swap", [ Ty.path "usize" ] |),
                                  [ b; h ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        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 (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), f |);
                                          M.SubPointer.get_array_field (| M.read (| v |), d |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (| "core::mem::swap", [ Ty.path "usize" ] |),
                                  [ d; f ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        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 (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), e |);
                                          M.SubPointer.get_array_field (| M.read (| v |), d |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::function::FnMut",
                                              F,
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply (Ty.path "&") [] [ T ];
                                                    Ty.apply (Ty.path "&") [] [ T ]
                                                  ]
                                              ],
                                              "call_mut",
                                              []
                                            |),
                                            [
                                              M.read (| is_less |);
                                              Value.Tuple
                                                [
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| v |),
                                                    f
                                                  |);
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| v |),
                                                    e
                                                  |)
                                                ]
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ := M.write (| d, M.read (| f |) |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::function::FnMut",
                                                              F,
                                                              [
                                                                Ty.tuple
                                                                  [
                                                                    Ty.apply (Ty.path "&") [] [ T ];
                                                                    Ty.apply (Ty.path "&") [] [ T ]
                                                                  ]
                                                              ],
                                                              "call_mut",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| is_less |);
                                                              Value.Tuple
                                                                [
                                                                  M.SubPointer.get_array_field (|
                                                                    M.read (| v |),
                                                                    e
                                                                  |);
                                                                  M.SubPointer.get_array_field (|
                                                                    M.read (| v |),
                                                                    b
                                                                  |)
                                                                ]
                                                            ]
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    let~ _ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply (Ty.path "slice") [] [ T ],
                                                            "swap",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| v |);
                                                            M.read (| e |);
                                                            M.read (| b |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::function::FnMut",
                                                                      F,
                                                                      [
                                                                        Ty.tuple
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path "&")
                                                                              []
                                                                              [ T ];
                                                                            Ty.apply
                                                                              (Ty.path "&")
                                                                              []
                                                                              [ T ]
                                                                          ]
                                                                      ],
                                                                      "call_mut",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (| is_less |);
                                                                      Value.Tuple
                                                                        [
                                                                          M.SubPointer.get_array_field (|
                                                                            M.read (| v |),
                                                                            h
                                                                          |);
                                                                          M.SubPointer.get_array_field (|
                                                                            M.read (| v |),
                                                                            e
                                                                          |)
                                                                        ]
                                                                    ]
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            let~ _ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "slice")
                                                                      []
                                                                      [ T ],
                                                                    "swap",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| v |);
                                                                    M.read (| e |);
                                                                    M.read (| h |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |)))
                                              ]
                                            |) in
                                          M.return_ (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)))
                              ]
                            |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), d |);
                                          M.SubPointer.get_array_field (| M.read (| v |), b |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ := M.write (| d, M.read (| b |) |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::function::FnMut",
                                              F,
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply (Ty.path "&") [] [ T ];
                                                    Ty.apply (Ty.path "&") [] [ T ]
                                                  ]
                                              ],
                                              "call_mut",
                                              []
                                            |),
                                            [
                                              M.read (| is_less |);
                                              Value.Tuple
                                                [
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| v |),
                                                    h
                                                  |);
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| v |),
                                                    d
                                                  |)
                                                ]
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ := M.write (| d, M.read (| h |) |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "swap",
                          []
                        |),
                        [ M.read (| v |); M.read (| d |); M.read (| e |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_ninther : M.IsFunction "core::slice::sort::select::ninther" ninther.
      
      (*
      fn median_idx<T, F: FnMut(&T, &T) -> bool>(
          v: &[T],
          is_less: &mut F,
          mut a: usize,
          b: usize,
          mut c: usize,
      ) -> usize {
          if is_less(&v[c], &v[a]) {
              mem::swap(&mut a, &mut c);
          }
          if is_less(&v[c], &v[b]) {
              return c;
          }
          if is_less(&v[b], &v[a]) {
              return a;
          }
          b
      }
      *)
      Definition median_idx (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ v; is_less; a; b; c ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let is_less := M.alloc (| is_less |) in
            let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            let c := M.alloc (| c |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), c |);
                                          M.SubPointer.get_array_field (| M.read (| v |), a |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (| "core::mem::swap", [ Ty.path "usize" ] |),
                                  [ a; c ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        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 (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), c |);
                                          M.SubPointer.get_array_field (| M.read (| v |), b |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| M.read (| c |) |) |) |)
                            |)));
                        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 (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply (Ty.path "&") [] [ T ];
                                            Ty.apply (Ty.path "&") [] [ T ]
                                          ]
                                      ],
                                      "call_mut",
                                      []
                                    |),
                                    [
                                      M.read (| is_less |);
                                      Value.Tuple
                                        [
                                          M.SubPointer.get_array_field (| M.read (| v |), b |);
                                          M.SubPointer.get_array_field (| M.read (| v |), a |)
                                        ]
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| M.read (| a |) |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  b
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_median_idx : M.IsFunction "core::slice::sort::select::median_idx" median_idx.
    End select.
  End sort.
End slice.
