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

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

# pw writes xs and counts them from n; the softmax prow3 runs on them reports 1 + (|xs| + n - 1)
def cnt_pw(+xs: List<&2, F32>, +idx: U32, +sc: F32, +n: Nat, +off: U32, q: Array<F32>, k: Array<F32>, p: Array<F32>) -> {T.pr_n(T.prow3(off, q, k, T.pw(xs, idx, sc, n, p))) == 1n+Nat.sub(Nat.add(List.length(&2, F32, xs), n), 1n) : Nat}:
  match xs:
    case Nil{}:
      cnt_psm2(q, k, Nat.sub(n, 1n), off, T.pmax0(Nat.sub(n, 1n), off, Array.get(F32, p, off)))
    case Con{+x, +t}:
      Equal.trans(Nat, T.pr_n(T.prow3(off, q, k, T.pw(t, (idx + 1 : U32), sc, 1n+n, Array.set(F32, p, idx, (x * sc : F32))))), 1n+Nat.sub(Nat.add(List.length(&2, F32, t), 1n+n), 1n), 1n+Nat.sub(1n+Nat.add(List.length(&2, F32, t), n), 1n), cnt_pw(t, (idx + 1 : U32), sc, 1n+n, off, q, k, Array.set(F32, p, idx, (x * sc : F32))), Equal.cong(Nat, Nat, z => 1n+Nat.sub(z, 1n), Nat.add(List.length(&2, F32, t), 1n+n), 1n+Nat.add(List.length(&2, F32, t), n), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), n), Nat.add(List.length(&2, F32, t), 1n+n), NL.add_succ(List.length(&2, F32, t), n))))

Uses (21):
  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=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_psm2
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=pmax0
  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=prow3
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=pw