def transpose_observation_mapped
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:2391
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
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/transform_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
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/transpose_PROOF.bend as TransposeProof
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as TransposeSpec
2391def transpose_observation_mapped(+input: Shape.Shape, +a: U32, +b: U32, +plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
2392 -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)>, +index: U32,
2393 +mapping: Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index>,
2394 -map_exact: {Done{mapping} == Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index) :
2395 Result<&2, &2, Layout.Error, Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index>>},
2396 -prefix: Transforms.Prefix<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, retained, target,
2397 Shape.logical_numel(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)))>,
2398 +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)))) == True{} : Bool},
2399 +axes_inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2400 Totality.TransposeObservation<input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), original, target, a, b, index>:
2401 Totality.TransposeObservation{
2402 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index),
2403 Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index),
2404 Totality.reference_observe(input, original, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)),
2405 {\{Totality.CopyObservation: equal => equal} :
2406 Totality.CopyObservation<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, target, index> ->
2407 {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
2408 Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index) : Maybe<&2, F32>}}(
2409 prefix_observation(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, retained, target, index, prefix, inside)),
2410 Equal.trans(Maybe<&2, F32>, Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index),
2411 Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2412 Totality.reference_observe(input, original, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)),
2413 Equal.sym(Maybe<&2, F32>, Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2414 Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index),
2415 Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index>>, Maybe<&2, F32>,
2416 Transforms.expected_mapped(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, original),
2417 Done{mapping}, Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index), map_exact)),
2418 Equal.trans(Maybe<&2, F32>, Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2419 Core.observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2420 Totality.reference_observe(input, original, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)),
2421 {\{ObserveBridge: equal => equal} :
2422 ObserveBridge<input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)> ->
2423 {Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)) ==
2424 Core.observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)) : Maybe<&2, F32>}}(
2425 logical_observe_bridge(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping),
2426 Laws.mapped_mathematical_bounded(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping))),
2427 Equal.cong(Maybe<&2, U32>, Maybe<&2, F32>, Totality.reference_observe(input, original),
2428 Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)},
2429 Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index),
2430 %TransposeProof.transpose_axes_requested(input, a, b, axes_inside) :
2431 {Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)} ==
2432 Layout.reference_source_coordinates(Shape.dimensions(input), Axis.scatter(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(_),
2433 Shape.words(Shape.digits(Shape.extents(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), U32.to_nat(index))), 0n)) : Maybe<&2, U32>}
2434 Laws.mapping_reference(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)))))}