def h.u_same0

bend-kit-collections@0.1.4.1 · PROOF.bend:2711

import Base

2711def h.u_same0(
2712  +o: U32, +hk: U32, +mask: U32, -c: Bool,
2713  e1: {U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)) == True{} : Bool},
2714  e2: {U32.is_eq((o .&. mask : U32), 0) == c : Bool}
2715) -> {U32.is_eq((hk .&. mask : U32), 0) == c : Bool}:
2716  rw(U32, z => {U32.is_eq(z, 0) == c : Bool}, (hk .&. mask : U32), (o .&. mask : U32),
2717    Equal.sym(U32, (o .&. mask : U32), (hk .&. mask : U32),
2718      h.u_sound((o .&. mask : U32), (hk .&. mask : U32), e1)),
2719    e2)