law axis_inverse_reverse_composition

bendtorch-core@0.1.0.0 · src/tensor/axis_LAWS.bend:116

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis

116law axis_inverse_reverse_composition:
117  for -A: Data
118  for +rank: Nat
119  for +axes: List<&2, Nat>
120  for +items: List<&2, A>
121  for bound: Shape.LE(rank, 4n)
122  for accepted: {True{} == Axis.valid(rank, axes) : Bool}
123  for length: {List.length(&2, A, items) == rank : Nat}
124  {Axis.order(A, Axis.order(A, items, Axis.inverse_axes(rank, axes)), axes) == items : List<&2, A>}