CorePROOF.prefix_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 785-797 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=785&end_line=797

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/word_injective.bend as Injective
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

def prefix_equal(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
  -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
  -after: Core.Tensor<Shape.output_shape(plan)>, converted: {U32.to_nat(index) == cursor : Nat},
  checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, index),
  observed: {Core.observe(Shape.output_shape(plan), after, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>},
  +other: U32, equal: {U32.to_nat(other) == cursor : Nat}) ->
  Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
    {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}:
  %Injective.u32_natural_injective(index, other)(Equal.trans(Nat, U32.to_nat(index), cursor, U32.to_nat(other), converted,
    Equal.sym(Nat, U32.to_nat(other), cursor, equal))) :
    Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, _) &
      {Core.observe(Shape.output_shape(plan), after, _) == Elementwise.expected(operation, plan, original_left, original_right, _) : Maybe<&2, F32>}
  (checked, observed)

Uses (18):
  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=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=Sigma
  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/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape
  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=ObservationChecked
  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=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_injective.bend&name=u32_natural_injective