law zb2_none

lawful-bytes@0.1.1.0 · proof_fast_word.bend:83

import Base
import lawful-bytes@0.1.1.0/fast.bend as FA

83# The same for the flags of two words or-ed (find2).
84law zb2_none:
85  for +v1: U32
86  for +v2: U32
87  {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == Nat.is_eq(Nat.min(P0(v1), P0(v2)), 4n) : Bool}