SliceLAWS.slice_scatter_miss: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend as SliceLAWS
Lines 393-422 of bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend&start_line=393&end_line=422

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

# ... and the slot of input cell (o, i, r) where no k below the length has
# i = start + k * step holds +0.0, as PyTorch's slice_backward leaves it.
law slice_scatter_miss:
  for +depth: Nat
  for +splits: Nat
  for +outer: Nat
  for +extent: Nat
  for +inner: Nat
  for +start: Nat
  for +step: Nat
  for +length: Nat
  for +count: Nat
  for +base: Nat
  for +dg: Nat
  for -G: Array<F32>
  for g: Array<F32>
  for same: {g == G : Array<F32>}
  for valid: Model.Balanced(F32, dg, G)
  for +path: Model.Path(depth)
  for +o: Nat
  for +i: Nat
  for +r: Nat
  for i_below: {Nat.is_lt(i, extent) == True{} : Bool}
  for r_below: {Nat.is_lt(r, inner) == True{} : Bool}
  for missed: @+k: Nat -> @below: {Nat.is_lt(k, length) == True{} : Bool} ->
    {Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i) == False{} : Bool}
  for at: {Nat.add(Model.offset(depth, path), base) == position(extent, inner, o, i, r) : Nat}
  for inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}
  Holds<{Model.observe(F32, depth, Slice.scatter_build(depth, splits, Slice.Plan{outer, extent, inner, start, step, length}, count, base, g), path) ==
    Some{0.0} : Maybe<&2, F32>}>

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=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=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.add
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  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=Sigma
  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=Path
  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/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=scatter_build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=scattered
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=target
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend&name=position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=scatter_slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=target_miss