def comm_e2

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

1676def comm_e2(+b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, b, p) == G.Gf8Bits.mul(b, G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, p) : G.Gf8Bits}:
1677  match p:
1678    case G.Gf8Bits{+p0, +p1, +p2, +p3, +p4, +p5, +p6, +p7}:
1679      %dec(b) : {G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, _, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) == G.Gf8Bits.mul(b, G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) : G.Gf8Bits}
1680      %dec(b) : {G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, ss(bl(b), basis()), G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) == G.Gf8Bits.mul(_, G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) : G.Gf8Bits}
1681      Equal.trans(G.Gf8Bits, G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, ss(bl(b), basis()), G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), ss(bl(b), mr(basis(), G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7})), G.Gf8Bits.mul(ss(bl(b), basis()), G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), lin_r(bl(b), basis(), G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), Equal.sym(G.Gf8Bits, G.Gf8Bits.mul(ss(bl(b), basis()), G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), ss(bl(b), ml(basis(), G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7})), lin_l(bl(b), basis(), G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7})))
Uses (13)

Used by (1)

bend-osdev-gf@0.1.1.0/PROOF:mlr