ReductionPROOF.logical_keeps: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 49-64 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=49&end_line=64

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_LAWS.bend as Laws

def logical_keeps(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
  values: List<&2, F32>, logical: Laws.LogicalValues(fuel, shape, original, cursor, values),
  -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
  Laws.LogicalValues(fuel, shape, tensor, cursor, values):
  match fuel values:
    case 0n Nil{}:
      Unit{}
    case 1n+tail +value <> rest:
      Laws.LogicalStep{exact, observed, remaining} = logical
      Laws.LogicalStep{exact, Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, U32.from_nat(cursor)),
        Core.checked_observe(shape, original, U32.from_nat(cursor)), Some{value}, kept(U32.from_nat(cursor)), observed),
        logical_keeps(tail, shape, original, tensor, 1n+cursor, rest, remaining, kept)}
    case 0n value <> rest:
      Empty.absurd(Laws.LogicalValues(0n, shape, tensor, cursor, value <> rest), logical)
    case 1n+tail Nil{}:
      Empty.absurd(Laws.LogicalValues(1n+tail, shape, tensor, cursor, Nil{}), logical)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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=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=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/reduction_LAWS.bend&name=LogicalStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LogicalValues