GatherPROOF.stepped_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 491-499 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=491&end_line=499

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 stepped_is(+i: Nat, +at: Nat, +slot: Nat, +acc: F32, +dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>,
  -valid: Model.Balanced(F32, dg, G), -index_valid: Model.Balanced(U32, di, I)) ->
  Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.stepped(i, at, slot, acc, (G, I))>>:
  Generic.Fact{{\{Generic.Fact: q => q} :
    Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.compared(i, at, acc, G, Array.get(U32, I, U32.from_nat(slot)))>> ->
    Stepped<dg, G, di, I, i, at, slot, acc, Gather.compared(i, at, acc, G, Array.get(U32, I, U32.from_nat(slot)))>}(
    compared_is(i, at, slot, acc, dg, G, di, I, Array.get(U32, I, U32.from_nat(slot)),
      Refinement.law_get_retains(U32, di, I, U32.from_nat(slot), index_valid),
      Refinement.law_get_refines(U32, di, I, U32.from_nat(slot), index_valid), valid))}

Uses (15):
  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=Nat
  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=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=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/tensor/gather.bend&name=compared
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=stepped
  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=compared_is
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact