PROOF.tr.split_eq: def of bend-osdev-cipher-modes@0.1.0.0
Import: import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
Lines 1001-1002 of bend-osdev-cipher-modes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&start_line=1001&end_line=1002

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}:
  Equal.sym(M.CmSplit, M.cm.split.fast(xs), M.cm.split(xs), Equal.trans(M.CmSplit, M.cm.split.go(xs, Nil{}), tr.split_fin(Nil{}, M.cm.split(xs)), M.cm.split(xs), tr.split_go(xs, Nil{}), tr.split_fin_nil(M.cm.split(xs))))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_fin
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_fin_nil
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmSplit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.split.fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.split.go