BatchedMatmulPROOF.right_start_spec: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedMatmulPROOF
Lines 420-453 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&start_line=420&end_line=453

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

def right_start_spec(+lo: Matrix.Order, +ro: Matrix.Order, +inner: Nat, +rows: Nat, +columns: Nat, +l1: Nat, +l2: Nat, +r1: Nat, +r2: Nat, +o2: Nat,
  +b1: Nat, +b2: Nat, +row: Nat, +column: Nat,
  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +column_below: {Nat.is_lt(column, columns) == True{} : Bool},
  +batch_below: {Nat.is_lt(b2, o2) == True{} : Bool}) ->
  {Batched.right_start(Laws.layout_of(lo, ro, inner, rows, columns, l1, l2, r1, r2, o2), Laws.cell_position(o2, rows, columns, b1, b2, row, column)) ==
    Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}:
  +q = Nat.add(Nat.mul(b1, o2), b2)
  +r = Nat.add(Nat.mul(row, columns), column)
  +rc = Nat.mul(rows, columns)
  +within = MatrixIndex.lt_mul_add(row, rows, column, columns, row_below, column_below)
  %Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(q, rc), r), rc), q, div_exact(q, rc, r, within)) :
    {right_from(ro, inner, rows, columns, r1, r2, o2, _, Nat.mod(Nat.add(Nat.mul(q, rc), r), rc)) == Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, rc), r), rc), r, mod_exact(q, rc, r, within)) :
    {right_from(ro, inner, rows, columns, r1, r2, o2, q, _) == Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Nat.div(q, o2), b1, div_exact(b1, o2, b2, batch_below)) :
    {Nat.add(Nat.mul(Batched.batch_number(r1, r2, _, Nat.mod(q, o2)), Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, Nat.mod(r, columns), 0n)) ==
      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Nat.mod(q, o2), b2, mod_exact(b1, o2, b2, batch_below)) :
    {Nat.add(Nat.mul(Batched.batch_number(r1, r2, b1, _), Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, Nat.mod(r, columns), 0n)) ==
      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Nat.mod(r, columns), column, mod_exact(row, columns, column, column_below)) :
    {Nat.add(Nat.mul(Batched.batch_number(r1, r2, b1, b2), Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, _, 0n)) ==
      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Batched.batch_number(r1, r2, b1, b2), Nat.add(Nat.mul(Shape.broadcast_index(r1, b1), r2), Shape.broadcast_index(r2, b2)),
    batch_number_spec(r1, r2, b1, b2)) :
    {Nat.add(Nat.mul(_, Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, column, 0n)) ==
      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Matrix.read_offset(ro, inner, columns, column, 0n), Laws.matrix_offset(ro, inner, columns, column, 0n), read_offset_spec(ro, inner, columns, column, 0n)) :
    {Nat.add(Nat.mul(Nat.add(Nat.mul(Shape.broadcast_index(r1, b1), r2), Shape.broadcast_index(r2, b2)), Nat.mul(inner, columns)), _) ==
      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  %Equal.sym(Nat, Nat.mul(inner, columns), Nat.mul(columns, inner), Nats.mul_comm(inner, columns)) :
    {Nat.add(Nat.mul(Nat.add(Nat.mul(Shape.broadcast_index(r1, b1), r2), Shape.broadcast_index(r2, b2)), _), Laws.matrix_offset(ro, inner, columns, column, 0n)) ==
      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
  {==}

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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/nat_proofs.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=batch_number
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=right_start
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=cell_position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=layout_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=matrix_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=operand_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=batch_number_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=div_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=mod_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=read_offset_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=right_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Order
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=read_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=lt_mul_add