GatherPROOF.looked_keeps: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 254-263 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=254&end_line=263

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

# A forward read hands both arrays back ...
def looked_keeps(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, -I: Array<U32>, pair: Array<U32> & U32,
  -kept: {Refinement.first(U32, pair) == I : Array<U32>}, -valid: Model.Balanced(F32, da, A)) ->
  Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, pair)) == (A, I) : Array<F32> & Array<U32>}>:
  (index, +j) = pair
  Generic.Fact{Equal.trans(Array<F32> & Array<U32>, Pair.snd(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j)))))),
    (Refinement.first(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))), index), (A, I),
    take_snd(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))),
    both(Refinement.first(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))), index, A, I,
      Refinement.law_get_retains(F32, da, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))), valid), kept))}

Uses (21):
  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=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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  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/refinement.bend&name=first
  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/tensor/gather.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=looked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=both
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=take_snd
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact