BatchedMatmulPROOF.batch_number_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 358-368 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=358&end_line=368

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched

# The batch number of the build reads each operand's batch as the shape
# module broadcasts it.
def batch_number_spec(+first: Nat, +second: Nat, +b1: Nat, +b2: Nat) ->
  {Batched.batch_number(first, second, b1, b2) == Nat.add(Nat.mul(Shape.broadcast_index(first, b1), second), Shape.broadcast_index(second, b2)) : Nat}:
  %Equal.sym(Nat, Batched.stretch(b1, Nat.is_eq(first, 1n)), Shape.broadcast_index(first, b1), stretch_spec(first, b1)) :
    {Nat.add(Nat.mul(_, second), Batched.stretch(b2, Nat.is_eq(second, 1n))) ==
      Nat.add(Nat.mul(Shape.broadcast_index(first, b1), second), Shape.broadcast_index(second, b2)) : Nat}
  %Equal.sym(Nat, Batched.stretch(b2, Nat.is_eq(second, 1n)), Shape.broadcast_index(second, b2), stretch_spec(second, b2)) :
    {Nat.add(Nat.mul(Shape.broadcast_index(first, b1), second), _) ==
      Nat.add(Nat.mul(Shape.broadcast_index(first, b1), second), Shape.broadcast_index(second, b2)) : Nat}
  {==}

Uses (9):
  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.is_eq
  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/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=stretch
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=stretch_spec