TransformPROOF.prefix_written_case: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 306-328 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=306&end_line=328

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/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms

def prefix_written_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>,
  -original: Core.Tensor<input>, -before: Core.Tensor<Layout.output(input, axes, plan)>, -after: Core.Tensor<Layout.output(input, axes, plan)>,
  -cursor: Nat, +other: Nat,
  prior: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
    {Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(j)) ==
      Transforms.expected_output(input, axes, plan, original, U32.from_nat(j)) : Maybe<&2, F32>},
  current: {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(cursor)) ==
    Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)) : Maybe<&2, F32>},
  frame: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
    {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(j)) ==
      Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(j)) : Maybe<&2, F32>},
  split: Either<&2, &2, {Nat.is_lt(other, cursor) == True{} : Bool}, {other == cursor : Nat}>) ->
  {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(other)) ==
    Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)) : Maybe<&2, F32>}:
  match split:
    case Inl{+earlier}:
      Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(other)),
        Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(other)),
        Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)), frame(other, earlier), prior(other, earlier))
    case Inr{equal}:
      %Equal.sym(Nat, other, cursor, equal) : {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(_)) ==
        Transforms.expected_output(input, axes, plan, original, U32.from_nat(_)) : Maybe<&2, F32>}
      current

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  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
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_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/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/layout.bend&name=Plan
  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/transforms.bend&name=expected_output