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

Module collections.
  Module vec_deque.
    Module iter_mut.
      (* StructRecord
        {
          name := "IterMut";
          const_params := [];
          ty_params := [ "T" ];
          fields :=
            [
              ("i1", Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ]);
              ("i2", Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ])
            ];
        } *)
      
      Module Impl_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*
            pub(super) fn new(i1: slice::IterMut<'a, T>, i2: slice::IterMut<'a, T>) -> Self {
                Self { i1, i2 }
            }
        *)
        Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ i1; i2 ] =>
            ltac:(M.monadic
              (let i1 := M.alloc (| i1 |) in
              let i2 := M.alloc (| i2 |) in
              Value.StructRecord
                "alloc::collections::vec_deque::iter_mut::IterMut"
                [ ("i1", M.read (| i1 |)); ("i2", M.read (| i2 |)) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (T : Ty.t),
          M.IsAssociatedFunction (Self T) "new" (new T).
      End Impl_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_tuple("IterMut").field(&self.i1.as_slice()).field(&self.i2.as_slice()).finish()
            }
        *)
        Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::builders::DebugTuple",
                  "finish",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::builders::DebugTuple",
                      "field",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::builders::DebugTuple",
                          "field",
                          []
                        |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Formatter",
                                "debug_tuple",
                                []
                              |),
                              [ M.read (| f |); M.read (| Value.String "IterMut" |) ]
                            |)
                          |);
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                "as_slice",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i1"
                                |)
                              ]
                            |)
                          |)
                        ]
                      |);
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                            "as_slice",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::collections::vec_deque::iter_mut::IterMut",
                              "i2"
                            |)
                          ]
                        |)
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_default_Default_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*
            fn default() -> Self {
                IterMut { i1: Default::default(), i2: Default::default() }
            }
        *)
        Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "alloc::collections::vec_deque::iter_mut::IterMut"
                [
                  ("i1",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("i2",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::default::Default"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method (default T)) ].
      End Impl_core_default_Default_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_traits_iterator_Iterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*     type Item = &'a mut T; *)
        Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
        
        (*
            fn next(&mut self) -> Option<&'a mut T> {
                match self.i1.next() {
                    Some(val) => Some(val),
                    None => {
                        // most of the time, the iterator will either always
                        // call next(), or always call next_back(). By swapping
                        // the iterators once the first one is empty, we ensure
                        // that the first branch is taken as often as possible,
                        // without sacrificing correctness, as i1 is empty anyways
                        mem::swap(&mut self.i1, &mut self.i2);
                        self.i1.next()
                    }
                }
            }
        *)
        Definition next (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "next",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i1"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple "core::option::Option::Some" [ M.read (| val |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::mem::swap",
                                [ Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ] ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i1"
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i2"
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                              [],
                              "next",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::iter_mut::IterMut",
                                "i1"
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                match self.i1.advance_by(n) {
                    Ok(()) => Ok(()),
                    Err(remaining) => {
                        mem::swap(&mut self.i1, &mut self.i2);
                        self.i1.advance_by(remaining.get())
                    }
                }
            }
        *)
        Definition advance_by
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "advance_by",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i1"
                        |);
                        M.read (| n |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::result::Result::Ok",
                            0
                          |) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::result::Result::Err",
                            0
                          |) in
                        let remaining := M.copy (| γ0_0 |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::mem::swap",
                                [ Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ] ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i1"
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i2"
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                              [],
                              "advance_by",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::iter_mut::IterMut",
                                "i1"
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::num::nonzero::NonZero")
                                    []
                                    [ Ty.path "usize" ],
                                  "get",
                                  []
                                |),
                                [ M.read (| remaining |) ]
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                let len = self.len();
                (len, Some(len))
            }
        *)
        Definition size_hint (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::exact_size::ExactSizeIterator",
                        Ty.apply
                          (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut")
                          []
                          [ T ],
                        [],
                        "len",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (| len |);
                      Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<Acc, F>(self, accum: Acc, mut f: F) -> Acc
            where
                F: FnMut(Acc, Self::Item) -> Acc,
            {
                let accum = self.i1.fold(accum, &mut f);
                self.i2.fold(accum, &mut f)
            }
        *)
        Definition fold (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [ Acc; F ], [ self; accum; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let accum := M.alloc (| accum |) in
              let f := M.alloc (| f |) in
              M.read (|
                let~ accum :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "fold",
                        [ Acc; Ty.apply (Ty.path "&mut") [] [ F ] ]
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "alloc::collections::vec_deque::iter_mut::IterMut",
                            "i1"
                          |)
                        |);
                        M.read (| accum |);
                        f
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      [],
                      "fold",
                      [ Acc; Ty.apply (Ty.path "&mut") [] [ F ] ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i2"
                        |)
                      |);
                      M.read (| accum |);
                      f
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<B, F, R>(&mut self, init: B, mut f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                let acc = self.i1.try_fold(init, &mut f)?;
                self.i2.try_fold(acc, &mut f)
            }
        *)
        Definition try_fold (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [ B; F; R ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ acc :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                R,
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                    [],
                                    "try_fold",
                                    [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::vec_deque::iter_mut::IterMut",
                                      "i1"
                                    |);
                                    M.read (| init |);
                                    f
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            R,
                                            [ Ty.associated ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                          [],
                          "try_fold",
                          [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::collections::vec_deque::iter_mut::IterMut",
                            "i2"
                          |);
                          M.read (| acc |);
                          f
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(mut self) -> Option<&'a mut T> {
                self.next_back()
            }
        *)
        Definition last (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ],
                  [],
                  "next_back",
                  []
                |),
                [ self ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                // Safety: The TrustedRandomAccess contract requires that callers only pass an index
                // that is in bounds.
                unsafe {
                    let i1_len = self.i1.len();
                    if idx < i1_len {
                        self.i1.__iterator_get_unchecked(idx)
                    } else {
                        self.i2.__iterator_get_unchecked(idx - i1_len)
                    }
                }
            }
        *)
        Definition __iterator_get_unchecked
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self; idx ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let idx := M.alloc (| idx |) in
              M.read (|
                let~ i1_len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::exact_size::ExactSizeIterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "len",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i1"
                        |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.lt (| M.read (| idx |), M.read (| i1_len |) |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                  [],
                                  "__iterator_get_unchecked",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::collections::vec_deque::iter_mut::IterMut",
                                    "i1"
                                  |);
                                  M.read (| idx |)
                                ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                  [],
                                  "__iterator_get_unchecked",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::collections::vec_deque::iter_mut::IterMut",
                                    "i2"
                                  |);
                                  BinOp.Wrap.sub (| M.read (| idx |), M.read (| i1_len |) |)
                                ]
                              |)
                            |)))
                      ]
                    |)
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item T));
              ("next", InstanceField.Method (next T));
              ("advance_by", InstanceField.Method (advance_by T));
              ("size_hint", InstanceField.Method (size_hint T));
              ("fold", InstanceField.Method (fold T));
              ("try_fold", InstanceField.Method (try_fold T));
              ("last", InstanceField.Method (last T));
              ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked T))
            ].
      End Impl_core_iter_traits_iterator_Iterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*
            fn next_back(&mut self) -> Option<&'a mut T> {
                match self.i2.next_back() {
                    Some(val) => Some(val),
                    None => {
                        // most of the time, the iterator will either always
                        // call next(), or always call next_back(). By swapping
                        // the iterators once the first one is empty, we ensure
                        // that the first branch is taken as often as possible,
                        // without sacrificing correctness, as i2 is empty anyways
                        mem::swap(&mut self.i1, &mut self.i2);
                        self.i2.next_back()
                    }
                }
            }
        *)
        Definition next_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::double_ended::DoubleEndedIterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "next_back",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i2"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple "core::option::Option::Some" [ M.read (| val |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::mem::swap",
                                [ Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ] ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i1"
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i2"
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::double_ended::DoubleEndedIterator",
                              Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                              [],
                              "next_back",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::iter_mut::IterMut",
                                "i2"
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                match self.i2.advance_back_by(n) {
                    Ok(()) => Ok(()),
                    Err(remaining) => {
                        mem::swap(&mut self.i1, &mut self.i2);
                        self.i2.advance_back_by(remaining.get())
                    }
                }
            }
        *)
        Definition advance_back_by
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::double_ended::DoubleEndedIterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "advance_back_by",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i2"
                        |);
                        M.read (| n |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::result::Result::Ok",
                            0
                          |) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::result::Result::Err",
                            0
                          |) in
                        let remaining := M.copy (| γ0_0 |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::mem::swap",
                                [ Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ] ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i1"
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::iter_mut::IterMut",
                                  "i2"
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::double_ended::DoubleEndedIterator",
                              Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                              [],
                              "advance_back_by",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::iter_mut::IterMut",
                                "i2"
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::num::nonzero::NonZero")
                                    []
                                    [ Ty.path "usize" ],
                                  "get",
                                  []
                                |),
                                [ M.read (| remaining |) ]
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<Acc, F>(self, accum: Acc, mut f: F) -> Acc
            where
                F: FnMut(Acc, Self::Item) -> Acc,
            {
                let accum = self.i2.rfold(accum, &mut f);
                self.i1.rfold(accum, &mut f)
            }
        *)
        Definition rfold (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [ Acc; F ], [ self; accum; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let accum := M.alloc (| accum |) in
              let f := M.alloc (| f |) in
              M.read (|
                let~ accum :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::double_ended::DoubleEndedIterator",
                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                        [],
                        "rfold",
                        [ Acc; Ty.apply (Ty.path "&mut") [] [ F ] ]
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "alloc::collections::vec_deque::iter_mut::IterMut",
                            "i2"
                          |)
                        |);
                        M.read (| accum |);
                        f
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      [],
                      "rfold",
                      [ Acc; Ty.apply (Ty.path "&mut") [] [ F ] ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "alloc::collections::vec_deque::iter_mut::IterMut",
                          "i1"
                        |)
                      |);
                      M.read (| accum |);
                      f
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<B, F, R>(&mut self, init: B, mut f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                let acc = self.i2.try_rfold(init, &mut f)?;
                self.i1.try_rfold(acc, &mut f)
            }
        *)
        Definition try_rfold (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [ B; F; R ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ acc :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                R,
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::double_ended::DoubleEndedIterator",
                                    Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                    [],
                                    "try_rfold",
                                    [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::vec_deque::iter_mut::IterMut",
                                      "i2"
                                    |);
                                    M.read (| init |);
                                    f
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            R,
                                            [ Ty.associated ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::double_ended::DoubleEndedIterator",
                          Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                          [],
                          "try_rfold",
                          [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::collections::vec_deque::iter_mut::IterMut",
                            "i1"
                          |);
                          M.read (| acc |);
                          f
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("next_back", InstanceField.Method (next_back T));
              ("advance_back_by", InstanceField.Method (advance_back_by T));
              ("rfold", InstanceField.Method (rfold T));
              ("try_rfold", InstanceField.Method (try_rfold T))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*
            fn len(&self) -> usize {
                self.i1.len() + self.i2.len()
            }
        *)
        Definition len (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              BinOp.Wrap.add (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::exact_size::ExactSizeIterator",
                    Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                    [],
                    "len",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::collections::vec_deque::iter_mut::IterMut",
                      "i1"
                    |)
                  ]
                |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::exact_size::ExactSizeIterator",
                    Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                    [],
                    "len",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::collections::vec_deque::iter_mut::IterMut",
                      "i2"
                    |)
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn is_empty(&self) -> bool {
                self.i1.is_empty() && self.i2.is_empty()
            }
        *)
        Definition is_empty (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              LogicalOp.and (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::exact_size::ExactSizeIterator",
                    Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                    [],
                    "is_empty",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::collections::vec_deque::iter_mut::IterMut",
                      "i1"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::exact_size::ExactSizeIterator",
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      [],
                      "is_empty",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::vec_deque::iter_mut::IterMut",
                        "i2"
                      |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("len", InstanceField.Method (len T)); ("is_empty", InstanceField.Method (is_empty T))
            ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_traits_marker_FusedIterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_traits_marker_TrustedLen_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccess_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccess"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_adapters_zip_TrustedRandomAccess_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::iter_mut::IterMut") [] [ T ].
        
        (*     const MAY_HAVE_SIDE_EFFECT: bool = false; *)
        (* Ty.path "bool" *)
        Definition value_MAY_HAVE_SIDE_EFFECT (T : Ty.t) : Value.t :=
          let Self : Ty.t := Self T in
          M.run ltac:(M.monadic (M.alloc (| Value.Bool false |))).
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccessNoCoerce"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("value_MAY_HAVE_SIDE_EFFECT", InstanceField.Constant (value_MAY_HAVE_SIDE_EFFECT T))
            ].
      End Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_for_alloc_collections_vec_deque_iter_mut_IterMut_T.
    End iter_mut.
  End vec_deque.
End collections.
