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

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

def hf(n: Nat, +acc: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.horner(fs(n), acc, b, p) == xk(n, acc, p) : G.Gf8Bits}:
  match n:
    case 0n:
      {==}
    case 1n+k:
      %Equal.sym(G.Gf8Bits, G.Gf8Bits.xor(G.Gf8Bits.x(acc, p), G.Gf8Bits.zero()), G.Gf8Bits.x(acc, p), rx_zr(G.Gf8Bits.x(acc, p))) : {G.Gf8Bits.horner(fs(k), _, b, p) == xk(k, G.Gf8Bits.x(acc, p), p) : G.Gf8Bits}
      hf(k, G.Gf8Bits.x(acc, p), b, p)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=fs
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_zr
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=xk
  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.x
  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