def inverse_axes_naturals

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1995

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping

1995def inverse_axes_naturals(+input: Shape.Shape, +axes: List<&2, U32>, +accepted: {True{} == Layout.bijective(input, axes) : Bool}) ->
1996  {Shape.naturals(Totality.inverse_axes(input, axes)) == Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)) : List<&2, Nat>}:
1997  words_bounded_exact(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), Shape.rank(input),
1998    %Equal.sym(Nat, U32.to_nat(Shape.rank(input)), Shape.rank_dimensions(Shape.dimensions(input)), AxisAlgebra.rank_exact(input)) :
1999      {True{} == Axis.bounded(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), _) : Bool}
2000    Mapping.and_left(Axis.bounded(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(input))),
2001      Axis.unique(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
2002      Mapping.and_right(Nat.is_eq(List.length(&2, Nat, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.rank_dimensions(Shape.dimensions(input))),
2003        Bool.and(Axis.bounded(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(input))),
2004          Axis.unique(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))),
2005        AxisAlgebra.facts_inverse_valid(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), AxisAlgebra.shape_facts(input, axes, accepted)))))