ReduceFiberProof.shifted: 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 474-511 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=474&end_line=511

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

# On a row of stride s, left stride L and right stride R, the positions
# d * s + q .. d * s + q + n - 1 have digit d and walk the rows below at
# q .. q + n - 1.
def shifted(+n: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +inner: Nat, +base: Nat,
  +digit: Nat, +q: Nat, +room: {Nat.is_le(Nat.add(q, n), stride) == True{} : Bool}, +mode: MaskMode<left, digit, target, inner>) ->
  {masked(n, Shape.Row{stride, left, right} <> rest, target, base, Nat.add(Nat.mul(digit, stride), q)) ==
    masked(n, rest, inner, Nat.add(base, Nat.mul(right, digit)), q) : 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, {==})
      +wl = Shape.walk_left(rest, q)
      +wr = Shape.walk_right(rest, q)
      +tail = masked(m, rows, target, base, 1n+c)
      +goal_right = kept(Nat.is_eq(wl, inner), Nat.add(Nat.add(base, Nat.mul(right, digit)), wr),
        masked(m, rest, inner, Nat.add(base, Nat.mul(right, digit)), 1n+q))
      %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),
          Nat.add(base, Nat.add(Nat.mul(right, _), Shape.walk_right(rest, Nat.mod(c, stride)))), tail) == goal_right : 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),
          Nat.add(base, Nat.add(Nat.mul(right, digit), Shape.walk_right(rest, _))), tail) == goal_right : List<&2, Nat>}
      %mode_mask(left, digit, target, inner, mode, wl) :
        {kept(_, Nat.add(base, Nat.add(Nat.mul(right, digit), wr)), tail) == goal_right : List<&2, Nat>}
      %Equal.sym(Nat, Nat.add(base, Nat.add(Nat.mul(right, digit), wr)), Nat.add(Nat.add(base, Nat.mul(right, digit)), wr),
        Index.add_assoc(base, Nat.mul(right, digit), wr)) :
        {kept(Nat.is_eq(wl, inner), _, tail) == goal_right : List<&2, Nat>}
      %Arith.add_succ(Nat.mul(digit, stride), q) :
        {kept(Nat.is_eq(wl, inner), Nat.add(Nat.add(base, Nat.mul(right, digit)), wr), masked(m, rows, target, base, _)) == goal_right : List<&2, Nat>}
      Equal.cong(List<&2, Nat>, List<&2, Nat>, xs => kept(Nat.is_eq(wl, inner), Nat.add(Nat.add(base, Nat.mul(right, digit)), wr), xs),
        masked(m, rows, target, base, Nat.add(Nat.mul(digit, stride), 1n+q)),
        masked(m, rest, inner, Nat.add(base, Nat.mul(right, digit)), 1n+q),
        shifted(m, stride, left, right, rest, target, inner, base, digit, 1n+q, le_step(q, m, stride, room), mode))

Uses (24):
  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=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=MaskMode
  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=mode_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/shape/index_proofs.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ