(s : String.Slice) →
  (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1) →
    (x : String.Slice.Pattern.ForwardSliceSearcher s) →
      ((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)) →
            (Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd) → motive x