TransposeLAWS.permute_source_transposed: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transpose_LAWS.bend as TransposeLAWS
Lines 31-45 of bendtorch-core@0.1.0.0/src/tensor/transpose_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_LAWS.bend&start_line=31&end_line=45

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values

# The index map of a rank-2 transpose reads the transposed cell. For an input
# of dimensions [rows, columns], output cell [j, l] of the [columns, rows]
# transpose sits at j * rows + l, and `permute_source` with axes [1, 0] sends
# it to input index l * columns + j, the input cell [l, j].
law permute_source_transposed:
  for +input: Shape.Shape
  for +rows: U32
  for +columns: U32
  for matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}
  for +j: Nat
  for j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}
  for +l: Nat
  for l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}
  {Values.permute_source(input, [1, 0], U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) ==
    Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  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/tensor/observation.bend&name=permute_source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend&name=permute_source_transposed