ElementwisePROOF.loop_retains: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 393-415 of bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&start_line=393&end_line=415

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
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

def loop_retains(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
  -left: Core.Dynamic, -right: Core.Dynamic, state: Elementwise.State<Shape.output_shape(plan)>,
  -left_same: Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})),
  -right_same: Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))) ->
  Totality.Retention<left, right, Elementwise.loop(fuel, operation, plan, cursor, state)>:
  match fuel:
    case 0n:
      Elementwise.State{retained_left, retained_right, output} = state
      Totality.Retention{left_same, right_same}
    case 1n+remaining:
      loop_finish_retains(remaining, operation, plan, cursor, left, right, Elementwise.natural_step(operation, plan, cursor, state),
        {\{NaturalSources: l => r => NaturalSources{
          property => Equal.trans(Totality.Inspection,
            Totality.inspect(property, natural_left_owner(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))),
            Totality.inspect(property, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})), Totality.inspect(property, left), l(property), left_same(property)),
          property => Equal.trans(Totality.Inspection,
            Totality.inspect(property, natural_right_owner(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))),
            Totality.inspect(property, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})), Totality.inspect(property, right), r(property), right_same(property))}} :
          NaturalSources<Shape.output_shape(plan), cursor, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
            Elementwise.natural_step(operation, plan, cursor, state)> ->
          NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.natural_step(operation, plan, cursor, state)>}(
            natural_decided_retains(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state)),
        state => l => r => loop_retains(remaining, operation, plan, 1n+cursor, left, right, state, l, r))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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=bool_case
  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/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=loop
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=natural_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=NaturalSources
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=loop_finish_retains
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=natural_decided_retains
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=natural_left_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=natural_right_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_left_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_right_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=Inspection
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=Retention
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=SameSource
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=inspect