def rx_assoc

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

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

318def rx_assoc(+a: G.Gf8Bits, +b: G.Gf8Bits, +c: G.Gf8Bits) -> {G.Gf8Bits.xor(G.Gf8Bits.xor(a, b), c) == G.Gf8Bits.xor(a, G.Gf8Bits.xor(b, c)) : G.Gf8Bits}:
319  match a b c:
320    case G.Gf8Bits{+a0, +a1, +a2, +a3, +a4, +a5, +a6, +a7} G.Gf8Bits{+b0, +b1, +b2, +b3, +b4, +b5, +b6, +b7} G.Gf8Bits{+c0, +c1, +c2, +c3, +c4, +c5, +c6, +c7}:
321      rb_eq(Bool.xor(Bool.xor(a0, b0), c0), Bool.xor(Bool.xor(a1, b1), c1), Bool.xor(Bool.xor(a2, b2), c2), Bool.xor(Bool.xor(a3, b3), c3), Bool.xor(Bool.xor(a4, b4), c4), Bool.xor(Bool.xor(a5, b5), c5), Bool.xor(Bool.xor(a6, b6), c6), Bool.xor(Bool.xor(a7, b7), c7), Bool.xor(a0, Bool.xor(b0, c0)), Bool.xor(a1, Bool.xor(b1, c1)), Bool.xor(a2, Bool.xor(b2, c2)), Bool.xor(a3, Bool.xor(b3, c3)), Bool.xor(a4, Bool.xor(b4, c4)), Bool.xor(a5, Bool.xor(b5, c5)), Bool.xor(a6, Bool.xor(b6, c6)), Bool.xor(a7, Bool.xor(b7, c7)), bx_assoc(a0, b0, c0), bx_assoc(a1, b1, c1), bx_assoc(a2, b2, c2), bx_assoc(a3, b3, c3), bx_assoc(a4, b4, c4), bx_assoc(a5, b5, c5), bx_assoc(a6, b6, c6), bx_assoc(a7, b7, c7))