PROOF.ap.m11: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 1807-1810 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=1807&end_line=1810

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.m11(+x: U32) -> {X.aes.m11(x) == G.Gf8.mul(G.Gf8.aes(), 11, x) : U32}:
  %Equal.sym(U32, U32.and(255, x), U32.and(255, U32.and(255, x)), Equal.sym(U32, U32.and(255, U32.and(255, x)), U32.and(255, x), ap.bb(x))) : {X.aes.c11(_) == G.Gf8.mul(G.Gf8.aes(), 11, x) : U32}
  %ap.glo(11, x) : {X.aes.c11(U32.and(255, U32.and(255, x))) == _ : U32}
  ap.m11b(x)

Uses (10):
  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.and
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.bb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.glo
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m11b
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.c11
  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-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