ProjectionProofs.walk_right_rows: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as ProjectionProofs
Lines 50-64 of bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&start_line=50&end_line=64

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as Unique

def walk_right_rows(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +index: Nat, same: {List.length(&2, Nat, left) == List.length(&2, Nat, output) : Nat}) -> {Shape.walk_right(Shape.index_rows(left, right, output), index) == dot(strides_of(right), Shape.digits(output, index)) : Nat}:
  match left right output:
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      +stride = Shape.numel(ot)
      Equal.cong(Nat, Nat, rest => Nat.add(Nat.mul(Shape.broadcast_index(rh, Shape.numel(rt)), Nat.div(index, stride)), rest), Shape.walk_right(Shape.index_rows(lt, rt, ot), Nat.mod(index, stride)), dot(strides_of(rt), Shape.digits(ot, Nat.mod(index, stride))), walk_right_rows(lt, rt, ot, Nat.mod(index, stride), Unique.succ_injective(List.length(&2, Nat, lt), List.length(&2, Nat, ot), same)))
    case Nil{} Nil{} Nil{}:
      {==}
    case Nil{} rh <> rt Nil{}:
      {==}
    case Nil{} right oh <> ot:
      Empty.absurd({Shape.walk_right(Shape.index_rows(Nil{}, right, oh <> ot), index) == dot(strides_of(right), Shape.digits(oh <> ot, index)) : Nat}, Unique.succ_zero(List.length(&2, Nat, ot), Equal.sym(Nat, 0n, 1n+List.length(&2, Nat, ot), same)))
    case lh <> lt Nil{} output:
      {==}
    case lh <> lt rh <> rt Nil{}:
      {==}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=dot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=strides_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=succ_injective
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=succ_zero