law zb_eq

lawful-bytes@0.1.1.0 · proof_fast_w1.bend:51

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

51# fast.bend's zb is lawful-words' zb.
52law zb_eq:
53  for +v: U32
54  {FA.zb(v) == W.zb(v) : U32}