SlicePROOF.missed_k: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
Lines 826-842 of bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&start_line=826&end_line=842

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

# Input cell (o, i, r) that no k below the length reaches reads nothing.
def missed_k(+outer: Nat, +extent: Nat, +inner: Nat, +start: Nat, +step: Nat, +length: Nat, +row: Nat, +r: Nat, +i: Nat, +k: Nat,
  missed: @+k: Nat -> @below: {Nat.is_lt(k, length) == True{} : Bool} -> {Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i) == False{} : Bool},
  decision: Shape.BoolCase<Slice.hits(start, step, length, i, k)>) ->
  {picked_k(outer, extent, inner, start, step, length, row, r, i, k) == None{} : Maybe<&2, Nat>}:
  match decision:
    case Shape.BFalse{equal}:
      %equal : {Slice.picked(Slice.Plan{outer, extent, inner, start, step, length}, row, r, i, k, _) == None{} : Maybe<&2, Nat>}
      {==}
    case Shape.BTrue{equal}:
      +rest = Arith.and_right(Nat.is_le(start, i), Bool.and(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i)),
        Equal.sym(Bool, True{}, Slice.hits(start, step, length, i, k), equal))
      Empty.absurd({picked_k(outer, extent, inner, start, step, length, row, r, i, k) == None{} : Maybe<&2, Nat>},
        Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), True{},
          Equal.sym(Bool, Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), False{},
            missed(k, Arith.and_left(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), rest))),
          Arith.and_right(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), rest))))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=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_le
  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=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  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=hits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=picked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=picked_k