TransformPROOF.inverse_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 2265-2317 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=2265&end_line=2317

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

def inverse_observation_mapped(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
  +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>,
  -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -middle: Core.Tensor<Layout.output(input, axes, plan)>,
  -middle_retained: Core.Tensor<Layout.output(input, axes, plan)>,
  -restored: Core.Tensor<Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)>, +index: U32,
  +second: Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>,
  -second_exact: {Done{second} == Layout.map_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index) :
    Result<&2, &2, Layout.Error, Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>>},
  +first: Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>,
  -first_exact: {Done{first} == Layout.map_index(input, axes, plan,
    Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) :
      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)>>},
  -first_prefix: Transforms.Prefix<input, axes, plan, original, retained, middle, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
  -second_prefix: Transforms.Prefix<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, middle_retained, restored,
    Shape.logical_numel(Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)))>,
  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}) ->
  Totality.RestoreObservation<input, Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), original, restored, index>:
  Totality.RestoreObservation{
  Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index),
    Transforms.expected_output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, index), Core.observe(input, original, index),
    {\{Totality.CopyObservation: equal => equal} :
      Totality.CopyObservation<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, restored, index> ->
        {Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index) ==
          Transforms.expected_output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, index) : Maybe<&2, F32>}}(
            prefix_observation(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, middle_retained, restored, index, second_prefix,
              %Equal.sym(List<&2, U32>, Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)), Shape.dimensions(input),
                Laws.inverse_permutation_dimensions(input, axes, plan, inverse)) : {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
              inside)),
    %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>}
    Equal.trans(Maybe<&2, F32>, 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)),
      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),
      {\{ObserveBridge: equal => equal} : ObserveBridge<Layout.output(input, axes, plan), middle,
        Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)> ->
          {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)) ==
            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>}}(
              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),
                Laws.mapped_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
      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)),
        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),
        {\{Totality.CopyObservation: equal => equal} : Totality.CopyObservation<input, axes, plan, original, middle,
          Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)> ->
            {Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) ==
              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>}}(
                prefix_observation(input, axes, plan, original, retained, middle,
                  Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first_prefix,
                  Laws.mapped_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
        %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>}
        %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,
          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>}
        {\{ObserveBridge: equal => equal} : ObserveBridge<input, original, index> ->
          {Core.checked_observe(input, original, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}(
            logical_observe_bridge(input, original, index, inside)))))}

Uses (34):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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.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=dimensions
  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/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=source_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend&name=inverse_mapping_restores_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend&name=inverse_permutation_dimensions
  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_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=RestoreObservation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=inverse_axes
  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