BatchedMatmulPROOF.output_nats: 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 693-710 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=693&end_line=710

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
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws

def output_nats(+rank: Nat, +o1: U32, +o2: U32, +first: Nat, +second: Nat,
  +e1: {U32.to_nat(o1) == first : Nat}, +e2: {U32.to_nat(o2) == second : Nat}, +rows: U32, +lv: Bool, +columns: U32, +rv: Bool) ->
  {Shape.naturals(List.append(&2, U32, Batched.batch_dims(rank, o1, o2), Batched.matrix_dims(rows, lv, columns, rv))) ==
    List.append(&2, Nat, batch_nats(rank, first, second),
      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}:
  %Equal.sym(List<&2, Nat>, Shape.naturals(List.append(&2, U32, Batched.batch_dims(rank, o1, o2), Batched.matrix_dims(rows, lv, columns, rv))),
    List.append(&2, Nat, Shape.naturals(Batched.batch_dims(rank, o1, o2)), Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv))),
    naturals_append(Batched.batch_dims(rank, o1, o2), Batched.matrix_dims(rows, lv, columns, rv))) :
    {_ == List.append(&2, Nat, batch_nats(rank, first, second),
      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}
  %Equal.sym(List<&2, Nat>, Shape.naturals(Batched.batch_dims(rank, o1, o2)), batch_nats(rank, first, second), batch_part(rank, o1, o2, first, second, e1, e2)) :
    {List.append(&2, Nat, _, Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv))) == List.append(&2, Nat, batch_nats(rank, first, second),
      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}
  %Equal.sym(List<&2, Nat>, Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv)),
    List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns))), matrix_part(rows, lv, columns, rv)) :
    {List.append(&2, Nat, batch_nats(rank, first, second), _) == List.append(&2, Nat, batch_nats(rank, first, second),
      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}
  {==}

Uses (15):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=batch_dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=matrix_dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=batch_nats
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=batch_part
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=matrix_part
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=naturals_append