def actual_admission

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:1048

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

1048def actual_admission(+left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1049  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1050  -valid: Totality.MatrixInputs<left, right>) -> Totality.MatrixBounds<rows, inner, right_inner, columns>:
1051  Totality.MatrixBounds{
1052    {\{Totality.MatrixInputs: old_rows => old_inner => old_right_inner => old_columns => old_le => old_re => compatible => supported =>
1053      Equal.trans(Nat, U32.to_nat(inner), U32.to_nat(old_inner), U32.to_nat(right_inner),
1054        Equal.cong(U32, Nat, U32.to_nat, inner, old_inner, second_equal(rows, inner, old_rows, old_inner,
1055          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))),
1056        Equal.trans(Nat, U32.to_nat(old_inner), U32.to_nat(old_right_inner), U32.to_nat(right_inner), compatible,
1057          Equal.cong(U32, Nat, U32.to_nat, old_right_inner, right_inner, Equal.sym(U32, right_inner, old_right_inner,
1058            first_equal(right_inner, columns, old_right_inner, old_columns,
1059              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))))))} :
1060                Totality.MatrixInputs<left, right> -> {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}}(valid),
1061    {\{Totality.MatrixInputs: old_rows => old_inner => old_right_inner => old_columns => old_le => old_re => compatible => supported =>
1062      %Equal.sym(U32, rows, old_rows, first_equal(rows, inner, old_rows, old_inner,
1063        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))) :
1064          Shape.LE(Shape.logical_numel([_, columns]), 1048576n)
1065      %Equal.sym(U32, columns, old_columns, second_equal(right_inner, columns, old_right_inner, old_columns,
1066        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))) :
1067          Shape.LE(Shape.logical_numel([old_rows, _]), 1048576n)
1068      supported} : Totality.MatrixInputs<left, right> -> Shape.LE(Shape.logical_numel([rows, columns]), 1048576n)}(valid)}