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

Module iter.
  Module traits.
    Module iterator.
      (* fn _assert_is_object_safe(_: &dyn Iterator<Item = ()>) {} *)
      Definition _assert_is_object_safe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ β0 ] =>
          ltac:(M.monadic
            (let β0 := M.alloc (| β0 |) in
            M.match_operator (| β0, [ fun γ => ltac:(M.monadic (Value.Tuple [])) ] |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function__assert_is_object_safe :
        M.IsFunction "core::iter::traits::iterator::_assert_is_object_safe" _assert_is_object_safe.
      
      (* Trait *)
      Module Iterator.
        Definition next_chunk
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [ N ], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_function (| "core::array::iter_next_chunk", [ Ty.associated; Self ] |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_next_chunk :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "next_chunk" next_chunk.
        Definition size_hint
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.Tuple
                [
                  Value.Integer IntegerKind.Usize 0;
                  Value.StructTuple "core::option::Option::None" []
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_size_hint :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "size_hint" size_hint.
        Definition count (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "fold",
                  [
                    Ty.path "usize";
                    Ty.function [ Ty.tuple [ Ty.path "usize"; Ty.associated ] ] (Ty.path "usize")
                  ]
                |),
                [
                  M.read (| self |);
                  Value.Integer IntegerKind.Usize 0;
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0; α1 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let count := M.copy (| γ |) in
                                    M.match_operator (|
                                      M.alloc (| α1 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (BinOp.Wrap.add (|
                                              M.read (| count |),
                                              Value.Integer IntegerKind.Usize 1
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_count :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "count" count.
        Definition last (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "fold",
                  [
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ];
                    Ty.function
                      [
                        Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ];
                        Ty.associated
                      ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.read (| self |);
                  Value.StructTuple "core::option::Option::None" [];
                  M.get_associated_function (| Self, "some.last", [] |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_last :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "last" last.
        Definition advance_by
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                Value.StructRecord
                                  "core::ops::range::Range"
                                  [
                                    ("start", Value.Integer IntegerKind.Usize 0);
                                    ("end_", M.read (| n |))
                                  ]
                              ]
                            |)
                          |),
                          [
                            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
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [ Ty.associated ],
                                                                "is_none",
                                                                []
                                                              |),
                                                              [
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::iter::traits::iterator::Iterator",
                                                                      Self,
                                                                      [],
                                                                      "next",
                                                                      []
                                                                    |),
                                                                    [ M.read (| self |) ]
                                                                  |)
                                                                |)
                                                              ]
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              Value.StructTuple
                                                                "core::result::Result::Err"
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::num::nonzero::NonZero")
                                                                        []
                                                                        [ Ty.path "usize" ],
                                                                      "new_unchecked",
                                                                      []
                                                                    |),
                                                                    [
                                                                      BinOp.Wrap.sub (|
                                                                        M.read (| n |),
                                                                        M.read (| i |)
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_advance_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "advance_by" advance_by.
        Definition nth (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.tuple [] ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [
                                      Ty.tuple [];
                                      Ty.apply
                                        (Ty.path "core::num::nonzero::NonZero")
                                        []
                                        [ Ty.path "usize" ]
                                    ],
                                  "ok",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Self,
                                      [],
                                      "advance_by",
                                      []
                                    |),
                                    [ M.read (| self |); M.read (| n |) ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.associated ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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",
                          Self,
                          [],
                          "next",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_nth :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "nth" nth.
        Definition step_by
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; step ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let step := M.alloc (| step |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::step_by::StepBy") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| step |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_step_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "step_by" step_by.
        Definition chain (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ U ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::iter::adapters::chain::Chain")
                    []
                    [ Self; Ty.associated ],
                  "new",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      U,
                      [],
                      "into_iter",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_chain :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "chain" chain.
        Definition zip (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ U ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::zip::Zip") [] [ Self; Ty.associated ],
                  "new",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      U,
                      [],
                      "into_iter",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_zip :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "zip" zip.
        Definition intersperse
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; separator ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let separator := M.alloc (| separator |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::intersperse::Intersperse") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| separator |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_intersperse :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "intersperse" intersperse.
        Definition intersperse_with
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ G ], [ self; separator ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let separator := M.alloc (| separator |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::iter::adapters::intersperse::IntersperseWith")
                    []
                    [ Self; G ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| separator |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_intersperse_with :
          M.IsProvidedMethod
            "core::iter::traits::iterator::Iterator"
            "intersperse_with"
            intersperse_with.
        Definition map (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ B; F ], [ 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.apply (Ty.path "core::iter::adapters::map::Map") [] [ Self; F ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_map :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "map" map.
        Definition for_each
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "fold",
                        [ Ty.tuple []; Ty.associated ]
                      |),
                      [
                        M.read (| self |);
                        Value.Tuple [];
                        M.call_closure (|
                          M.get_associated_function (| Self, "call.for_each", [] |),
                          [ M.read (| f |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_for_each :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "for_each" for_each.
        Definition filter (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::filter::Filter") [] [ Self; P ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| predicate |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_filter :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "filter" filter.
        Definition filter_map
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B; F ], [ 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.apply (Ty.path "core::iter::adapters::filter_map::FilterMap") [] [ Self; F ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_filter_map :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "filter_map" filter_map.
        Definition enumerate
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_enumerate :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "enumerate" enumerate.
        Definition peekable
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_peekable :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "peekable" peekable.
        Definition skip_while
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::skip_while::SkipWhile") [] [ Self; P ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| predicate |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_skip_while :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "skip_while" skip_while.
        Definition take_while
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::take_while::TakeWhile") [] [ Self; P ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| predicate |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_take_while :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "take_while" take_while.
        Definition map_while
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B; P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::map_while::MapWhile") [] [ Self; P ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| predicate |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_map_while :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "map_while" map_while.
        Definition skip (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::skip::Skip") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_skip :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "skip" skip.
        Definition take (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::take::Take") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_take :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "take" take.
        Definition scan (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ St; B; F ], [ self; initial_state; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let initial_state := M.alloc (| initial_state |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::scan::Scan") [] [ Self; St; F ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| initial_state |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_scan :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "scan" scan.
        Definition flat_map
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ U; F ], [ 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.apply (Ty.path "core::iter::adapters::flatten::FlatMap") [] [ Self; U; F ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_flat_map :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "flat_map" flat_map.
        Definition flatten
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::flatten::Flatten") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_flatten :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "flatten" flatten.
        Definition map_windows
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [ N ], [ F; R ], [ 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.apply
                    (Ty.path "core::iter::adapters::map_windows::MapWindows")
                    [ N ]
                    [ Self; F ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_map_windows :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "map_windows" map_windows.
        Definition fuse (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_fuse :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "fuse" fuse.
        Definition inspect
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ F ], [ 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.apply (Ty.path "core::iter::adapters::inspect::Inspect") [] [ Self; F ],
                  "new",
                  []
                |),
                [ M.read (| self |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_inspect :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "inspect" inspect.
        Definition by_ref (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (| self |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_by_ref :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "by_ref" by_ref.
        Definition collect
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::collect::FromIterator",
                  B,
                  [ Ty.associated ],
                  "from_iter",
                  [ Self ]
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_collect :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "collect" collect.
        Definition try_collect
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::try_process",
                  [
                    Ty.apply (Ty.path "core::iter::adapters::by_ref_sized::ByRefSized") [] [ Self ];
                    Ty.associated;
                    Ty.associated;
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "core::iter::adapters::GenericShunt")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::iter::adapters::by_ref_sized::ByRefSized")
                                  []
                                  [ Self ];
                                Ty.associated
                              ]
                          ]
                      ]
                      B;
                    B
                  ]
                |),
                [
                  Value.StructTuple
                    "core::iter::adapters::by_ref_sized::ByRefSized"
                    [ M.read (| self |) ];
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let i := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::GenericShunt")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path
                                                "core::iter::adapters::by_ref_sized::ByRefSized")
                                              []
                                              [ Self ];
                                            Ty.associated
                                          ],
                                        [],
                                        "collect",
                                        [ B ]
                                      |),
                                      [ M.read (| i |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_try_collect :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "try_collect" try_collect.
        Definition collect_into
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ E ], [ self; collection ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let collection := M.alloc (| collection |) in
              M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::Extend",
                        E,
                        [ Ty.associated ],
                        "extend",
                        [ Self ]
                      |),
                      [ M.read (| collection |); M.read (| self |) ]
                    |)
                  |) in
                M.alloc (| M.read (| collection |) |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_collect_into :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "collect_into" collect_into.
        Definition partition
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B; F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.read (|
                let~ left :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (| "core::default::Default", B, [], "default", [] |),
                      []
                    |)
                  |) in
                let~ right :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (| "core::default::Default", B, [], "default", [] |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "fold",
                        [ Ty.tuple []; Ty.associated ]
                      |),
                      [
                        M.read (| self |);
                        Value.Tuple [];
                        M.call_closure (|
                          M.get_associated_function (| Self, "extend.partition", [] |),
                          [ M.read (| f |); left; right ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [ M.read (| left |); M.read (| right |) ] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_partition :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "partition" partition.
        Definition partition_in_place
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ T; P ], [ self; β1 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let β1 := M.alloc (| β1 |) in
              M.match_operator (|
                β1,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let predicate := M.alloc (| γ |) in
                      M.read (|
                        let~ true_count := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                        let~ _ :=
                          M.loop (|
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Self,
                                              [],
                                              "find",
                                              [ Ty.associated ]
                                            |),
                                            [
                                              self;
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Self,
                                                  "is_false.partition_in_place",
                                                  []
                                                |),
                                                [ M.read (| predicate |); true_count ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let head := M.copy (| γ0_0 |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::double_ended::DoubleEndedIterator",
                                                      Self,
                                                      [],
                                                      "rfind",
                                                      [ Ty.associated ]
                                                    |),
                                                    [
                                                      self;
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Self,
                                                          "is_true.partition_in_place",
                                                          []
                                                        |),
                                                        [ M.read (| predicate |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let tail := M.copy (| γ0_0 |) in
                                              let~ _ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (| "core::mem::swap", [ T ] |),
                                                    [ M.read (| head |); M.read (| tail |) ]
                                                  |)
                                                |) in
                                              let~ _ :=
                                                let β := true_count in
                                                M.write (|
                                                  β,
                                                  BinOp.Wrap.add (|
                                                    M.read (| β |),
                                                    Value.Integer IntegerKind.Usize 1
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)))
                                        ]
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)))
                          |) in
                        true_count
                      |)))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_partition_in_place :
          M.IsProvidedMethod
            "core::iter::traits::iterator::Iterator"
            "partition_in_place"
            partition_in_place.
        Definition is_partitioned
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              LogicalOp.or (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Self,
                    [],
                    "all",
                    [ Ty.apply (Ty.path "&mut") [] [ P ] ]
                  |),
                  [ self; predicate ]
                |),
                ltac:(M.monadic
                  (UnOp.not (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "any",
                        [ P ]
                      |),
                      [ self; M.read (| predicate |) ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_is_partitioned :
          M.IsProvidedMethod
            "core::iter::traits::iterator::Iterator"
            "is_partitioned"
            is_partitioned.
        Definition try_fold
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          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~ accum := M.copy (| init |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Self,
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let x := M.copy (| γ0_0 |) in
                                  let~ _ :=
                                    M.write (|
                                      accum,
                                      M.read (|
                                        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::ops::function::FnMut",
                                                    F,
                                                    [ Ty.tuple [ B; Ty.associated ] ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [
                                                    f;
                                                    Value.Tuple
                                                      [ M.read (| accum |); M.read (| x |) ]
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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 (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| accum |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_try_fold :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "try_fold" try_fold.
        Definition try_for_each
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ F; R ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "try_fold",
                  [ Ty.tuple []; Ty.associated; R ]
                |),
                [
                  M.read (| self |);
                  Value.Tuple [];
                  M.call_closure (|
                    M.get_associated_function (| Self, "call.try_for_each", [] |),
                    [ M.read (| f |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_try_for_each :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "try_for_each" try_for_each.
        Definition fold (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ B; F ], [ 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.read (|
                let~ accum := M.copy (| init |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Self,
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let x := M.copy (| γ0_0 |) in
                              let~ _ :=
                                M.write (|
                                  accum,
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [ Ty.tuple [ B; Ty.associated ] ],
                                      "call_mut",
                                      []
                                    |),
                                    [ f; Value.Tuple [ M.read (| accum |); M.read (| x |) ] ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) in
                accum
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_fold :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "fold" fold.
        Definition reduce (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ first :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Self,
                                    [],
                                    "next",
                                    []
                                  |),
                                  [ self ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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 (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Self,
                              [],
                              "fold",
                              [ Ty.associated; F ]
                            |),
                            [ M.read (| self |); M.read (| first |); M.read (| f |) ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_reduce :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "reduce" reduce.
        Definition try_reduce
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ R; impl_FnMut_Self_Item__Self_Item__arrow_R ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ first :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Self,
                                [],
                                "next",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |),
                          [
                            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
                                i));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::Try",
                                            Ty.associated,
                                            [],
                                            "from_output",
                                            []
                                          |),
                                          [ Value.StructTuple "core::option::Option::None" [] ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)
                      |) in
                    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",
                                Self,
                                [],
                                "try_fold",
                                [ Ty.associated; impl_FnMut_Self_Item__Self_Item__arrow_R; R ]
                              |),
                              [ M.read (| self |); M.read (| first |); M.read (| f |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let r := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::FromResidual",
                                  Ty.associated,
                                  [ Ty.associated ],
                                  "from_residual",
                                  []
                                |),
                                [ M.read (| r |) ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let i := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.associated,
                                  [],
                                  "from_output",
                                  []
                                |),
                                [ Value.StructTuple "core::option::Option::Some" [ M.read (| i |) ]
                                ]
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_try_reduce :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "try_reduce" try_reduce.
        Definition all (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "core::ops::control_flow::ControlFlow")
                    []
                    [ Ty.tuple []; Ty.tuple [] ],
                  [
                    Ty.apply
                      (Ty.path "core::ops::control_flow::ControlFlow")
                      []
                      [ Ty.tuple []; Ty.tuple [] ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "try_fold",
                        [
                          Ty.tuple [];
                          Ty.associated;
                          Ty.apply
                            (Ty.path "core::ops::control_flow::ControlFlow")
                            []
                            [ Ty.tuple []; Ty.tuple [] ]
                        ]
                      |),
                      [
                        M.read (| self |);
                        Value.Tuple [];
                        M.call_closure (|
                          M.get_associated_function (| Self, "check.all", [] |),
                          [ M.read (| f |) ]
                        |)
                      ]
                    |)
                  |);
                  M.alloc (|
                    Value.StructTuple
                      "core::ops::control_flow::ControlFlow::Continue"
                      [ Value.Tuple [] ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_all :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "all" all.
        Definition any (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "core::ops::control_flow::ControlFlow")
                    []
                    [ Ty.tuple []; Ty.tuple [] ],
                  [
                    Ty.apply
                      (Ty.path "core::ops::control_flow::ControlFlow")
                      []
                      [ Ty.tuple []; Ty.tuple [] ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "try_fold",
                        [
                          Ty.tuple [];
                          Ty.associated;
                          Ty.apply
                            (Ty.path "core::ops::control_flow::ControlFlow")
                            []
                            [ Ty.tuple []; Ty.tuple [] ]
                        ]
                      |),
                      [
                        M.read (| self |);
                        Value.Tuple [];
                        M.call_closure (|
                          M.get_associated_function (| Self, "check.any", [] |),
                          [ M.read (| f |) ]
                        |)
                      ]
                    |)
                  |);
                  M.alloc (|
                    Value.StructTuple
                      "core::ops::control_flow::ControlFlow::Break"
                      [ Value.Tuple [] ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_any :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "any" any.
        Definition find (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::ops::control_flow::ControlFlow")
                    []
                    [ Ty.associated; Ty.tuple [] ],
                  "break_value",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Self,
                      [],
                      "try_fold",
                      [
                        Ty.tuple [];
                        Ty.associated;
                        Ty.apply
                          (Ty.path "core::ops::control_flow::ControlFlow")
                          []
                          [ Ty.associated; Ty.tuple [] ]
                      ]
                    |),
                    [
                      M.read (| self |);
                      Value.Tuple [];
                      M.call_closure (|
                        M.get_associated_function (| Self, "check.find", [] |),
                        [ M.read (| predicate |) ]
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_find :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "find" find.
        Definition find_map
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B; F ], [ 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.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; Ty.tuple [] ],
                  "break_value",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Self,
                      [],
                      "try_fold",
                      [
                        Ty.tuple [];
                        Ty.associated;
                        Ty.apply
                          (Ty.path "core::ops::control_flow::ControlFlow")
                          []
                          [ B; Ty.tuple [] ]
                      ]
                    |),
                    [
                      M.read (| self |);
                      Value.Tuple [];
                      M.call_closure (|
                        M.get_associated_function (| Self, "check.find_map", [] |),
                        [ M.read (| f |) ]
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_find_map :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "find_map" find_map.
        Definition try_find
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ R; impl_FnMut__Self_Item__arrow_R ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "try_fold",
                        [
                          Ty.tuple [];
                          Ty.associated;
                          Ty.apply
                            (Ty.path "core::ops::control_flow::ControlFlow")
                            []
                            [ Ty.associated; Ty.tuple [] ]
                        ]
                      |),
                      [
                        M.read (| self |);
                        Value.Tuple [];
                        M.call_closure (|
                          M.get_associated_function (| Self, "check.try_find", [] |),
                          [ M.read (| f |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let x := M.copy (| γ0_0 |) in
                        x));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.associated,
                              [],
                              "from_output",
                              []
                            |),
                            [ Value.StructTuple "core::option::Option::None" [] ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_try_find :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "try_find" try_find.
        Definition position
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.read (|
                let~ acc := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::ops::control_flow::ControlFlow")
                        []
                        [ Ty.path "usize"; Ty.tuple [] ],
                      "break_value",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Self,
                          [],
                          "try_fold",
                          [
                            Ty.tuple [];
                            Ty.associated;
                            Ty.apply
                              (Ty.path "core::ops::control_flow::ControlFlow")
                              []
                              [ Ty.path "usize"; Ty.tuple [] ]
                          ]
                        |),
                        [
                          M.read (| self |);
                          Value.Tuple [];
                          M.call_closure (|
                            M.get_associated_function (| Self, "check.position", [] |),
                            [ M.read (| predicate |); acc ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_position :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "position" position.
        Definition rposition
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.read (|
                let~ n :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::exact_size::ExactSizeIterator",
                        Ty.apply (Ty.path "&mut") [] [ Self ],
                        [],
                        "len",
                        []
                      |),
                      [ self ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::ops::control_flow::ControlFlow")
                        []
                        [ Ty.path "usize"; Ty.path "usize" ],
                      "break_value",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::double_ended::DoubleEndedIterator",
                          Self,
                          [],
                          "try_rfold",
                          [
                            Ty.path "usize";
                            Ty.associated;
                            Ty.apply
                              (Ty.path "core::ops::control_flow::ControlFlow")
                              []
                              [ Ty.path "usize"; Ty.path "usize" ]
                          ]
                        |),
                        [
                          M.read (| self |);
                          M.read (| n |);
                          M.call_closure (|
                            M.get_associated_function (| Self, "check.rposition", [] |),
                            [ M.read (| predicate |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_rposition :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "rposition" rposition.
        Definition max (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "max_by",
                  [
                    Ty.function
                      [
                        Ty.apply (Ty.path "&") [] [ Ty.associated ];
                        Ty.apply (Ty.path "&") [] [ Ty.associated ]
                      ]
                      (Ty.path "core::cmp::Ordering")
                  ]
                |),
                [
                  M.read (| self |);
                  M.get_trait_method (| "core::cmp::Ord", Ty.associated, [], "cmp", [] |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_max :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "max" max.
        Definition min (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "min_by",
                  [
                    Ty.function
                      [
                        Ty.apply (Ty.path "&") [] [ Ty.associated ];
                        Ty.apply (Ty.path "&") [] [ Ty.associated ]
                      ]
                      (Ty.path "core::cmp::Ordering")
                  ]
                |),
                [
                  M.read (| self |);
                  M.get_trait_method (| "core::cmp::Ord", Ty.associated, [], "cmp", [] |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_min :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "min" min.
        Definition max_by_key
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B; F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.tuple [ B; Ty.associated ] ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::iter::adapters::map::Map")
                                    []
                                    [ Self; Ty.associated ],
                                  [],
                                  "max_by",
                                  [
                                    Ty.function
                                      [
                                        Ty.apply (Ty.path "&") [] [ Ty.tuple [ B; Ty.associated ] ];
                                        Ty.apply (Ty.path "&") [] [ Ty.tuple [ B; Ty.associated ] ]
                                      ]
                                      (Ty.path "core::cmp::Ordering")
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Self,
                                      [],
                                      "map",
                                      [ Ty.tuple [ B; Ty.associated ]; Ty.associated ]
                                    |),
                                    [
                                      M.read (| self |);
                                      M.call_closure (|
                                        M.get_associated_function (| Self, "key.max_by_key", [] |),
                                        [ M.read (| f |) ]
                                      |)
                                    ]
                                  |);
                                  M.get_associated_function (| Self, "compare.max_by_key", [] |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.associated ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |),
                      [
                        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 x := M.copy (| γ0_1 |) in
                            M.alloc (|
                              Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ]
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_max_by_key :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "max_by_key" max_by_key.
        Definition max_by (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self; compare ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let compare := M.alloc (| compare |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "reduce",
                  [ Ty.associated ]
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_associated_function (| Self, "fold.max_by", [] |),
                    [ M.read (| compare |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_max_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "max_by" max_by.
        Definition min_by_key
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ B; F ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.tuple [ B; Ty.associated ] ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::iter::adapters::map::Map")
                                    []
                                    [ Self; Ty.associated ],
                                  [],
                                  "min_by",
                                  [
                                    Ty.function
                                      [
                                        Ty.apply (Ty.path "&") [] [ Ty.tuple [ B; Ty.associated ] ];
                                        Ty.apply (Ty.path "&") [] [ Ty.tuple [ B; Ty.associated ] ]
                                      ]
                                      (Ty.path "core::cmp::Ordering")
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Self,
                                      [],
                                      "map",
                                      [ Ty.tuple [ B; Ty.associated ]; Ty.associated ]
                                    |),
                                    [
                                      M.read (| self |);
                                      M.call_closure (|
                                        M.get_associated_function (| Self, "key.min_by_key", [] |),
                                        [ M.read (| f |) ]
                                      |)
                                    ]
                                  |);
                                  M.get_associated_function (| Self, "compare.min_by_key", [] |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.associated ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "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))
                        ]
                      |),
                      [
                        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 x := M.copy (| γ0_1 |) in
                            M.alloc (|
                              Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ]
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_min_by_key :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "min_by_key" min_by_key.
        Definition min_by (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self; compare ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let compare := M.alloc (| compare |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "reduce",
                  [ Ty.associated ]
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_associated_function (| Self, "fold.min_by", [] |),
                    [ M.read (| compare |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_min_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "min_by" min_by.
        Definition rev (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_rev :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "rev" rev.
        Definition unzip (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ A; B; FromA; FromB ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ unzipped :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.tuple [ FromA; FromB ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::Extend",
                        Ty.tuple [ FromA; FromB ],
                        [ Ty.tuple [ A; B ] ],
                        "extend",
                        [ Self ]
                      |),
                      [ unzipped; M.read (| self |) ]
                    |)
                  |) in
                unzipped
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_unzip :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "unzip" unzip.
        Definition copied (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_copied :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "copied" copied.
        Definition cloned (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::cloned::Cloned") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_cloned :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "cloned" cloned.
        Definition cycle (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::cycle::Cycle") [] [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_cycle :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "cycle" cycle.
        Definition array_chunks
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [ N ], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::iter::adapters::array_chunks::ArrayChunks")
                    [ N ]
                    [ Self ],
                  "new",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_array_chunks :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "array_chunks" array_chunks.
        Definition sum (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as S ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::accum::Sum",
                  S,
                  [ Ty.associated ],
                  "sum",
                  [ Self ]
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_sum :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "sum" sum.
        Definition product
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ P ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::accum::Product",
                  P,
                  [ Ty.associated ],
                  "product",
                  [ Self ]
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_product :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "product" product.
        Definition cmp (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "cmp_by",
                  [
                    I;
                    Ty.function
                      [ Ty.tuple [ Ty.associated; Ty.associated ] ]
                      (Ty.path "core::cmp::Ordering")
                  ]
                |),
                [
                  M.read (| self |);
                  M.read (| other |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0; α1 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let x := M.copy (| γ |) in
                                    M.match_operator (|
                                      M.alloc (| α1 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let y := M.copy (| γ |) in
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::Ord",
                                                Ty.associated,
                                                [],
                                                "cmp",
                                                []
                                              |),
                                              [ x; y ]
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_cmp :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "cmp" cmp.
        Definition cmp_by (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I; F ], [ self; other; cmp ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              let cmp := M.alloc (| cmp |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::iter::traits::iterator::iter_compare",
                        [ Self; Ty.associated; Ty.associated; Ty.path "core::cmp::Ordering" ]
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            I,
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| other |) ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (| Self, "compare.cmp_by", [] |),
                          [ M.read (| cmp |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let ord := M.copy (| γ0_0 |) in
                        ord));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let ord := M.copy (| γ0_0 |) in
                        ord))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_cmp_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "cmp_by" cmp_by.
        Definition partial_cmp
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "partial_cmp_by",
                  [
                    I;
                    Ty.function
                      [ Ty.tuple [ Ty.associated; Ty.associated ] ]
                      (Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "core::cmp::Ordering" ])
                  ]
                |),
                [
                  M.read (| self |);
                  M.read (| other |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0; α1 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let x := M.copy (| γ |) in
                                    M.match_operator (|
                                      M.alloc (| α1 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let y := M.copy (| γ |) in
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialOrd",
                                                Ty.associated,
                                                [ Ty.associated ],
                                                "partial_cmp",
                                                []
                                              |),
                                              [ x; y ]
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_partial_cmp :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "partial_cmp" partial_cmp.
        Definition partial_cmp_by
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ _ as I; F ], [ self; other; partial_cmp ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              let partial_cmp := M.alloc (| partial_cmp |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::iter::traits::iterator::iter_compare",
                        [
                          Self;
                          Ty.associated;
                          Ty.associated;
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "core::cmp::Ordering" ]
                        ]
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            I,
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| other |) ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (| Self, "compare.partial_cmp_by", [] |),
                          [ M.read (| partial_cmp |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let ord := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.StructTuple "core::option::Option::Some" [ M.read (| ord |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let ord := M.copy (| γ0_0 |) in
                        ord))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_partial_cmp_by :
          M.IsProvidedMethod
            "core::iter::traits::iterator::Iterator"
            "partial_cmp_by"
            partial_cmp_by.
        Definition eq (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "eq_by",
                  [ I; Ty.function [ Ty.tuple [ Ty.associated; Ty.associated ] ] (Ty.path "bool") ]
                |),
                [
                  M.read (| self |);
                  M.read (| other |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0; α1 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let x := M.copy (| γ |) in
                                    M.match_operator (|
                                      M.alloc (| α1 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let y := M.copy (| γ |) in
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialEq",
                                                Ty.associated,
                                                [ Ty.associated ],
                                                "eq",
                                                []
                                              |),
                                              [ x; y ]
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_eq :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "eq" eq.
        Definition eq_by (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I; F ], [ self; other; eq ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              let eq := M.alloc (| eq |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::iter::traits::iterator::iter_compare",
                        [ Self; Ty.associated; Ty.associated; Ty.tuple [] ]
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            I,
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| other |) ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (| Self, "compare.eq_by", [] |),
                          [ M.read (| eq |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let ord := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.path "core::cmp::Ordering",
                              [ Ty.path "core::cmp::Ordering" ],
                              "eq",
                              []
                            |),
                            [ ord; M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_eq_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "eq_by" eq_by.
        Definition ne (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              UnOp.not (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Self,
                    [],
                    "eq",
                    [ I ]
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_ne :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "ne" ne.
        Definition lt (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::cmp::Ordering" ],
                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::cmp::Ordering" ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "partial_cmp",
                        [ I ]
                      |),
                      [ M.read (| self |); M.read (| other |) ]
                    |)
                  |);
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [ Value.StructTuple "core::cmp::Ordering::Less" [] ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_lt :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "lt" lt.
        Definition le (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "partial_cmp",
                        [ I ]
                      |),
                      [ M.read (| self |); M.read (| other |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        M.find_or_pattern (|
                          γ0_0,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_le :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "le" le.
        Definition gt (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::cmp::Ordering" ],
                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::cmp::Ordering" ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "partial_cmp",
                        [ I ]
                      |),
                      [ M.read (| self |); M.read (| other |) ]
                    |)
                  |);
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [ Value.StructTuple "core::cmp::Ordering::Greater" [] ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_gt :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "gt" gt.
        Definition ge (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ _ as I ], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "partial_cmp",
                        [ I ]
                      |),
                      [ M.read (| self |); M.read (| other |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        M.find_or_pattern (|
                          γ0_0,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_ge :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "ge" ge.
        Definition is_sorted
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Self,
                  [],
                  "is_sorted_by",
                  [
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.apply (Ty.path "&") [] [ Ty.associated ];
                            Ty.apply (Ty.path "&") [] [ Ty.associated ]
                          ]
                      ]
                      (Ty.path "bool")
                  ]
                |),
                [
                  M.read (| self |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0; α1 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let a := M.copy (| γ |) in
                                    M.match_operator (|
                                      M.alloc (| α1 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let b := M.copy (| γ |) in
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialOrd",
                                                Ty.apply (Ty.path "&") [] [ Ty.associated ],
                                                [ Ty.apply (Ty.path "&") [] [ Ty.associated ] ],
                                                "le",
                                                []
                                              |),
                                              [ a; M.alloc (| M.read (| b |) |) ]
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_is_sorted :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "is_sorted" is_sorted.
        Definition is_sorted_by
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ F ], [ self; compare ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let compare := M.alloc (| compare |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ last :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Self,
                                [],
                                "next",
                                []
                              |),
                              [ self ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let e := M.copy (| γ0_0 |) in
                                e));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (| M.read (| M.return_ (| Value.Bool true |) |) |)
                                |)))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Self,
                          [],
                          "all",
                          [ Ty.associated ]
                        |),
                        [
                          self;
                          M.call_closure (|
                            M.get_associated_function (| Self, "check.is_sorted_by", [] |),
                            [ last; M.read (| compare |) ]
                          |)
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_is_sorted_by :
          M.IsProvidedMethod "core::iter::traits::iterator::Iterator" "is_sorted_by" is_sorted_by.
        Definition is_sorted_by_key
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ F; K ], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::iter::adapters::map::Map") [] [ Self; F ],
                  [],
                  "is_sorted",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Self,
                      [],
                      "map",
                      [ K; F ]
                    |),
                    [ M.read (| self |); M.read (| f |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_is_sorted_by_key :
          M.IsProvidedMethod
            "core::iter::traits::iterator::Iterator"
            "is_sorted_by_key"
            is_sorted_by_key.
        Definition __iterator_get_unchecked
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; _idx ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let _idx := M.alloc (| _idx |) in
              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
                                  "internal error: entered unreachable code: Always specialized"
                              |)
                            ]
                        |);
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "none",
                              []
                            |),
                            []
                          |)
                        |)
                      ]
                    |)
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod___iterator_get_unchecked :
          M.IsProvidedMethod
            "core::iter::traits::iterator::Iterator"
            "__iterator_get_unchecked"
            __iterator_get_unchecked.
      End Iterator.
      
      (*
      fn iter_compare<A, B, F, T>(mut a: A, mut b: B, f: F) -> ControlFlow<T, Ordering>
      where
          A: Iterator,
          B: Iterator,
          F: FnMut(A::Item, B::Item) -> ControlFlow<T>,
      {
          #[inline]
          fn compare<'a, B, X, T>(
              b: &'a mut B,
              mut f: impl FnMut(X, B::Item) -> ControlFlow<T> + 'a,
          ) -> impl FnMut(X) -> ControlFlow<ControlFlow<T, Ordering>> + 'a
          where
              B: Iterator,
          {
              move |x| match b.next() {
                  None => ControlFlow::Break(ControlFlow::Continue(Ordering::Greater)),
                  Some(y) => f(x, y).map_break(ControlFlow::Break),
              }
          }
      
          match a.try_for_each(compare(&mut b, f)) {
              ControlFlow::Continue(()) => ControlFlow::Continue(match b.next() {
                  None => Ordering::Equal,
                  Some(_) => Ordering::Less,
              }),
              ControlFlow::Break(x) => x,
          }
      }
      *)
      Definition iter_compare (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ A; B; F; T ], [ a; b; f ] =>
          ltac:(M.monadic
            (let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      A,
                      [],
                      "try_for_each",
                      [
                        Ty.associated;
                        Ty.apply
                          (Ty.path "core::ops::control_flow::ControlFlow")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::ops::control_flow::ControlFlow")
                              []
                              [ T; Ty.path "core::cmp::Ordering" ];
                            Ty.tuple []
                          ]
                      ]
                    |),
                    [
                      a;
                      M.call_closure (|
                        M.get_function (|
                          "core::iter::traits::iterator::iter_compare.compare",
                          []
                        |),
                        [ b; M.read (| f |) ]
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Continue"
                          [
                            M.read (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      B,
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ b ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        Value.StructTuple "core::cmp::Ordering::Equal" []
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      M.alloc (|
                                        Value.StructTuple "core::cmp::Ordering::Less" []
                                      |)))
                                ]
                              |)
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      x))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_iter_compare :
        M.IsFunction "core::iter::traits::iterator::iter_compare" iter_compare.
      
      Module iter_compare.
        (*
            fn compare<'a, B, X, T>(
                b: &'a mut B,
                mut f: impl FnMut(X, B::Item) -> ControlFlow<T> + 'a,
            ) -> impl FnMut(X) -> ControlFlow<ControlFlow<T, Ordering>> + 'a
            where
                B: Iterator,
            {
                move |x| match b.next() {
                    None => ControlFlow::Break(ControlFlow::Continue(Ordering::Greater)),
                    Some(y) => f(x, y).map_break(ControlFlow::Break),
                }
            }
        *)
        Definition compare (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ B; X; T; impl_FnMut_X__B_Item__arrow_ControlFlow_T___plus__'a ], [ b; f ] =>
            ltac:(M.monadic
              (let b := M.alloc (| b |) in
              let f := M.alloc (| f |) in
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let x := M.copy (| γ |) in
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          B,
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ M.read (| b |) ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            Value.StructTuple
                                              "core::ops::control_flow::ControlFlow::Break"
                                              [
                                                Value.StructTuple
                                                  "core::ops::control_flow::ControlFlow::Continue"
                                                  [
                                                    Value.StructTuple
                                                      "core::cmp::Ordering::Greater"
                                                      []
                                                  ]
                                              ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let y := M.copy (| γ0_0 |) in
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ops::control_flow::ControlFlow")
                                                  []
                                                  [ T; Ty.tuple [] ],
                                                "map_break",
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::ops::control_flow::ControlFlow")
                                                    []
                                                    [ T; Ty.path "core::cmp::Ordering" ];
                                                  Ty.function
                                                    [ T ]
                                                    (Ty.apply
                                                      (Ty.path
                                                        "core::ops::control_flow::ControlFlow")
                                                      []
                                                      [ T; Ty.path "core::cmp::Ordering" ])
                                                ]
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    impl_FnMut_X__B_Item__arrow_ControlFlow_T___plus__'a,
                                                    [ Ty.tuple [ X; Ty.associated ] ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [
                                                    f;
                                                    Value.Tuple [ M.read (| x |); M.read (| y |) ]
                                                  ]
                                                |);
                                                M.constructor_as_closure
                                                  "core::ops::control_flow::ControlFlow::Break"
                                              ]
                                            |)
                                          |)))
                                    ]
                                  |)
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_compare :
          M.IsFunction "core::iter::traits::iterator::iter_compare::compare" compare.
        
        Module compare.
          (* Error OpaqueTy *)
        End compare.
      End iter_compare.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Sized_I_for_ref_mut_I.
        Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ I ].
        
        (*     type Item = I::Item; *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn next(&mut self) -> Option<I::Item> {
                ( **self).next()
            }
        *)
        Definition next (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "next",
                  []
                |),
                [ M.read (| M.read (| self |) |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                ( **self).size_hint()
            }
        *)
        Definition size_hint (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "size_hint",
                  []
                |),
                [ M.read (| M.read (| self |) |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                ( **self).advance_by(n)
            }
        *)
        Definition advance_by
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "advance_by",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<Self::Item> {
                ( **self).nth(n)
            }
        *)
        Definition nth (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (| "core::iter::traits::iterator::Iterator", I, [], "nth", [] |),
                [ M.read (| M.read (| self |) |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<B, F>(self, init: B, f: F) -> B
            where
                F: FnMut(B, Self::Item) -> B,
            {
                self.spec_fold(init, f)
            }
        *)
        Definition fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ B; F ], [ 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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::IteratorRefSpec",
                  Ty.apply (Ty.path "&mut") [] [ I ],
                  [],
                  "spec_fold",
                  [ B; F ]
                |),
                [ M.read (| self |); M.read (| init |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                self.spec_try_fold(init, f)
            }
        *)
        Definition try_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I 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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::IteratorRefSpec",
                  Ty.apply (Ty.path "&mut") [] [ I ],
                  [],
                  "spec_try_fold",
                  [ B; F; R ]
                |),
                [ M.read (| self |); M.read (| init |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I));
              ("next", InstanceField.Method (next I));
              ("size_hint", InstanceField.Method (size_hint I));
              ("advance_by", InstanceField.Method (advance_by I));
              ("nth", InstanceField.Method (nth I));
              ("fold", InstanceField.Method (fold I));
              ("try_fold", InstanceField.Method (try_fold I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Sized_I_for_ref_mut_I.
      
      (* Trait *)
      (* Empty module 'IteratorRefSpec' *)
      
      Module Impl_core_iter_traits_iterator_IteratorRefSpec_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Sized_I_for_ref_mut_I.
        Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ I ].
        
        (*
            default fn spec_fold<B, F>(self, init: B, mut f: F) -> B
            where
                F: FnMut(B, Self::Item) -> B,
            {
                let mut accum = init;
                while let Some(x) = self.next() {
                    accum = f(accum, x);
                }
                accum
            }
        *)
        Definition spec_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ B; F ], [ 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.read (|
                let~ accum := M.copy (| init |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      I,
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |)
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let x := M.copy (| γ0_0 |) in
                              let~ _ :=
                                M.write (|
                                  accum,
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [ Ty.tuple [ B; Ty.associated ] ],
                                      "call_mut",
                                      []
                                    |),
                                    [ f; Value.Tuple [ M.read (| accum |); M.read (| x |) ] ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) in
                accum
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn spec_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 mut accum = init;
                while let Some(x) = self.next() {
                    accum = f(accum, x)?;
                }
                try { accum }
            }
        *)
        Definition spec_try_fold
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I 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~ accum := M.copy (| init |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply (Ty.path "&mut") [] [ I ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let x := M.copy (| γ0_0 |) in
                                  let~ _ :=
                                    M.write (|
                                      accum,
                                      M.read (|
                                        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::ops::function::FnMut",
                                                    F,
                                                    [ Ty.tuple [ B; Ty.associated ] ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [
                                                    f;
                                                    Value.Tuple
                                                      [ M.read (| accum |); M.read (| x |) ]
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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 (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| accum |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::IteratorRefSpec"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("spec_fold", InstanceField.Method (spec_fold I));
              ("spec_try_fold", InstanceField.Method (spec_try_fold I))
            ].
      End Impl_core_iter_traits_iterator_IteratorRefSpec_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Sized_I_for_ref_mut_I.
      
      Module Impl_core_iter_traits_iterator_IteratorRefSpec_where_core_iter_traits_iterator_Iterator_I_for_ref_mut_I.
        Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ I ].
        
        (*
                fn $fold<AAA, FFF>(mut self, init: AAA, fold: FFF) -> AAA
                where
                    FFF: FnMut(AAA, Self::Item) -> AAA,
                {
                    use crate::ops::NeverShortCircuit;
        
                    self.$try_fold(init, NeverShortCircuit::wrap_mut_2(fold)).0
                }
        *)
        Definition spec_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ AAA; FFF ], [ self; init; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let fold := M.alloc (| fold |) in
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::IteratorRefSpec",
                        Ty.apply (Ty.path "&mut") [] [ I ],
                        [],
                        "spec_try_fold",
                        [
                          AAA;
                          Ty.associated;
                          Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ AAA ]
                        ]
                      |),
                      [
                        self;
                        M.read (| init |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ AAA ],
                            "wrap_mut_2",
                            [ AAA; Ty.associated; FFF ]
                          |),
                          [ M.read (| fold |) ]
                        |)
                      ]
                    |)
                  |),
                  "core::ops::try_trait::NeverShortCircuit",
                  0
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn spec_try_fold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                ( **self).try_fold(init, f)
            }
        *)
        Definition spec_try_fold
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I 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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "try_fold",
                  [ B; F; R ]
                |),
                [ M.read (| M.read (| self |) |); M.read (| init |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::IteratorRefSpec"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("spec_fold", InstanceField.Method (spec_fold I));
              ("spec_try_fold", InstanceField.Method (spec_try_fold I))
            ].
      End Impl_core_iter_traits_iterator_IteratorRefSpec_where_core_iter_traits_iterator_Iterator_I_for_ref_mut_I.
    End iterator.
  End traits.
End iter.
