∀ (pat : String.Slice) (table : Array ℕ) (ht₀ : 0 < table.size) (ht : table.size ≤ pat.utf8ByteSize)
  (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) (hs : table.size < pat.utf8ByteSize),
  (table.push
        (if h_1 :
            pat.getUTF8Byte
                {
                  byteIdx :=
                    ↑(String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat
                        (pat.getUTF8Byte { byteIdx := table.size } hs) table ht h table[table.size - 1] ⋯) }
                ⋯ =
              pat.getUTF8Byte { byteIdx := table.size } hs then
          ↑(String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝¹ pat
                (pat.getUTF8Byte { byteIdx := table.size } hs) table ht h table[table.size - 1] ⋯) +
            1
        else
          ↑(String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝² pat
              (pat.getUTF8Byte { byteIdx := table.size } hs) table ht h table[table.size - 1] ⋯))).size ≤
    pat.utf8ByteSize