∀ (pat : String.Slice)
  (computeDistance :
    UInt8 →
      (table : Array ℕ) →
        table.size ≤ pat.utf8ByteSize →
          (∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) → (guess : ℕ) → guess < table.size → { n // n ≤ table.size })
  (table : Array ℕ),
  0 < table.size →
    table.size ≤ pat.utf8ByteSize →
      (∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) →
        table.size < pat.utf8ByteSize → ¬table.size + 1 ≤ pat.utf8ByteSize → False