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

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

def horner_lin_b(ts: List<&2, Bool>, +A: G.Gf8Bits, +C: G.Gf8Bits, +u: G.Gf8Bits, +v: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.horner(ts, G.Gf8Bits.xor(A, C), G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.horner(ts, A, u, p), G.Gf8Bits.horner(ts, C, v, p)) : G.Gf8Bits}:
  match ts:
    case Nil{}:
      {==}
    case Con{+t, rest}:
      %Equal.sym(G.Gf8Bits, G.Gf8Bits.step(t, G.Gf8Bits.xor(A, C), G.Gf8Bits.xor(u, v), p), G.Gf8Bits.xor(G.Gf8Bits.step(t, A, u, p), G.Gf8Bits.step(t, C, v, p)), step_lin_b(t, A, C, u, v, p)) : {G.Gf8Bits.horner(rest, _, G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.horner(rest, G.Gf8Bits.step(t, A, u, p), u, p), G.Gf8Bits.horner(rest, G.Gf8Bits.step(t, C, v, p), v, p)) : G.Gf8Bits}
      horner_lin_b(rest, G.Gf8Bits.step(t, A, u, p), G.Gf8Bits.step(t, C, v, p), u, v, p)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=step_lin_b
  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.horner
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.step
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.xor