ElementwisePROOF.natural_decided_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 740-756 of bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&start_line=740&end_line=756

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

def natural_decided_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>,
  -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
  -exact: {U32.to_nat(index) == cursor : Nat}, -inside: {Nat.is_lt(cursor, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
  NaturalSuccess<Shape.output_shape(plan), cursor, Elementwise.natural_step_decided(operation, plan, cursor, index, state, decision)>:
  match decision:
    case Shape.BFalse{equal}:
      Elementwise.State{left, right, output} = state
      NaturalSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor), PlanProof.eq_true(U32.to_nat(index), cursor, exact), equal))}
    case Shape.BTrue{equal}:
      natural_result_success(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal),
        Elementwise.step(operation, plan, index, state),
        {\{StepSuccess: successful => successful} : StepSuccess<Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)> ->
          {step_succeeded(Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)) == True{} : Bool}}(
            actual_step_success(operation, plan, index, state, fits,
              %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}
              inside)))

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  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/shape/core.bend&name=BoolCase
  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=elements
  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/shape/nat_proofs.bend&name=contradiction
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=eq_true
  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=State
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=natural_step_decided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=FittingSources
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=NaturalSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=StepSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=actual_step_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=natural_result_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_left_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_right_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_succeeded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=natural_equal