law rep_byte

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:224

import Base
import lawful-words@0.1.0.0/defs.bend as W
import lawful-bytes@0.1.1.0/fast.bend as FA

224law rep_byte:
225  for +c: U32
226  for +j: Nat
227  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
228  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
229  {W.byte(FA.rep(c), j) == c : U32}