BendMlLlama.read_len: law of bend-ml-llama@0.2.1.0 Import: import bend-ml-llama@0.2.1.0/main.bend as BendMlLlama Lines 700-710 of bend-ml-llama@0.2.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-llama@0.2.1.0/main.bend&start_line=700&end_line=710 import Base import bend-ml-tensor-array@0.1.19.0/main.bend as TA # LAW (read_len): reading m + 1 numbers of an array onto acc gives m + 1 more scores. # PROOF: by induction on m. With 0 left it reads one number onto acc (1 + the length of acc, by the definitions); # with 1 + p left it reads one and recurses one index down, and len_step moves the 1 out of the sum (tensor-array's # leaf_len, for scores). law read_len: for k: Array for +m: Nat for +idx: U32 for +acc: List<&2, F32> for rc: Array & F32 {sr_len(sr_of(k, TA.read_l(m, idx, acc, rc))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat} Uses (15): 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=F32 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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=bend-ml-llama@0.2.1.0/main.bend&name=sr_len https://jend.leeeet.dev/definition.txt?path=bend-ml-llama@0.2.1.0/main.bend&name=sr_of https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=len_step https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=read_l