BackwardPROOF.somes_bumped: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 142-152 of bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&start_line=142&end_line=152

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws

def somes_bumped(slot: Maybe<&2, F32>, +rest: List<&2, Maybe<&2, F32>>, +below: Nat, +target: Nat, +value: F32, flag: Bool,
  ih: {Laws.somes(Backward.bump(rest, below, target, value)) == Laws.mark(Laws.somes(rest), below, target) : List<&2, Bool>}) ->
  {Laws.somes(Backward.bumped(slot, rest, value, unit => Backward.bump(rest, below, target, value), flag)) ==
    Laws.marked(Maybe.is_some(&2, F32, slot), Laws.somes(rest), unit => Laws.mark(Laws.somes(rest), below, target), flag) : List<&2, Bool>}:
  match flag:
    case True{}:
      Equal.cong(Bool, List<&2, Bool>, found => found <> Laws.somes(rest),
        Maybe.is_some(&2, F32, Backward.accumulate(slot, Some{value})), True{}, is_some_accumulate(slot, value))
    case False{}:
      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, slot) <> xs,
        Laws.somes(Backward.bump(rest, below, target, value)), Laws.mark(Laws.somes(rest), below, target), ih)

Uses (14):
  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=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=accumulate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=bump
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=bumped
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=mark
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=marked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=somes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=is_some_accumulate