-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.instIteratorId.match_1.splitter : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          (motive : Std.IterM Id String.Slice → Std.IterStep (Std.IterM Id String.Slice) String.Slice → Sort u_1) →
            (x : Std.IterM Id String.Slice) →
              (x_1 : Std.IterStep (Std.IterM Id String.Slice) String.Slice) →
                ((currPos : s.Pos) →
                    (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                      (currPos_1 : s.Pos) →
                        (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                          (out : String.Slice) →
                            motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 }
                              (Std.IterStep.yield
                                { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' } out)) →
                  ((currPos : s.Pos) →
                      (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                        (out : String.Slice) →
                          motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 }
                            (Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.atEnd } out)) →
                    ((currPos : s.Pos) →
                        (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                          (currPos_1 : s.Pos) →
                            (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                              motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 }
                                (Std.IterStep.skip
                                  { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' })) →
                      ((currPos : s.Pos) →
                          (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                            motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 }
                              (Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.atEnd })) →
                        ((currPos : s.Pos) →
                            (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                              motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 }
                                Std.IterStep.done) →
                          ((it : Std.IterM Id String.Slice) →
                              (out : String.Slice) →
                                motive { internalState := String.Slice.SplitInclusiveIterator.atEnd }
                                  (Std.IterStep.yield it out)) →
                            ((it : Std.IterM Id String.Slice) →
                                motive { internalState := String.Slice.SplitInclusiveIterator.atEnd }
                                  (Std.IterStep.skip it)) →
                              (Unit →
                                  motive { internalState := String.Slice.SplitInclusiveIterator.atEnd }
                                    Std.IterStep.done) →
                                motive x x_1