MatmulPROOF.actual_admission: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 1048-1068 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=1048&end_line=1068

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality

def actual_admission(+left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
  -valid: Totality.MatrixInputs<left, right>) -> Totality.MatrixBounds<rows, inner, right_inner, columns>:
  Totality.MatrixBounds{
    {\{Totality.MatrixInputs: old_rows => old_inner => old_right_inner => old_columns => old_le => old_re => compatible => supported =>
      Equal.trans(Nat, U32.to_nat(inner), U32.to_nat(old_inner), U32.to_nat(right_inner),
        Equal.cong(U32, Nat, U32.to_nat, inner, old_inner, second_equal(rows, inner, old_rows, old_inner,
          Equal.trans(List<&2, U32>, [rows, inner], Shape.dimensions(left), [old_rows, old_inner], Equal.sym(List<&2, U32>, Shape.dimensions(left), [rows, inner], le), old_le))),
        Equal.trans(Nat, U32.to_nat(old_inner), U32.to_nat(old_right_inner), U32.to_nat(right_inner), compatible,
          Equal.cong(U32, Nat, U32.to_nat, old_right_inner, right_inner, Equal.sym(U32, right_inner, old_right_inner,
            first_equal(right_inner, columns, old_right_inner, old_columns,
              Equal.trans(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), [old_right_inner, old_columns], Equal.sym(List<&2, U32>, Shape.dimensions(right), [right_inner, columns], re), old_re))))))} :
                Totality.MatrixInputs<left, right> -> {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}}(valid),
    {\{Totality.MatrixInputs: old_rows => old_inner => old_right_inner => old_columns => old_le => old_re => compatible => supported =>
      %Equal.sym(U32, rows, old_rows, first_equal(rows, inner, old_rows, old_inner,
        Equal.trans(List<&2, U32>, [rows, inner], Shape.dimensions(left), [old_rows, old_inner], Equal.sym(List<&2, U32>, Shape.dimensions(left), [rows, inner], le), old_le))) :
          Shape.LE(Shape.logical_numel([_, columns]), 1048576n)
      %Equal.sym(U32, columns, old_columns, second_equal(right_inner, columns, old_right_inner, old_columns,
        Equal.trans(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), [old_right_inner, old_columns], Equal.sym(List<&2, U32>, Shape.dimensions(right), [right_inner, columns], re), old_re))) :
          Shape.LE(Shape.logical_numel([old_rows, _]), 1048576n)
      supported} : Totality.MatrixInputs<left, right> -> Shape.LE(Shape.logical_numel([rows, columns]), 1048576n)}(valid)}

Uses (15):
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=MatrixBounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=MatrixInputs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=first_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=second_equal