def transpose_output_inside

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

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/permutation_mapping.bend as Mapping
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as TransposeSpec

2478def transpose_output_inside(+input: Shape.Shape, +a: U32, +b: U32,
2479  +plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
2480  +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2481  {True{} == TransposeSpec.valid(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b) : Bool}:
2482  %Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))),
2483    Shape.rank_dimensions(Shape.dimensions(input)), Mapping.permutation_output_rank(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)) :
2484      {True{} == TransposeSpec.axes_valid(_, U32.to_nat(a), U32.to_nat(b)) : Bool}
2485  inside