def mlx_c

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

1755def 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>}:
1756  %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>}
1757  %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>}
1758  %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>}
1759  %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>}
1760  %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>}
1761  %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>}
1762  %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>}
1763  %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>}
1764  {==}
Uses (7)

Used by (1)

bend-osdev-gf@0.1.1.0/PROOF:assoc