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

import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-collections@1.0.0.0/src/crypto/aes/types.bend as TT

def ap.ismask(+x: TT.State, +v: TT.State, +e: {x == X.aes.mask(v) : TT.State}) -> {x == X.aes.mask(x) : TT.State}:
  %Equal.sym(TT.State, x, X.aes.mask(v), e) : {_ == X.aes.mask(_) : TT.State}
  Equal.sym(TT.State, X.aes.mask(X.aes.mask(v)), X.aes.mask(v), ap.mm(v))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask