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

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

def horner_zero(ts: List<&2, Bool>, +p: G.Gf8Bits) -> {G.Gf8Bits.horner(ts, G.Gf8Bits.zero(), G.Gf8Bits.zero(), p) == G.Gf8Bits.zero() : G.Gf8Bits}:
  match ts:
    case Nil{}:
      {==}
    case Con{+t, rest}:
      %Equal.sym(G.Gf8Bits, G.Gf8Bits.step(t, G.Gf8Bits.zero(), G.Gf8Bits.zero(), p), G.Gf8Bits.zero(), step_zero(t, p)) : {G.Gf8Bits.horner(rest, _, G.Gf8Bits.zero(), p) == G.Gf8Bits.zero() : G.Gf8Bits}
      horner_zero(rest, 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_zero
  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.zero