law byte_pack4

lawful-words@0.1.0.0 · proof_bytes.bend:1266

import Base
import lawful-words@0.1.0.0/defs.bend as D

1266law byte_pack4:
1267  for +b0: U32
1268  for +b1: U32
1269  for +b2: U32
1270  for +b3: U32
1271  for +j: Nat
1272  for +h0: {U32.is_lt(b0, 256) == True{} : Bool}
1273  for +h1: {U32.is_lt(b1, 256) == True{} : Bool}
1274  for +h2: {U32.is_lt(b2, 256) == True{} : Bool}
1275  for +h3: {U32.is_lt(b3, 256) == True{} : Bool}
1276  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1277  {D.byte(D.pack4(b0, b1, b2, b3), j) == D.nth4(j, b0, b1, b2, b3) : U32}