def same_presence
bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:565
import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
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
565def same_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
566 -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +source: U32) ->
567 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}>:
568 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))),
569 Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
570 word_presence(values, U32.to_nat(source)),
571 Equal.trans(Bool, TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
572 TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)), Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
573 Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Laws.word_at(values, U32.to_nat(source)),
574 Core.checked_observe(shape, tensor, source),
575 Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, source), Laws.word_at(values, U32.to_nat(source)), listed(source))),
576 {\{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}}(
577 observed_presence(shape, tensor, source, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), {==}))))}