def h.u_diff.c

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

import Base

2721def h.u_diff.c(
2722  +o: U32, +hk: U32, +mask: U32, +c: Bool,
2723  e2: {U32.is_eq((o .&. mask : U32), 0) == c : Bool},
2724  ed: {U32.is_eq((hk .&. mask : U32), 0) == Bool.not(c) : Bool},
2725  b: Bool, eb: {b == U32.is_eq(o, hk) : Bool}
2726) -> {b == False{} : Bool}:
2727  match b:
2728    case True{}:
2729      +e3 = rw(U32, z => {U32.is_eq((z .&. mask : U32), 0) == c : Bool}, hk, o,
2730        Equal.sym(U32, o, hk, h.u_sound(o, hk, h.sb(True{}, U32.is_eq(o, hk), eb))), e2)
2731      Empty.absurd({True{} == False{} : Bool}, h.cnc(c, Equal.trans(Bool, c, U32.is_eq((hk .&. mask : U32), 0), Bool.not(c),
2732          Equal.sym(Bool, U32.is_eq((hk .&. mask : U32), 0), c, e3), ed)))
2733    case False{}:
2734      {==}