PROOF.cnt_drow: def of bendtorch@1.3.0.0 Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF Lines 220-234 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=220&end_line=234 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 count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw def cnt_drow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2, +sc: F32, +off: U32, pa: Array) -> {T.pr_n(T.prow2(sc, off, pa, T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}: match m r: case 0n T.D2{a, b, +s}: +rw = T.rcat(s <> acc, Nil{}) +la = List.length(&2, F32, acc) Equal.trans(Nat, T.pr_n(T.prow3(off, a, b, T.pw(rw, off, sc, 0n, pa))), 1n+Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), 1n+la, cnt_pw(rw, off, sc, 0n, off, a, b, pa), Equal.cong(Nat, Nat, z => 1n+z, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), la, Equal.trans(Nat, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), Nat.sub(1n+la, 1n), la, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(List.length(&2, F32, rw), 0n), 1n+la, Equal.trans(Nat, Nat.add(List.length(&2, F32, rw), 0n), List.length(&2, F32, rw), 1n+la, NL.add_zero(List.length(&2, F32, rw)), Equal.trans(Nat, List.length(&2, F32, rw), Nat.add(1n+la, 0n), 1n+la, len_rcat(s <> acc, Nil{}), NL.add_zero(1n+la)))), sub0(la)))) case 1n++p T.D2{a, b, +s}: Equal.trans(Nat, T.pr_n(T.prow2(sc, off, pa, T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), cnt_drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b), sc, off, pa), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc))))) Uses (25): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array 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=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=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_pw https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=len_rcat https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=sub0 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=D2 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=dot0 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=drow 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=prow2 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 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=rcat