law le_fit

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:616

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

616law le_fit:
617  for +xs: List<&2, U32>
618  for +b: Nat
619  for +k: Nat
620  for +one: Nat
621  for +h1: {one == 1n : Nat}
622  for +hb: {Nat.is_lt(b, C.shift(k, one)) == True{} : Bool}
623  for +h: {le_all(xs, b) == True{} : Bool}
624  {fit_all(xs, k) == True{} : Bool}