def h.u_route_t.c

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

import Base

2690def h.u_route_t.c(
2691  +o: U32, +hk: U32, +mask: U32, ob: {h.onebit(mask) == True{} : Bool},
2692  e1: {U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)) == False{} : Bool},
2693  e2: {U32.is_eq((o .&. mask : U32), 0) == False{} : Bool},
2694  b: Bool, eb: {b == U32.is_eq((hk .&. mask : U32), 0) : Bool}
2695) -> {b == True{} : Bool}:
2696  match b:
2697    case True{}:
2698      {==}
2699    case False{}:
2700      h.tf({False{} == True{} : Bool}, U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)),
2701        h.route(o, hk, mask, ob, e2, h.sb(False{}, U32.is_eq((hk .&. mask : U32), 0), eb)),
2702        e1)