∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size) (guess : ℕ) (hg : guess < stackPos),
  ¬guess = 0 →
    String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (guess - 1) ⋯ ≤ guess - 1 →
      ¬String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝¹ pat (guess - 1) ⋯ < guess → False