def cnt_drow

bendtorch@1.3.0.0 · PROOF.bend:220

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

220# the count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw
221def 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<F32>) -> {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}:
222  match m r:
223    case 0n T.D2{a, b, +s}:
224      +rw = T.rcat(s <> acc, Nil{})
225      +la = List.length(&2, F32, acc)
226      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),
227        Equal.cong(Nat, Nat, z => 1n+z, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), la,
228          Equal.trans(Nat, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), Nat.sub(1n+la, 1n), la,
229            Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(List.length(&2, F32, rw), 0n), 1n+la,
230              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)),
231                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)))),
232            sub0(la))))
233    case 1n++p T.D2{a, b, +s}:
234      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)))))