GradientPROOF.loop_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 479-495 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=479&end_line=495

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
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 loop_inv(fuel: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, state: Gradient.State<shape>,
  -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
  -same: Totality.SameSource(contribution, state_contribution(shape, state))) ->
  Holds<LoopInv(shape, original, contribution, Nat.add(fuel, cursor), Gradient.loop(fuel, shape, cursor, state))>:
  match fuel:
    case 0n:
      Gradient.State{owner, total} = state
      Holds{({==}, inv)}
    case 1n+remaining:
      Holds{
        %Arith.add_succ(remaining, cursor) : LoopInv(shape, original, contribution, _, Gradient.loop(1n+remaining, shape, cursor, state))
        {\{Holds: proof => proof} :
          Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(1n+remaining, shape, cursor, state))> ->
          LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(1n+remaining, shape, cursor, state))}(
          decided_inv(remaining, shape, original, contribution, cursor, U32.from_nat(cursor), state,
            Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), inv, same,
            state => inv => same => loop_inv(remaining, shape, original, contribution, 1n+cursor, state, inv, same)))}

Uses (20):
  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=Sigma
  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/autograd/gradient.bend&name=State
  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_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=decided_inv
  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/shape/core.bend&name=Shape
  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/storage/arith.bend&name=add_succ
  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