def ax

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

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

1745def ax(+b: G.Gf8Bits, +c: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits.x(b, p), c, p) == G.Gf8Bits.x(G.Gf8Bits.mul(b, c, p), p) : G.Gf8Bits}:
1746  Equal.trans(G.Gf8Bits, G.Gf8Bits.mul(G.Gf8Bits.x(b, p), c, p), ss(bl(c), xs(G.Gf8Bits.x(b, p), p)), G.Gf8Bits.x(G.Gf8Bits.mul(b, c, p), p), Equal.trans(G.Gf8Bits, G.Gf8Bits.mul(G.Gf8Bits.x(b, p), c, p), G.Gf8Bits.mul(c, G.Gf8Bits.x(b, p), p), ss(bl(c), xs(G.Gf8Bits.x(b, p), p)), comm(G.Gf8Bits.x(b, p), c, p), Equal.trans(G.Gf8Bits, G.Gf8Bits.mul(c, G.Gf8Bits.x(b, p), p), G.Gf8Bits.mul(ss(bl(c), basis()), G.Gf8Bits.x(b, p), p), ss(bl(c), xs(G.Gf8Bits.x(b, p), p)), Equal.cong(G.Gf8Bits, G.Gf8Bits, z => G.Gf8Bits.mul(z, G.Gf8Bits.x(b, p), p), c, ss(bl(c), basis()), Equal.sym(G.Gf8Bits, ss(bl(c), basis()), c, dec(c))), Equal.trans(G.Gf8Bits, G.Gf8Bits.mul(ss(bl(c), basis()), G.Gf8Bits.x(b, p), p), ss(bl(c), ml(basis(), G.Gf8Bits.x(b, p), p)), ss(bl(c), xs(G.Gf8Bits.x(b, p), p)), lin_l(bl(c), basis(), G.Gf8Bits.x(b, p), p), Equal.cong(List<&2, G.Gf8Bits>, G.Gf8Bits, l => ss(bl(c), l), ml(basis(), G.Gf8Bits.x(b, p), p), xs(G.Gf8Bits.x(b, p), p), ml_x(G.Gf8Bits.x(b, p), p))))), Equal.sym(G.Gf8Bits, G.Gf8Bits.x(G.Gf8Bits.mul(b, c, p), p), ss(bl(c), xl(xs(b, p), p)), Equal.trans(G.Gf8Bits, G.Gf8Bits.x(G.Gf8Bits.mul(b, c, p), p), G.Gf8Bits.x(G.Gf8Bits.mul(c, b, p), p), ss(bl(c), xl(xs(b, p), p)), Equal.cong(G.Gf8Bits, G.Gf8Bits, z => G.Gf8Bits.x(z, p), G.Gf8Bits.mul(b, c, p), G.Gf8Bits.mul(c, b, p), comm(b, c, p)), Equal.trans(G.Gf8Bits, G.Gf8Bits.x(G.Gf8Bits.mul(c, b, p), p), G.Gf8Bits.x(G.Gf8Bits.mul(ss(bl(c), basis()), b, p), p), ss(bl(c), xl(xs(b, p), p)), Equal.cong(G.Gf8Bits, G.Gf8Bits, z => G.Gf8Bits.x(G.Gf8Bits.mul(z, b, p), p), c, ss(bl(c), basis()), Equal.sym(G.Gf8Bits, ss(bl(c), basis()), c, dec(c))), Equal.trans(G.Gf8Bits, G.Gf8Bits.x(G.Gf8Bits.mul(ss(bl(c), basis()), b, p), p), G.Gf8Bits.x(ss(bl(c), ml(basis(), b, p)), p), ss(bl(c), xl(xs(b, p), p)), Equal.cong(G.Gf8Bits, G.Gf8Bits, z => G.Gf8Bits.x(z, p), G.Gf8Bits.mul(ss(bl(c), basis()), b, p), ss(bl(c), ml(basis(), b, p)), lin_l(bl(c), basis(), b, p)), Equal.trans(G.Gf8Bits, G.Gf8Bits.x(ss(bl(c), ml(basis(), b, p)), p), G.Gf8Bits.x(ss(bl(c), xs(b, p)), p), ss(bl(c), xl(xs(b, p), p)), Equal.cong(List<&2, G.Gf8Bits>, G.Gf8Bits, l => G.Gf8Bits.x(ss(bl(c), l), p), ml(basis(), b, p), xs(b, p), ml_x(b, p)), lin_x(bl(c), xs(b, p), p)))))))