ProjectionProofs.walk_right_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as ProjectionProofs
Lines 150-166 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=150&end_line=166

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates

def walk_right_value(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast<left, right, output>, +index: Shape.Fin(Shape.numel(output))) -> {Shape.walk_right(Shape.index_table(left, right, output), Shape.Fin.value(Shape.numel(output), index)) == Shape.row_major(right, Shape.project_right(left, right, output, alignment, Shape.unflatten(output, index))) : Nat}:
  +value = Shape.Fin.value(Shape.numel(output), index)
  +ds = Shape.digits(output, value)
  +nl = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left))
  +nr = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right))
  +coordinate = Shape.unflatten(output, index)
  +projected = Shape.project_right(left, right, output, alignment, coordinate)
  +strides = strides_of(right)
  +dropped = List.drop(&2, Nat, ds, nr)
  %Equal.sym(Nat, Shape.walk_right(Shape.index_rows(Shape.pad(nl, left), Shape.pad(nr, right), output), value), dot(strides_of(Shape.pad(nr, right)), ds), walk_right_rows(Shape.pad(nl, left), Shape.pad(nr, right), output, value, left_padded(left, right, output, alignment))) : {_ == Shape.row_major(right, projected) : Nat}
  %Equal.cong(List<&2, Nat>, Nat, steps => dot(steps, ds), zeros(nr, strides), strides_of(Shape.pad(nr, right)), Equal.sym(List<&2, Nat>, strides_of(Shape.pad(nr, right)), zeros(nr, strides), pad_strides(nr, right))) : {_ == Shape.row_major(right, projected) : Nat}
  %Equal.sym(Nat, dot(zeros(nr, strides), ds), dot(strides, dropped), dot_zeros(nr, ds, strides)) : {_ == Shape.row_major(right, projected) : Nat}
  %Equal.sym(Nat, dot(strides, dropped), Shape.offset(right, Shape.broadcast_indices(right, dropped)), dot_broadcast(right, dropped)) : {_ == Shape.row_major(right, projected) : Nat}
  %Equal.cong(Nat, Nat, width => Shape.offset(right, Shape.broadcast_indices(right, List.drop(&2, Nat, ds, Nat.sub(width, List.length(&2, Nat, right))))), List.length(&2, Nat, ds), List.length(&2, Nat, output), digits_length(output, value)) : {_ == Shape.row_major(right, projected) : Nat}
  %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(right, Shape.project_indices(right, values)), Shape.indices(output, coordinate), ds, Coordinates.digits_unflatten(output, index)) : {_ == Shape.row_major(right, projected) : Nat}
  %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(right, values), Shape.indices(right, projected), Shape.project_indices(right, Shape.indices(output, coordinate)), Broadcast.project_right(left, right, output, alignment, coordinate)) : {_ == Shape.row_major(right, projected) : Nat}
  Coordinates.offset_indices(right, projected)

Uses (35):
  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.drop
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=project_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=digits_unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=offset_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_indices
  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=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices
  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=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=project_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=project_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=row_major
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten
  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=digits_length
  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=dot_broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=dot_zeros
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=left_padded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=pad_strides
  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/projection_proofs.bend&name=walk_right_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=zeros