Fill.lanes_len: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as Fill
Lines 297-304 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&start_line=297&end_line=304

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

def lanes_len(+n: Nat, +l: Nat, +r: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.lanes_go(n, l, r, s, p, q, sl, mm, t, mem)) == SC.length(A.Block, mem) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +rest:
      +m2 = SA.segment(r, s, l, p, q, sl, mm, t, mem)
      Equal.trans(Nat, SC.length(A.Block, SA.lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
        lanes_len(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, m2), segment_len(r, s, l, p, q, sl, mm, t, mem))

Uses (9):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&name=segment_len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=lanes_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=segment
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block