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

import Base

def ap.isb(+x: U32, +y: U32, +e: {x == U32.and(255, y) : U32}) -> {x == U32.and(255, x) : U32}:
  %Equal.sym(U32, x, U32.and(255, y), e) : {_ == U32.and(255, _) : U32}
  Equal.sym(U32, U32.and(255, U32.and(255, y)), U32.and(255, y), ap.bb(y))

Uses (4):
  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