ElementwiseParallelProof.right_out: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof
Lines 117-131 of bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&start_line=117&end_line=131

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

def right_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
  -x: F32, -la: Array<F32>, pair: Array<F32> & F32, -exact: {pair == Array.get(F32, B, right_at(plan, position)) : Array<F32> & F32},
  -ex: {Some{x} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>},
  -el: {la == A : Array<F32>}, -valid: Model.Balanced(F32, dr, B)) ->
  Fact<CellOut(operation, plan, dl, dr, A, B, position, Elementwise.cell_right(operation, x, la, pair))>:
  (kept, y) = pair
  Fact{(pair_equal(la, kept, A, B, el,
      {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, y)) == B : Array<F32>})> -> {Refinement.first(F32, (kept, y)) == B : Array<F32>}}(
        read_keeps(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid))),
    {\{Fact: q => q} : Fact<({Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>})> ->
      {Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>}}(
      pick_value(operation, x, y, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))), ex,
        {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>})> ->
          {Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>}}(
          read_value(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid)))))}

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  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=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/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second
  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=cell_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=scalar
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=CellOut
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=left_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=pair_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=pick
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=pick_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=read_keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=read_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=right_at