def comm_e6

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

1704def comm_e6(+b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, b, p) == G.Gf8Bits.mul(b, G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, p) : G.Gf8Bits}:
1705  match p:
1706    case G.Gf8Bits{+p0, +p1, +p2, +p3, +p4, +p5, +p6, +p7}:
1707      %dec(b) : {G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, _, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) == G.Gf8Bits.mul(b, G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) : G.Gf8Bits}
1708      %dec(b) : {G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, ss(bl(b), basis()), G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) == G.Gf8Bits.mul(_, G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}) : G.Gf8Bits}
1709      Equal.trans(G.Gf8Bits, G.Gf8Bits.mul(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, ss(bl(b), basis()), G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), ss(bl(b), mr(basis(), G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7})), G.Gf8Bits.mul(ss(bl(b), basis()), G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), lin_r(bl(b), basis(), G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, 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{}, False{}, False{}, False{}, False{}, True{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}), ss(bl(b), ml(basis(), G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}, G.Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7})), lin_l(bl(b), basis(), G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, 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