PROOF.ap.imixg: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 1830-1837 of bend-osdev-aes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&start_line=1830&end_line=1837

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

def ap.imixg(+p: U32, +q: U32, +r: U32, +s: U32) -> {X.aes.imix0(p, q, r, s) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}:
  %Equal.sym(U32, X.aes.m14(p), G.Gf8.mul(G.Gf8.aes(), 14, p), ap.m14(p)) : {U32.xor(U32.xor(_, X.aes.m11(q)), U32.xor(X.aes.m13(r), X.aes.m9(s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
  %Equal.sym(U32, X.aes.m11(q), G.Gf8.mul(G.Gf8.aes(), 11, q), ap.m11(q)) : {U32.xor(U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), _), U32.xor(X.aes.m13(r), X.aes.m9(s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
  %Equal.sym(U32, X.aes.m13(r), G.Gf8.mul(G.Gf8.aes(), 13, r), ap.m13(r)) : {U32.xor(U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), U32.xor(_, X.aes.m9(s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
  %Equal.sym(U32, X.aes.m9(s), G.Gf8.mul(G.Gf8.aes(), 9, s), ap.m9(s)) : {U32.xor(U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), U32.xor(G.Gf8.mul(G.Gf8.aes(), 13, r), _)) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
  %Equal.sym(U32, U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), ap.xg(14, 11, p, q)) : {U32.xor(_, U32.xor(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
  %Equal.sym(U32, U32.xor(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s)), ap.xg(13, 9, r, s)) : {U32.xor(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), _) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
  ap.xg0(G.Gf8Bits.xor(G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 14, p)), G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 11, q))), G.Gf8Bits.xor(G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 13, r)), G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 9, s))))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m11
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m13
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m14
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m9
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xg
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xg0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.imix0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.m11
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.m13
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.m14
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.m9
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.aes
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.xor