-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.instIteratorOfPure.match_1.splitter : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
        {m : Type → Type u_1} →
          {s : String.Slice} →
            (motive : Std.IterM m String.Slice → Std.IterStep (Std.IterM m String.Slice) String.Slice → Sort u_2) →
              (x : Std.IterM m String.Slice) →
                (x_1 : Std.IterStep (Std.IterM m 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.RevSplitIterator.operating currPos s_1 }
                                (Std.IterStep.yield
                                  { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' } out)) →
                    ((currPos : s.Pos) →
                        (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                          (out : String.Slice) →
                            motive { internalState := String.Slice.RevSplitIterator.operating currPos s_1 }
                              (Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.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.RevSplitIterator.operating currPos s_1 }
                                  (Std.IterStep.skip
                                    { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' })) →
                        ((currPos : s.Pos) →
                            (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                              motive { internalState := String.Slice.RevSplitIterator.operating currPos s_1 }
                                (Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.atEnd })) →
                          ((currPos : s.Pos) →
                              (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                                motive { internalState := String.Slice.RevSplitIterator.operating currPos s_1 }
                                  Std.IterStep.done) →
                            ((it : Std.IterM m String.Slice) →
                                (out : String.Slice) →
                                  motive { internalState := String.Slice.RevSplitIterator.atEnd }
                                    (Std.IterStep.yield it out)) →
                              ((it : Std.IterM m String.Slice) →
                                  motive { internalState := String.Slice.RevSplitIterator.atEnd }
                                    (Std.IterStep.skip it)) →
                                (Unit →
                                    motive { internalState := String.Slice.RevSplitIterator.atEnd } Std.IterStep.done) →
                                  motive x x_1