law ut

lawful-bytes@0.1.1.0 · proof_grow.bend:343

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

343# Only the first q words matter for the first m <= 4q bytes.
344law ut:
345  for +ws: List<&2, U32>
346  for +q: Nat
347  for +m: Nat
348  for +h: {Nat.is_le(m, Nat.mul(q, 4n)) == True{} : Bool}
349  {List.take(&2, U32, D.unpack(ws), m) == List.take(&2, U32, D.unpack(List.take(&2, U32, ws, q)), m) : List<&2, U32>}