ReductionPROOF.source_pair: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF Lines 559-589 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=559&end_line=589 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 source_pair(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor, +cursor: Nat, +accumulator: F32, -rec: @tensor: Core.Tensor -> @+value: F32 -> Laws.SourceSum, -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}, certificate: Core.Read, -source: Core.SourceRead, -retention: Core.SourceReadKeeps) -> Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape, tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))>: Core.Read{tensor, +result, +exact} = certificate Laws.SourceSum{unit => claim : @certificate: Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape, tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))> -> Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape, tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))) = \{Laws.SourceSum: proof => proof(Unit{})} prove : @certificates: Core.SourceRead & Core.SourceReadKeeps -> Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape, tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))) = \{Tuple: \{Core.SourceRead: meaning => \{Core.SourceReadKeeps: kept => %exact : Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape, tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, _)) claim(source_read(fuel, shape, original, cursor, accumulator, tensor, result, rec, exact_cursor, Equal.trans(Maybe<&2, F32>, Core.result_value(result), Core.read_value(shape, Core.read_flat(shape, original, U32.from_nat(cursor))), Core.checked_observe(shape, original, U32.from_nat(cursor)), Equal.cong(Core.Tensor & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair), (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), meaning), other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other), Core.retained_read_observe(shape, Core.read_flat(shape, original, U32.from_nat(cursor)), other), Core.checked_observe(shape, original, other), Equal.cong(Core.Tensor & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other), (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), kept(other))))}}} prove((source, retention))} Uses (27): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat 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=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat 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/tensor/core.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Read 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=SourceReadKeeps 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=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=result_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=retained_read_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=natural_sum_loop https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=read_step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LoopMeaning 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_PROOF.bend&name=source_read