CorePROOF.step_indices_certificate: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 609-628 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=609&end_line=628

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

def step_indices_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
  state: Elementwise.State<Shape.output_shape(plan)>, result: Result<&2, &1, Core.Error, U32 & U32>,
  exact: {result == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}) -> Elementwise.StepCertificate<operation, plan, index, state>:
  Elementwise.State{left, right, output} = state
  match result:
    case Fail{error}:
      Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
        Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Elementwise.Step<Shape.output_shape(plan)>,
          input => Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, input),
          Fail{error}, Elementwise.input_indices(plan, index), exact), Unit{}}
    case Done{indices}:
      (+left_index, +right_index) = indices
      step_left_certificate(operation, plan, index, left, right, output, left_index, right_index, exact,
        result => equality => Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
          Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, Done{(left_index, right_index)}),
          Elementwise.step(operation, plan, index, Elementwise.State{left, right, output}), equality,
          Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Elementwise.Step<Shape.output_shape(plan)>,
            input => Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, input),
            Done{(left_index, right_index)}, Elementwise.input_indices(plan, index), exact)),
        Core.dynamic_read_certificate(left, left_index))

Uses (19):
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=dynamic_read_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_left_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=StepCertificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=input_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step_indices