ReducePROOF.same_presence: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
Lines 565-577 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=565&end_line=577

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/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

def same_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
  -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +source: U32) ->
  Holds<{Nat.is_lt(U32.to_nat(source), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}>:
  Holds{Equal.trans(Bool, Nat.is_lt(U32.to_nat(source), List.length(&2, F32, values)), TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
    Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
    word_presence(values, U32.to_nat(source)),
    Equal.trans(Bool, TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
      TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)), Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
      Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Laws.word_at(values, U32.to_nat(source)),
        Core.checked_observe(shape, tensor, source),
        Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, source), Laws.word_at(values, U32.to_nat(source)), listed(source))),
      {\{Holds: proof => proof} : Holds<{TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
        observed_presence(shape, tensor, source, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), {==}))))}

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=Listed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=word_at
  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=observed_presence
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=word_presence
  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=Dynamic
  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/transform_PROOF.bend&name=maybe_present