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

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

def mlx_c(+b: G.Gf8Bits, +c: G.Gf8Bits, +p: G.Gf8Bits) -> {ml(xs(b, p), c, p) == xs(G.Gf8Bits.mul(b, c, p), p) : List<&2, G.Gf8Bits>}:
  %ak(0n, b, c, p) : {ml(xs(b, p), c, p) == [_, xk(1n, G.Gf8Bits.mul(b, c, p), p), xk(2n, G.Gf8Bits.mul(b, c, p), p), xk(3n, G.Gf8Bits.mul(b, c, p), p), xk(4n, G.Gf8Bits.mul(b, c, p), p), xk(5n, G.Gf8Bits.mul(b, c, p), p), xk(6n, G.Gf8Bits.mul(b, c, p), p), xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(1n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), _, xk(2n, G.Gf8Bits.mul(b, c, p), p), xk(3n, G.Gf8Bits.mul(b, c, p), p), xk(4n, G.Gf8Bits.mul(b, c, p), p), xk(5n, G.Gf8Bits.mul(b, c, p), p), xk(6n, G.Gf8Bits.mul(b, c, p), p), xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(2n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), G.Gf8Bits.mul(xk(1n, b, p), c, p), _, xk(3n, G.Gf8Bits.mul(b, c, p), p), xk(4n, G.Gf8Bits.mul(b, c, p), p), xk(5n, G.Gf8Bits.mul(b, c, p), p), xk(6n, G.Gf8Bits.mul(b, c, p), p), xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(3n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), G.Gf8Bits.mul(xk(1n, b, p), c, p), G.Gf8Bits.mul(xk(2n, b, p), c, p), _, xk(4n, G.Gf8Bits.mul(b, c, p), p), xk(5n, G.Gf8Bits.mul(b, c, p), p), xk(6n, G.Gf8Bits.mul(b, c, p), p), xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(4n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), G.Gf8Bits.mul(xk(1n, b, p), c, p), G.Gf8Bits.mul(xk(2n, b, p), c, p), G.Gf8Bits.mul(xk(3n, b, p), c, p), _, xk(5n, G.Gf8Bits.mul(b, c, p), p), xk(6n, G.Gf8Bits.mul(b, c, p), p), xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(5n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), G.Gf8Bits.mul(xk(1n, b, p), c, p), G.Gf8Bits.mul(xk(2n, b, p), c, p), G.Gf8Bits.mul(xk(3n, b, p), c, p), G.Gf8Bits.mul(xk(4n, b, p), c, p), _, xk(6n, G.Gf8Bits.mul(b, c, p), p), xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(6n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), G.Gf8Bits.mul(xk(1n, b, p), c, p), G.Gf8Bits.mul(xk(2n, b, p), c, p), G.Gf8Bits.mul(xk(3n, b, p), c, p), G.Gf8Bits.mul(xk(4n, b, p), c, p), G.Gf8Bits.mul(xk(5n, b, p), c, p), _, xk(7n, G.Gf8Bits.mul(b, c, p), p)] : List<&2, G.Gf8Bits>}
  %ak(7n, b, c, p) : {ml(xs(b, p), c, p) == [G.Gf8Bits.mul(xk(0n, b, p), c, p), G.Gf8Bits.mul(xk(1n, b, p), c, p), G.Gf8Bits.mul(xk(2n, b, p), c, p), G.Gf8Bits.mul(xk(3n, b, p), c, p), G.Gf8Bits.mul(xk(4n, b, p), c, p), G.Gf8Bits.mul(xk(5n, b, p), c, p), G.Gf8Bits.mul(xk(6n, b, p), c, p), _] : List<&2, G.Gf8Bits>}
  {==}

Uses (7):
  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=ak
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=ml
  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/PROOF.bend&name=xs
  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.mul