ReducePROOF.zero_inv: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
Lines 129-140 of bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&start_line=129&end_line=140

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/construction_contract_PROOF.bend as ConstructionProof
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation

def zero_inv(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +target: Shape.Shape, output: Core.Tensor<target>,
  -same: {Done{output} == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>}) ->
  Holds<Inv(plan, values, target, 0n, output)>:
  Holds{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(target, output, index),
    Core.read_value(target, Core.read_flat(target, output, index)), Some{0.0},
    Equal.sym(Maybe<&2, F32>, Core.read_value(target, Core.read_flat(target, output, index)), Core.checked_observe(target, output, index),
      {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<target, output, index> ->
        {Core.read_value(target, Core.read_flat(target, output, index)) == Core.checked_observe(target, output, index) : Maybe<&2, F32>}}(
        Core.source_read_model(target, output, index))),
    %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{output}, Core.new(target, 0.0), same) :
      {Observation.point(target, index, _) == Some{0.0} : Maybe<&2, F32>}
    ConstructionProof.point_value(target, 0.0, index, inside))}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=Inv
  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=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_contract_PROOF.bend&name=point_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=SourceRead
  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/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=new
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_flat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=source_read_model
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=point