Memory.leaf_slots: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
Lines 100-107 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&start_line=100&end_line=107

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/proofs/lib/nat.bend as N

def leaf_slots(+ws: List<&2, U32>, +h: {SC.length(U32, ws) == 1n : Nat}) -> {Con{nthv(ws, 0n), Nil{}} == ws : List<&2, U32>}:
  match ws:
    case Nil{}:
      Empty.absurd({Con{nthv(Nil{}, 0n), Nil{}} == Nil{} : List<&2, U32>}, N.zero_succ(0n, h))
    case Con{x, Nil{}}:
      {==}
    case Con{x, Con{y, r}}:
      Empty.absurd({Con{nthv(Con{x, Con{y, r}}, 0n), Nil{}} == Con{x, Con{y, r}} : List<&2, U32>}, N.succ_zero(SC.length(U32, r), N.succ_inj(1n+SC.length(U32, r), 0n, h)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=nthv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=succ_inj
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=succ_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=zero_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length