def bx_assoc

bend-osdev-gf@0.1.1.0 · PROOF.bend:34

import Base

34def bx_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}:
35  match a:
36    case True{}:
37      match b:
38        case True{}:
39          match c:
40            case True{}:
41              {==}
42            case False{}:
43              {==}
44        case False{}:
45          match c:
46            case True{}:
47              {==}
48            case False{}:
49              {==}
50    case False{}:
51      match b:
52        case True{}:
53          match c:
54            case True{}:
55              {==}
56            case False{}:
57              {==}
58        case False{}:
59          match c:
60            case True{}:
61              {==}
62            case False{}:
63              {==}