ReduceFiberProof.shifted_off: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 513-534 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=513&end_line=534

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

def shifted_off(+n: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat,
  +digit: Nat, +q: Nat, +room: {Nat.is_le(Nat.add(q, n), stride) == True{} : Bool}, +mode: OffMode<rest, left, stride, digit, target>) ->
  {masked(n, Shape.Row{stride, left, right} <> rest, target, base, Nat.add(Nat.mul(digit, stride), q)) == Nil{} : List<&2, Nat>}:
  match n:
    case 0n:
      {==}
    case 1n+m:
      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
      +c = Nat.add(Nat.mul(digit, stride), q)
      +below = lt_of_room(q, m, stride, room)
      +dq = div_of(c, stride, digit, q, below, {==})
      +mq = mod_of(c, stride, digit, q, below, {==})
      +tail = masked(m, rows, target, base, 1n+c)
      +position = Nat.add(base, Shape.walk_right(rows, c))
      %Equal.sym(Nat, Nat.div(c, stride), digit, dq) :
        {kept(Nat.is_eq(Nat.add(Nat.mul(left, _), Shape.walk_left(rest, Nat.mod(c, stride))), target), position, tail) == Nil{} : List<&2, Nat>}
      %Equal.sym(Nat, Nat.mod(c, stride), q, mq) :
        {kept(Nat.is_eq(Nat.add(Nat.mul(left, digit), Shape.walk_left(rest, _)), target), position, tail) == Nil{} : List<&2, Nat>}
      %off_mask(rest, left, stride, digit, target, mode, q, below) :
        {kept(_, position, tail) == Nil{} : List<&2, Nat>}
      %Arith.add_succ(Nat.mul(digit, stride), q) : {masked(m, rows, target, base, _) == Nil{} : List<&2, Nat>}
      shifted_off(m, stride, left, right, rest, target, base, digit, 1n+q, le_step(q, m, stride, room), mode)

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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.div
  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.mod
  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/autograd/reduce_fiber_proof.bend&name=OffMode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=div_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=le_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=lt_of_room
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=mod_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=off_mask
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ