{s : String.Slice} →
  {motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u} →
    ((pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos)) →
      ((pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h)) →
        ((needle : String.Slice) →
            (table : Vector ℕ needle.utf8ByteSize) →
              (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
                (stackPos needlePos : String.Pos.Raw) →
                  (hn : needlePos < needle.rawEndPos) →
                    motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn)) →
          motive String.Slice.Pattern.ForwardSliceSearcher.atEnd →
            (t : String.Slice.Pattern.ForwardSliceSearcher s) → motive t