ReduceFiberProof.masked_split: 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 277-299 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=277&end_line=299

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

def masked_split(+a: Nat, +b: Nat, +rows: List<&2, Shape.Row>, +target: Nat, +base: Nat, +cursor: Nat) ->
  {masked(Nat.add(a, b), rows, target, base, cursor) ==
    List.append(&2, Nat, masked(a, rows, target, base, cursor), masked(b, rows, target, base, Nat.add(cursor, a))) : List<&2, Nat>}:
  match a:
    case 0n:
      %Equal.sym(Nat, Nat.add(cursor, 0n), cursor, Broadcast.add_zero(cursor)) :
        {masked(b, rows, target, base, cursor) == masked(b, rows, target, base, _) : List<&2, Nat>}
      {==}
    case 1n+p:
      +keep = Nat.is_eq(Shape.walk_left(rows, cursor), target)
      +position = Nat.add(base, Shape.walk_right(rows, cursor))
      +front = masked(p, rows, target, base, 1n+cursor)
      %Equal.sym(Nat, Nat.add(cursor, 1n+p), 1n+Nat.add(cursor, p), Arith.add_succ(cursor, p)) :
        {masked(1n+Nat.add(p, b), rows, target, base, cursor) ==
          List.append(&2, Nat, kept(keep, position, front), masked(b, rows, target, base, _)) : List<&2, Nat>}
      Equal.trans(List<&2, Nat>, kept(keep, position, masked(Nat.add(p, b), rows, target, base, 1n+cursor)),
        kept(keep, position, List.append(&2, Nat, front, masked(b, rows, target, base, Nat.add(1n+cursor, p)))),
        List.append(&2, Nat, kept(keep, position, front), masked(b, rows, target, base, Nat.add(1n+cursor, p))),
        Equal.cong(List<&2, Nat>, List<&2, Nat>, xs => kept(keep, position, xs),
          masked(Nat.add(p, b), rows, target, base, 1n+cursor),
          List.append(&2, Nat, front, masked(b, rows, target, base, Nat.add(1n+cursor, p))),
          masked_split(p, b, rows, target, base, 1n+cursor)),
        kept_append(keep, position, front, masked(b, rows, target, base, Nat.add(1n+cursor, p))))

Uses (16):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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_append
  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/shape/broadcast_proofs.bend&name=add_zero
  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