ReduceFiberProof.masked_base: 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 591-604 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=591&end_line=604

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

def masked_base(+n: Nat, +rows: List<&2, Shape.Row>, +target: Nat, +base: Nat, +cursor: Nat) ->
  {masked(n, rows, target, base, cursor) == shift(base, masked(n, rows, target, 0n, cursor)) : List<&2, Nat>}:
  match n:
    case 0n:
      {==}
    case 1n+m:
      +keep = Nat.is_eq(Shape.walk_left(rows, cursor), target)
      +x = Shape.walk_right(rows, cursor)
      Equal.trans(List<&2, Nat>, kept(keep, Nat.add(base, x), masked(m, rows, target, base, 1n+cursor)),
        kept(keep, Nat.add(base, x), shift(base, masked(m, rows, target, 0n, 1n+cursor))),
        shift(base, kept(keep, x, masked(m, rows, target, 0n, 1n+cursor))),
        Equal.cong(List<&2, Nat>, List<&2, Nat>, tail => kept(keep, Nat.add(base, x), tail),
          masked(m, rows, target, base, 1n+cursor), shift(base, masked(m, rows, target, 0n, 1n+cursor)), masked_base(m, rows, target, base, 1n+cursor)),
        kept_shift(keep, base, x, masked(m, rows, target, 0n, 1n+cursor)))

Uses (13):
  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.trans
  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.is_eq
  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=kept_shift
  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=shift
  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