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