def step_retains

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:201

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_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient

201def step_retains(-shape: Shape.Shape, +index: U32, state: Gradient.State<shape>) ->
202  Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))>:
203  Gradient.State{contribution, total} = state
204  Holds{{\{ElementwiseProof.SourceModel: same =>
205    {\{Holds: proof => proof} :
206      Holds<Totality.SameSource(contribution, step_owner(shape, Gradient.step_contribution(shape, index, total, Core.read_dynamic(contribution, index))))> ->
207      Totality.SameSource(contribution, step_owner(shape, Gradient.step_contribution(shape, index, total, Core.read_dynamic(contribution, index))))}(
208      contribution_retains(shape, index, total, contribution, Core.read_dynamic(contribution, index), same))} :
209    ElementwiseProof.SourceModel<contribution, ElementwiseProof.dynamic_read_owner(Core.read_dynamic(contribution, index))> ->
210    Totality.SameSource(contribution, step_owner(shape, Gradient.step_contribution(shape, index, total, Core.read_dynamic(contribution, index))))}(
211    ElementwiseProof.dynamic_read_retains(contribution, index))}