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

import Base
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

def step_added(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
  +o: Nat, +i: Nat, +r: Nat, +rest: Nat, +k: Nat, +acc: F32,
  ih: @+next: F32 -> Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, next,
    Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (next, (G, I))))>,
  -result: F32 & (Array<F32> & Array<U32>),
  st: Stepped<dg, G, di, I, i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, result>) ->
  Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, result)>:
  match st:
    case Skipped{j, read, other, kept}:
      Generic.Fact{
        %Equal.sym(F32 & (Array<F32> & Array<U32>), result, (acc, (G, I)), kept) :
          StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, _)
        {\{Generic.Fact: q => q} : Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))> -> StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))}(
      {\{Generic.Fact: q => Generic.Fact{(Pair.fst(
          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))), q),
        Laws.Skips{j, read_slot(kind, count, inner, o, k, r, di, I, j, read), other, Pair.snd(
          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))), q)})}} :
        Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, acc, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))> ->
        Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))>}(ih(acc)))}
    case Taken{j, read, same, x, word, kept}:
      Generic.Fact{
        %Equal.sym(F32 & (Array<F32> & Array<U32>), result, (F32.add(acc, x), (G, I)), kept) :
          StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, _)
        {\{Generic.Fact: q => q} : Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))> -> StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))}(
      {\{Generic.Fact: q => Generic.Fact{(Pair.fst(
          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I)))) == (G, I) : Array<F32> & Array<U32>},
          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x),
            Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))), q),
        Laws.Adds{j, read_slot(kind, count, inner, o, k, r, di, I, j, read), same, x, word, Pair.snd(
          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I)))) == (G, I) : Array<F32> & Array<U32>},
          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x),
            Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))), q)})}} :
        Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, F32.add(acc, x),
          Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))> ->
        Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))>}(ih(F32.add(acc, x))))}

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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.fst
  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=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Lookup
  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=added
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=cell_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=slot_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=AddStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=Added
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=AddedIs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=StepIs
  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=read_slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact