law wlt

lawful-bytes@0.1.1.0 · proof_fast_find.bend:353

import Base

353# Word index bounds: the words searched lie inside the block.
354law wlt:
355  for +w: Nat
356  for +k: Nat
357  for +tt: Nat
358  for +ll: Nat
359  for +pp: Nat
360  for +h1: {Nat.is_lt(Nat.mul(Nat.add(w, k), 4n), tt) == True{} : Bool}
361  for +h2: {Nat.is_le(tt, ll) == True{} : Bool}
362  for +h3: {Nat.is_le(ll, Nat.mul(4n, pp)) == True{} : Bool}
363  {Nat.is_lt(w, pp) == True{} : Bool}