TransformPROOF.transpose_observation_mapped: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF Lines 2391-2434 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=2391&end_line=2434 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 def transpose_observation_mapped(+input: Shape.Shape, +a: U32, +b: U32, +plan: Layout.Plan, -original: Core.Tensor, -retained: Core.Tensor, -target: Core.Tensor, +index: U32, +mapping: Layout.Mapping, -map_exact: {Done{mapping} == Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}, -prefix: Transforms.Prefix, +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}, +axes_inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) -> Totality.TransposeObservation: Totality.TransposeObservation{ Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index), Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index), 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)), {\{Totality.CopyObservation: equal => equal} : Totality.CopyObservation -> {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) == Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index) : Maybe<&2, F32>}}( prefix_observation(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, retained, target, index, prefix, inside)), Equal.trans(Maybe<&2, F32>, Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index), Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)), 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)), 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)), Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index), Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping>, Maybe<&2, F32>, Transforms.expected_mapped(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, original), Done{mapping}, Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index), map_exact)), 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)), Core.observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)), 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)), {\{ObserveBridge: equal => equal} : ObserveBridge -> {Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)) == Core.observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)) : Maybe<&2, F32>}}( logical_observe_bridge(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping), Laws.mapped_mathematical_bounded(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping))), Equal.cong(Maybe<&2, U32>, Maybe<&2, F32>, Totality.reference_observe(input, original), Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)}, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index), %TransposeProof.transpose_axes_requested(input, a, b, axes_inside) : {Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)} == Layout.reference_source_coordinates(Shape.dimensions(input), Axis.scatter(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(_), 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>} Laws.mapping_reference(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)))))} Uses (44): 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=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe 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=Result 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=digits 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=extents https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel 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=scatter https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Mapping 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=map_index 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=reference_source_coordinates https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=source_index 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/transform_LAWS.bend&name=mapped_mathematical_bounded https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend&name=mapping_reference https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=ObserveBridge https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=logical_observe_bridge https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=prefix_observation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=CopyObservation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=TransposeObservation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=reference_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=transpose_reference https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Prefix https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=expected_mapped https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=expected_output 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=valid