GatherPROOF.summed_is: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 463-479 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=463&end_line=479

import Base
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/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

def summed_is(+i: Nat, +at: Nat, +slot: Nat, +acc: F32, +dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, index: Array<U32>, +j: U32,
  -kept: {index == I : Array<U32>}, -seen: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
  hit: Bool, -told: {Nat.is_eq(U32.to_nat(j), i) == hit : Bool}, -valid: Model.Balanced(F32, dg, G)) ->
  Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.summed(hit, at, acc, G, index)>>:
  match hit:
    case False{}:
      Generic.Fact{Skipped{j, seen, told, Equal.cong(Array<U32>, F32 & (Array<F32> & Array<U32>), b => (acc, (G, b)), index, I, kept)}}
    case True{}:
      Generic.Fact{Taken{j, seen, told, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at))),
        Equal.sym(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, G, U32.from_nat(at)))},
          Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(at))), Refinement.law_get_refines(F32, dg, G, U32.from_nat(at), valid)),
        Equal.trans(F32 & (Array<F32> & Array<U32>), Gather.accumulate(acc, index, Array.get(F32, G, U32.from_nat(at))),
          (F32.add(acc, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at)))), (Refinement.first(F32, Array.get(F32, G, U32.from_nat(at))), index)),
          (F32.add(acc, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at)))), (G, I)),
          accumulated(acc, index, Array.get(F32, G, U32.from_nat(at))),
          triple(acc, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at))), Refinement.first(F32, Array.get(F32, G, U32.from_nat(at))), index, G, I,
            Refinement.law_get_retains(F32, dg, G, U32.from_nat(at), valid), kept))}}

Uses (29):
  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=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=F32.add
  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=Nat.is_eq
  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.from_nat
  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/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=law_get_refines
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=law_get_retains
  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/gather.bend&name=accumulate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=summed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=Stepped
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=accumulated
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=triple
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact