law inc_fits

lawful-bytes@0.1.1.0 · proof_core.bend:553

import Base

553# An index below 4 * 2^d steps up by one.
554law inc_fits:
555  for +a: U32
556  for +d: Nat
557  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
558  for +h: {Nat.is_lt(U32.to_nat(a), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
559  {U32.to_nat((a + 1 : U32)) == Nat.add(U32.to_nat(a), 1n) : Nat}