def h.u_ne0.c

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

import Base

2671# Routing facts about hashes and a mask.
2672def h.u_ne0.c(
2673  +x: U32, +y: U32, e1: {U32.is_eq(x, y) == False{} : Bool}, e2: {U32.is_eq(x, 0) == True{} : Bool},
2674  b: Bool, eb: {b == U32.is_eq(y, 0) : Bool}
2675) -> {b == False{} : Bool}:
2676  match b:
2677    case True{}:
2678      h.tf({True{} == False{} : Bool}, U32.is_eq(x, y),
2679        rw(U32, z => {U32.is_eq(x, z) == True{} : Bool}, y, 0,
2680          h.u_sound(y, 0, h.sb(True{}, U32.is_eq(y, 0), eb)), e2),
2681        e1)
2682    case False{}:
2683      {==}