def xbit

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/xor.bend:30

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/random/pcg.bend as SP
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

30def xbit(+a: Bool, +b: Bool) -> {S.bit_value(Bool.xor(a, b)) == SP.b2n(Bool.not(Nat.is_eq(S.bit_value(a), S.bit_value(b)))) : Nat}:
31  match a b:
32    case True{} True{}:
33      {==}
34    case True{} False{}:
35      {==}
36    case False{} True{}:
37      {==}
38    case False{} False{}:
39      {==}