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

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.m13(+x: U32) -> {X.aes.m13(x) == G.Gf8.mul(G.Gf8.aes(), 13, 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.c13(_) == G.Gf8.mul(G.Gf8.aes(), 13, x) : U32}
  %ap.glo(13, x) : {X.aes.c13(U32.and(255, U32.and(255, x))) == _ : U32}
  ap.m13b(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.m13b
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.c13
  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-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