CorePROOF.step_right_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 549-579 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=549&end_line=579

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_right_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
  -original_left: Core.Dynamic, -original_right: Core.Dynamic,
  +left_index: U32, +right_index: U32, +left_value: F32,
  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
  certificate: Core.DynamicRead<original_right, right_index>,
  original_output: Core.Tensor<Shape.output_shape(plan)>,
  left: Core.Dynamic,
  -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
  lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
    {result == Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value,
      Core.read_dynamic(original_right, right_index)) : Elementwise.Step<Shape.output_shape(plan)>} ->
    {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>}) ->
  Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
  Core.DynamicRead{right, result, exact} = certificate
  match result:
    case Fail{error}:
      Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
        lift(Elementwise.Stop{left, right, error}, Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
          pair => Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, pair),
          (right, Fail{error}), Core.read_dynamic(original_right, right_index), exact)), Unit{}}
    case Done{+right_value}:
      step_write_certificate(operation, plan, index, original_left, original_right, original_output,
        left_index, right_index, left_value, right_value, indices_exact,
        Core.write_certificate(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), left, right, left_exact, exact,
        result => equality => lift(result,
          Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
            Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, (right, Done{right_value})),
            Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, Core.read_dynamic(original_right, right_index)), equality,
            Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
              pair => Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, pair),
              (right, Done{right_value}), Core.read_dynamic(original_right, right_index), exact))))

Uses (25):
  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=F32
  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=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=DynamicRead
  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=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=write_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_write_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=scalar
  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_right