∀ (s needle : String.Slice) (table : Vector ℕ needle.utf8ByteSize)
  (htable : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) (stackPos needlePos : String.Pos.Raw)
  (hn : needlePos < needle.rawEndPos),
  stackPos < s.rawEndPos →
    ∀ (h : ¬needlePos.inc = needle.rawEndPos),
      match
        Std.IterStep.skip
          {
            internalState :=
              String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable stackPos.inc needlePos.inc ⋯ } with
      | Std.IterStep.yield it' out =>
        match
          {
              internalState :=
                String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable stackPos needlePos
                  hn }.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
          {
              internalState :=
                String.Slice.Pattern.ForwardSliceSearcher.proper needle table htable stackPos needlePos
                  hn }.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