def inverse_observation_mapped
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:2265
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/transform_totality.bend as Totality
2265def inverse_observation_mapped(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2266 +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>,
2267 -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -middle: Core.Tensor<Layout.output(input, axes, plan)>,
2268 -middle_retained: Core.Tensor<Layout.output(input, axes, plan)>,
2269 -restored: Core.Tensor<Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)>, +index: U32,
2270 +second: Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>,
2271 -second_exact: {Done{second} == Layout.map_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index) :
2272 Result<&2, &2, Layout.Error, Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>>},
2273 +first: Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>,
2274 -first_exact: {Done{first} == Layout.map_index(input, axes, plan,
2275 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) :
2276 Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>>},
2277 -first_prefix: Transforms.Prefix<input, axes, plan, original, retained, middle, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
2278 -second_prefix: Transforms.Prefix<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, middle_retained, restored,
2279 Shape.logical_numel(Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)))>,
2280 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}) ->
2281 Totality.RestoreObservation<input, Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), original, restored, index>:
2282 Totality.RestoreObservation{
2283 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index),
2284 Transforms.expected_output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, index), Core.observe(input, original, index),
2285 {\{Totality.CopyObservation: equal => equal} :
2286 Totality.CopyObservation<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, restored, index> ->
2287 {Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index) ==
2288 Transforms.expected_output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, index) : Maybe<&2, F32>}}(
2289 prefix_observation(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, middle_retained, restored, index, second_prefix,
2290 %Equal.sym(List<&2, U32>, Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)), Shape.dimensions(input),
2291 Laws.inverse_permutation_dimensions(input, axes, plan, inverse)) : {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
2292 inside)),
2293 %second_exact : {Transforms.expected_mapped(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, middle, _) == Core.observe(input, original, index) : Maybe<&2, F32>}
2294 Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), middle,
2295 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)),
2296 Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)), Core.observe(input, original, index),
2297 {\{ObserveBridge: equal => equal} : ObserveBridge<Layout.output(input, axes, plan), middle,
2298 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)> ->
2299 {Core.checked_observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) ==
2300 Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) : Maybe<&2, F32>}}(
2301 logical_observe_bridge(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2302 Laws.mapped_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
2303 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)),
2304 Transforms.expected_output(input, axes, plan, original, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)), Core.observe(input, original, index),
2305 {\{Totality.CopyObservation: equal => equal} : Totality.CopyObservation<input, axes, plan, original, middle,
2306 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)> ->
2307 {Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) ==
2308 Transforms.expected_output(input, axes, plan, original, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) : Maybe<&2, F32>}}(
2309 prefix_observation(input, axes, plan, original, retained, middle,
2310 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first_prefix,
2311 Laws.mapped_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
2312 %first_exact : {Transforms.expected_mapped(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), original, _) == Core.observe(input, original, index) : Maybe<&2, F32>}
2313 %Equal.sym(U32, Layout.source_index(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first), index,
2314 Laws.inverse_mapping_restores_index(input, axes, plan, inverse, index, second, first)) : {Core.checked_observe(input, original, _) == Core.observe(input, original, index) : Maybe<&2, F32>}
2315 {\{ObserveBridge: equal => equal} : ObserveBridge<input, original, index> ->
2316 {Core.checked_observe(input, original, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}(
2317 logical_observe_bridge(input, original, index, inside)))))}