def ml_x

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

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

1734def ml_x(+b: G.Gf8Bits, +p: G.Gf8Bits) -> {ml(basis(), b, p) == xs(b, p) : List<&2, G.Gf8Bits>}:
1735  %me0(b, p) : {ml(basis(), b, p) == [_, xk(1n, b, p), xk(2n, b, p), xk(3n, b, p), xk(4n, b, p), xk(5n, b, p), xk(6n, b, p), xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1736  %me1(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), _, xk(2n, b, p), xk(3n, b, p), xk(4n, b, p), xk(5n, b, p), xk(6n, b, p), xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1737  %me2(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), _, xk(3n, b, p), xk(4n, b, p), xk(5n, b, p), xk(6n, b, p), xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1738  %me3(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, b, p), _, xk(4n, b, p), xk(5n, b, p), xk(6n, b, p), xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1739  %me4(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}, b, p), _, xk(5n, b, p), xk(6n, b, p), xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1740  %me5(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}, b, p), _, xk(6n, b, p), xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1741  %me6(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, False{}, False{}}, b, p), _, xk(7n, b, p)] : List<&2, G.Gf8Bits>}
1742  %me7(b, p) : {ml(basis(), b, p) == [G.Gf8Bits.mul(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, False{}, False{}}, b, p), G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, b, p), _] : List<&2, G.Gf8Bits>}
1743  {==}