∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size} (h₀ : 0 < stackPos) (k : ℕ),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (stackPos - 1) ⋯ + 1 < k → ¬k = k - 1 + 1 → False