MatrixIndexProof.stepped_left: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
Lines 243-247 of bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&start_line=243&end_line=247

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

# A matmul cell steps its left offset by one word and its right offset by a
# row of `columns` words: the term after term k sits at the offsets of k + 1.
def stepped_left(+inner: Nat, +row: Nat, +k: Nat) ->
  {Nat.add(1n, Nat.add(Nat.mul(row, inner), k)) == Nat.add(Nat.mul(row, inner), 1n+k) : Nat}:
  Equal.sym(Nat, Nat.add(Nat.mul(row, inner), 1n+k), 1n+Nat.add(Nat.mul(row, inner), k), Arith.add_succ(Nat.mul(row, inner), k))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ