-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.eq_1 : ∀ (s : String.Slice),
  String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep s =
    {
      IsPlausibleStep := fun it x =>
        match x with
        | Std.IterStep.yield it' out =>
          match it.internalState with
          | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos =>
            (∃ (h : pos ≠ s.endPos), it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h) ∨
              it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.atEnd
          | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h =>
            ∃ newPos, pos < newPos ∧ it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.emptyBefore newPos
          | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
            (∃ newStackPos newNeedlePos,
                ∃ (hn : newNeedlePos < needle.rawEndPos),
                  it'.internalState =
                      String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht newStackPos newNeedlePos hn ∧
                    (s.utf8ByteSize - newStackPos.byteIdx < s.utf8ByteSize - stackPos.byteIdx ∨
                      newStackPos = stackPos ∧ newNeedlePos < needlePos)) ∨
              it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.atEnd
          | String.Slice.Pattern.ForwardSliceSearcher.atEnd => False
        | Std.IterStep.skip it' =>
          match it.internalState with
          | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos =>
            (∃ (h : pos ≠ s.endPos), it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h) ∨
              it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.atEnd
          | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h =>
            ∃ newPos, pos < newPos ∧ it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.emptyBefore newPos
          | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
            (∃ newStackPos newNeedlePos,
                ∃ (hn : newNeedlePos < needle.rawEndPos),
                  it'.internalState =
                      String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht newStackPos newNeedlePos hn ∧
                    (s.utf8ByteSize - newStackPos.byteIdx < s.utf8ByteSize - stackPos.byteIdx ∨
                      newStackPos = stackPos ∧ newNeedlePos < needlePos)) ∨
              it'.internalState = String.Slice.Pattern.ForwardSliceSearcher.atEnd
          | String.Slice.Pattern.ForwardSliceSearcher.atEnd => False
        | Std.IterStep.done => True,
      step := fun x =>
        match x with
        | { internalState := iter } =>
          match iter with
          | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos =>
            have res := String.Slice.Pattern.SearchStep.matched pos pos;
            if h : pos ≠ s.endPos then
              pure
                (Std.Shrink.deflate
                  ⟨Std.IterStep.yield { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h } res,
                    ⋯⟩)
            else
              pure
                (Std.Shrink.deflate
                  ⟨Std.IterStep.yield { internalState := String.Slice.Pattern.ForwardSliceSearcher.atEnd } res, ⋯⟩)
          | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h =>
            have res := String.Slice.Pattern.SearchStep.rejected pos (pos.next h);
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.yield
                    { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyBefore (pos.next h) } res,
                  ⋯⟩)
          | String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable stackPos needlePos hn =>
            if h₁' : (stackPos.unoffsetBy needlePos).increaseBy needle.utf8ByteSize ≤ s.rawEndPos then
              have h₁ := ⋯;
              have stackByte := s.getUTF8Byte stackPos h₁;
              have patByte := needle.getUTF8Byte needlePos hn;
              if stackByte = patByte then
                let nextStackPos := stackPos.inc;
                let nextNeedlePos := needlePos.inc;
                if h : nextNeedlePos = needle.rawEndPos then
                  have res :=
                    String.Slice.Pattern.SearchStep.matched (s.pos! (nextStackPos.unoffsetBy nextNeedlePos))
                      (s.pos! nextStackPos);
                  pure
                    (Std.Shrink.deflate
                      ⟨Std.IterStep.yield
                          {
                            internalState :=
                              String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable nextStackPos 0 ⋯ }
                          res,
                        ⋯⟩)
                else
                  pure
                    (Std.Shrink.deflate
                      ⟨Std.IterStep.skip
                          {
                            internalState :=
                              String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable nextStackPos
                                nextNeedlePos ⋯ },
                        ⋯⟩)
              else
                if hnp : needlePos = 0 then
                  have basePos := s.pos! stackPos;
                  let nextStackPos := s.posGT stackPos h₁;
                  have res := String.Slice.Pattern.SearchStep.rejected basePos nextStackPos;
                  pure
                    (Std.Shrink.deflate
                      ⟨Std.IterStep.yield
                          {
                            internalState :=
                              String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable nextStackPos.offset 0
                                ⋯ }
                          res,
                        ⋯⟩)
                else
                  let newNeedlePos := table[needlePos.byteIdx - 1];
                  if newNeedlePos = 0 then
                    have basePos := s.pos! (stackPos.unoffsetBy needlePos);
                    let nextStackPos := s.posGE stackPos ⋯;
                    have res := String.Slice.Pattern.SearchStep.rejected basePos nextStackPos;
                    pure
                      (Std.Shrink.deflate
                        ⟨Std.IterStep.yield
                            {
                              internalState :=
                                String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable nextStackPos.offset
                                  0 ⋯ }
                            res,
                          ⋯⟩)
                  else
                    have oldBasePos := s.pos! (stackPos.unoffsetBy needlePos);
                    have newBasePos := s.pos! (stackPos.unoffsetBy { byteIdx := newNeedlePos });
                    have res := String.Slice.Pattern.SearchStep.rejected oldBasePos newBasePos;
                    pure
                      (Std.Shrink.deflate
                        ⟨Std.IterStep.yield
                            {
                              internalState :=
                                String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable stackPos
                                  { byteIdx := newNeedlePos } ⋯ }
                            res,
                          ⋯⟩)
            else
              if stackPos.unoffsetBy needlePos < s.rawEndPos then
                have basePos := stackPos.unoffsetBy needlePos;
                have res := String.Slice.Pattern.SearchStep.rejected (s.pos! basePos) s.endPos;
                pure
                  (Std.Shrink.deflate
                    ⟨Std.IterStep.yield { internalState := String.Slice.Pattern.ForwardSliceSearcher.atEnd } res, ⋯⟩)
              else pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)
          | String.Slice.Pattern.ForwardSliceSearcher.atEnd => pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩) }