law is_lt_top

lawful-bytes@0.1.1.0 · proof_fast_find.bend:431

import Base

431law is_lt_top:
432  for +to: U32
433  for +d: Nat
434  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
435  for +ht: {Nat.is_le(U32.to_nat(to), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
436  {U32.is_lt(4294967295, to) == False{} : Bool}