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

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 loop_certificate(fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
  -original: Core.Tensor<input>, source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
  -prefix: Transforms.Prefix<input, axes, plan, original, source, target, cursor>) ->
  Transforms.LoopCertificate<input, axes, plan, original, fuel, cursor, source, target>:
  match fuel:
    case 0n:
      Transforms.LoopCertificate{(source, Done{target}), {==}, prefix}
    case 1n++remaining:
      loop_after_natural(remaining, input, axes, plan, cursor, original, source, target, prefix,
        natural_certificate(input, axes, plan, cursor, source, target),
        source => target => invariant => loop_certificate(remaining, input, axes, plan, 1n+cursor, original, source, target, invariant))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=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/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/transform_PROOF.bend&name=loop_after_natural
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=natural_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=LoopCertificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Prefix