ReductionPROOF.sum_source_result: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 615-636 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=615&end_line=636

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/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws

def sum_source_result(+shape: Shape.Shape, -original: Core.Tensor<shape>,
  result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
  -source: Laws.SourceSum<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0, result>,
  -preservation: Laws.Preserved<shape, original, result>) -> Laws.SourceSumResult<shape, original, Reduction.sum_result(shape, result)>:
  match result:
    case Fail{error}:
      Laws.SourceSumResult{unit => Unit{}}
    case Done{pair}:
      (retained, +value) = pair
      Laws.SourceSumResult{unit =>
        prove : @certificates: Laws.SourceSum<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0,
          (Done{(retained, value)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>)> &
          Laws.Preserved<shape, original, (Done{(retained, value)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>)> ->
          Laws.SumResultMeaning(shape, original, Reduction.sum_result(shape, Done{(retained, value)})) =
          \{Tuple: \{Laws.SourceSum: meaning => \{Laws.Preserved: kept =>
            build : @meaning: Laws.SumMeaning<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0, value> ->
              Laws.SumResultMeaning(shape, original, Reduction.sum_result(shape, Done{(retained, value)})) =
              \{Laws.SumMeaning: values => logical => fold =>
                Laws.SumResult{values, logical,
                  Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, value, Reduction.sequential_sum(values, 0.0), fold), kept}}
            build(meaning(Unit{}))}}}
        prove((source, preservation))}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  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=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  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=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=sequential_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=sum_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=Preserved
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SourceSum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SourceSumResult
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SumMeaning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SumResult
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SumResultMeaning