GradientPROOF.decided_inv: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
Lines 454-477 of bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&start_line=454&end_line=477

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

def decided_inv(+remaining: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
  state: Gradient.State<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
  -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
  -same: Totality.SameSource(contribution, state_contribution(shape, state)),
  -rec: @state: Gradient.State<shape> -> @-inv: Inv(shape, original, contribution, 1n+cursor, state_total(shape, state)) ->
    @-same: Totality.SameSource(contribution, state_contribution(shape, state)) ->
    Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))>) ->
  Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.decided(shape, cursor, index, state,
    state => Gradient.loop(remaining, shape, 1n+cursor, state), decision))>:
  match decision:
    case Shape.BFalse{equal}:
      conversion_inv(shape, original, contribution, Nat.add(remaining, 1n+cursor), state)
    case Shape.BTrue{equal}:
      continue_inv(remaining, shape, original, contribution, cursor, Gradient.step(shape, index, state),
        {\{Holds: proof => proof} : Holds<StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))> ->
          StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))}(
          step_inv(shape, original, contribution, cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), state, inv, same)),
        {\{Holds: proof => proof} : Holds<Totality.SameSource(contribution, step_owner(shape, Gradient.step(shape, index, state)))> ->
          Totality.SameSource(contribution, step_owner(shape, Gradient.step(shape, index, state)))}(
          same_trans(contribution, state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)), same,
            {\{Holds: proof => proof} : Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))> ->
              Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))}(
              step_retains(shape, index, state)))),
        rec)

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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
  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/autograd/gradient.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient.bend&name=decided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient.bend&name=loop
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Inv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=LoopInv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=StepInv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=continue_inv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=conversion_inv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=same_trans
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=state_contribution
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=state_total
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=step_inv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=step_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=step_retains
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  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=Dynamic
  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/elementwise_totality.bend&name=SameSource
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=natural_equal