def horner_lin_b

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

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

387def 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}:
388  match ts:
389    case Nil{}:
390      {==}
391    case Con{+t, rest}:
392      %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}
393      horner_lin_b(rest, G.Gf8Bits.step(t, A, u, p), G.Gf8Bits.step(t, C, v, p), u, v, p)