PROOF.cnt_psm3: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF
Lines 201-205 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=201&end_line=205

import Base
import bendtorch@1.3.0.0/main.bend as T
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

# the whole softmax over 1 + kk numbers reports 1 + kk, whatever max and exp found (they are matched, not computed)
def cnt_psm3(q: Array<F32>, k: Array<F32>, +kk: Nat, +off: U32, r: T.AS) -> {T.pr_n(T.pr_of(q, k, T.psm3(kk, off, r))) == 1n+kk : Nat}:
  match r:
    case T.AS{a, +s}:
      Equal.trans(Nat, T.pr_n(T.pr_of(q, k, T.pdiv(kk, off, s, 0n, Array.get(F32, a, off)))), Nat.add(1n+kk, 0n), 1n+kk, cnt_div(q, k, kk, off, s, 0n, Array.get(F32, a, off)), NL.add_zero(1n+kk))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  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=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_div
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=AS
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=pdiv
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=pr_n
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=pr_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=psm3