ReduceFiberProof.walk_left_below: 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 398-425 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=398&end_line=425

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

# The left walk of a position below the output count lies below the
# left count.
def walk_left_below(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +aligned: Shape.Aligned(left, right, output),
  +q: Nat, +below: {Nat.is_lt(q, Shape.numel(output)) == True{} : Bool}) ->
  {Nat.is_lt(Shape.walk_left(Shape.index_rows(left, right, output), q), Shape.numel(left)) == True{} : Bool}:
  match left right output:
    case Nil{} Nil{} Nil{}:
      {==}
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      Shape.AStep{+axis, +tail} = aligned
      +s = Shape.numel(ot)
      walk_left_row(lh, rh, oh, axis, Shape.numel(lt), Nat.div(q, s), Shape.walk_left(Shape.index_rows(lt, rt, ot), Nat.mod(q, s)),
        div_below(q, oh, s, below),
        walk_left_below(lt, rt, ot, tail, Nat.mod(q, s),
          {\{Decomposed: m_below => sum => m_below} : Decomposed<q, s> -> {Nat.is_lt(Nat.mod(q, s), s) == True{} : Bool}}(
            decompose(q, s, positive_of(q, oh, s, below)))))
    case Nil{} Nil{} +oh <> +ot:
      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(Nil{}, Nil{}, oh <> ot), q), 1n) == True{} : Bool}, aligned)
    case Nil{} +rh <> +rt Nil{}:
      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(Nil{}, rh <> rt, Nil{}), q), 1n) == True{} : Bool}, aligned)
    case +lh <> +lt Nil{} Nil{}:
      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(lh <> lt, Nil{}, Nil{}), q), Shape.numel(lh <> lt)) == True{} : Bool}, aligned)
    case Nil{} +rh <> +rt +oh <> +ot:
      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(Nil{}, rh <> rt, oh <> ot), q), 1n) == True{} : Bool}, aligned)
    case +lh <> +lt Nil{} +oh <> +ot:
      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(lh <> lt, Nil{}, oh <> ot), q), Shape.numel(lh <> lt)) == True{} : Bool}, aligned)
    case +lh <> +lt +rh <> +rt Nil{}:
      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(lh <> lt, rh <> rt, Nil{}), q), Shape.numel(lh <> lt)) == True{} : Bool}, aligned)

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.div
  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.mod
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=Decomposed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=decompose
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=div_below
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=positive_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=walk_left_row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left