CorePROOF.loop_after_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 951-972 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=951&end_line=972

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 loop_after_certificate(+remaining: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original: Elementwise.State<Shape.output_shape(plan)>,
  -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, original),
  certificate: Elementwise.NaturalCertificate<operation, plan, cursor, original>,
  rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
    @-invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state) ->
      Elementwise.LoopCertificate<remaining, operation, plan, 1n+cursor, original_left, original_right, state>) ->
  Elementwise.LoopCertificate<1n+remaining, operation, plan, cursor, original_left, original_right, original>:
  Elementwise.NaturalCertificate{result, exact, meaning} = certificate
  match result:
    case Elementwise.NaturalStop{left, right, error}:
      Elementwise.LoopCertificate{((left, right), Fail{error}),
        Equal.cong(Elementwise.NaturalStep<Shape.output_shape(plan), cursor>, (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
          step => Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(remaining, operation, plan, 1n+cursor, state), step),
          Elementwise.NaturalStop{left, right, error}, Elementwise.natural_step(operation, plan, cursor, original), exact), Unit{}}
    case Elementwise.NaturalContinue{state, index, converted}:
      loop_continue_certificate(remaining, operation, plan, cursor, original_left, original_right, original, state, index, converted, exact,
        rec(state,
          {\{Elementwise.InvariantModel: invariant => invariant} :
            Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, state> ->
              Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state)}(invariant_advance(operation, plan, original_left, original_right, cursor, index, converted,
                original, state, invariant, meaning))))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=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=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=invariant_advance
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=loop_continue_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=InvariantModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=LoopCertificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=NaturalCertificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=NaturalStep
  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=StateInvariant
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=finish_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=loop
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=natural_step