TransformPROOF.transpose_output_axes: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF Lines 2487-2512 of bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=2487&end_line=2512 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/transform_totality.bend as Totality import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping import bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend as TransposeProof import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as TransposeSpec def transpose_output_axes(+input: Shape.Shape, +a: U32, +b: U32, +plan: Layout.Plan, +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) -> {Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0) == Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) : List<&2, U32>}: Equal.trans(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0), TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)), Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Equal.trans(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0), TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))), U32.to_nat(a), U32.to_nat(b)), TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)), TransposeProof.transpose_axes_requested(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, transpose_output_inside(input, a, b, plan, inside)), Equal.cong(Nat, List<&2, U32>, rank => TransposeSpec.requested_axes(rank, U32.to_nat(a), U32.to_nat(b)), Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))), Shape.rank_dimensions(Shape.dimensions(input)), Mapping.permutation_output_rank(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))), Equal.trans(List<&2, U32>, TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)), Layout.transpose_axes(Shape.dimensions(input), a, b, 0), Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Equal.sym(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)), TransposeProof.transpose_axes_requested(input, a, b, inside)), Equal.sym(List<&2, U32>, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Layout.transpose_axes(Shape.dimensions(input), a, b, 0), Equal.trans(List<&2, U32>, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Shape.words(Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))), Layout.transpose_axes(Shape.dimensions(input), a, b, 0), Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))), Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), TransposeProof.inverse_axes(input, a, b, inside)), words_naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0)))))) Uses (25): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=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=naturals https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=inverse_axes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=transpose_axes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=permutation_output_rank https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=transpose_output_inside https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=words_naturals https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=inverse_axes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend&name=inverse_axes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend&name=transpose_axes_requested https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend&name=requested_axes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend&name=valid