def bxor_assoc

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:32

import Base

32def bxor_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}:
33  match a b c:
34    case True{} True{} True{}:
35      {==}
36    case True{} True{} False{}:
37      {==}
38    case True{} False{} True{}:
39      {==}
40    case True{} False{} False{}:
41      {==}
42    case False{} True{} True{}:
43      {==}
44    case False{} True{} False{}:
45      {==}
46    case False{} False{} True{}:
47      {==}
48    case False{} False{} False{}:
49      {==}