def bx.ru32

bend-osdev-aes@0.1.0.0 · PROOF.bend:22

import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF

import Base
import bend-osdev-mode-core@0.1.0.0/LAWS.bend as CoreL

22def bx.ru32(a: U32, b: U32) -> {U32.xor(U32.xor(a, b), b) == a : U32}:
23  CoreL.u32_xor_xor(a, b)

Uses (3)

Used by (1)

bend-osdev-aes@0.1.0.0/PROOF:ap.ark2