∀ (pat : String.Slice) (table : Array ℕ) (ht₀ : 0 < table.size) (ht : table.size ≤ pat.utf8ByteSize)
  (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat table ht₀ ht h =
    if hs : table.size < pat.utf8ByteSize then
      let patByte := pat.getUTF8Byte { byteIdx := table.size } hs;
      let dist :=
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h
          table[table.size - 1] ⋯;
      String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat (table.push ↑dist) ⋯ ⋯ ⋯
    else Vector.mk table ⋯