def hf

bend-osdev-gf@0.1.1.0 · PROOF.bend:1612

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

1612def 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}:
1613  match n:
1614    case 0n:
1615      {==}
1616    case 1n+k:
1617      %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}
1618      hf(k, G.Gf8Bits.x(acc, p), b, p)