PROOF.m_lin_l: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
Lines 445-448 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=445&end_line=448

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

def m_lin_l(+s: G.Gf8Bits, +t: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits.xor(s, t), b, p) == G.Gf8Bits.xor(G.Gf8Bits.mul(s, b, p), G.Gf8Bits.mul(t, b, p)) : G.Gf8Bits}:
  match s t:
    case G.Gf8Bits{+s0, +s1, +s2, +s3, +s4, +s5, +s6, +s7} G.Gf8Bits{+t0, +t1, +t2, +t3, +t4, +t5, +t6, +t7}:
      horner_lin_a([GfPb{s7, t7}, GfPb{s6, t6}, GfPb{s5, t5}, GfPb{s4, t4}, GfPb{s3, t3}, GfPb{s2, t2}, GfPb{s1, t1}, GfPb{s0, t0}], G.Gf8Bits.zero(), G.Gf8Bits.zero(), b, p)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=GfPb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=horner_lin_a
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.zero