PROOF.x_lin: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
Lines 343-346 of bend-osdev-gf@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&start_line=343&end_line=346

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

def x_lin(+u: G.Gf8Bits, +v: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.x(G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.x(u, p), G.Gf8Bits.x(v, p)) : G.Gf8Bits}:
  match u v p:
    case G.Gf8Bits{+u0, +u1, +u2, +u3, +u4, +u5, +u6, +u7} G.Gf8Bits{+v0, +v1, +v2, +v3, +v4, +v5, +v6, +v7} G.Gf8Bits{+p0, +p1, +p2, +p3, +p4, +p5, +p6, +p7}:
      rb_eq(Bool.and(Bool.xor(u7, v7), p0), Bool.xor(Bool.xor(u0, v0), Bool.and(Bool.xor(u7, v7), p1)), Bool.xor(Bool.xor(u1, v1), Bool.and(Bool.xor(u7, v7), p2)), Bool.xor(Bool.xor(u2, v2), Bool.and(Bool.xor(u7, v7), p3)), Bool.xor(Bool.xor(u3, v3), Bool.and(Bool.xor(u7, v7), p4)), Bool.xor(Bool.xor(u4, v4), Bool.and(Bool.xor(u7, v7), p5)), Bool.xor(Bool.xor(u5, v5), Bool.and(Bool.xor(u7, v7), p6)), Bool.xor(Bool.xor(u6, v6), Bool.and(Bool.xor(u7, v7), p7)), Bool.xor(Bool.and(u7, p0), Bool.and(v7, p0)), Bool.xor(Bool.xor(u0, Bool.and(u7, p1)), Bool.xor(v0, Bool.and(v7, p1))), Bool.xor(Bool.xor(u1, Bool.and(u7, p2)), Bool.xor(v1, Bool.and(v7, p2))), Bool.xor(Bool.xor(u2, Bool.and(u7, p3)), Bool.xor(v2, Bool.and(v7, p3))), Bool.xor(Bool.xor(u3, Bool.and(u7, p4)), Bool.xor(v3, Bool.and(v7, p4))), Bool.xor(Bool.xor(u4, Bool.and(u7, p5)), Bool.xor(v4, Bool.and(v7, p5))), Bool.xor(Bool.xor(u5, Bool.and(u7, p6)), Bool.xor(v5, Bool.and(v7, p6))), Bool.xor(Bool.xor(u6, Bool.and(u7, p7)), Bool.xor(v6, Bool.and(v7, p7))), band_xor(u7, v7, p0), blin(u0, v0, u7, v7, p1), blin(u1, v1, u7, v7, p2), blin(u2, v2, u7, v7, p3), blin(u3, v3, u7, v7, p4), blin(u4, v4, u7, v7, p5), blin(u5, v5, u7, v7, p6), blin(u6, v6, u7, v7, p7))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=band_xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=blin
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rb_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.x
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.xor