def bx.u32

bend-osdev-cbc@0.1.0.0 · PROOF.bend:78

import Base

78def bx.u32(a: U32, b: U32) -> {U32.xor(a, U32.xor(a, b)) == b : U32}:
79  match a b:
80    case U32{x} U32{y}:
81      %bx.word(32n, x, y) : {U32{Word.xor(32n, x, Word.xor(32n, x, y))} == U32{_} : U32}
82      {==}