ReducePROOF.length_decided: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
Lines 587-608 of bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&start_line=587&end_line=608

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

def length_decided(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
  -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +below: Bool,
  -decision: {below == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) -> Holds<{List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
  match below:
    case True{}:
      Holds{Empty.absurd({List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, Arith.clash(
        Equal.trans(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), True{},
          Equal.sym(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), False{}, below_self(List.length(&2, F32, values))),
          Equal.trans(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), True{},
            {\{Holds: proof => proof} : Holds<{Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
              natural_presence(shape, tensor, values, listed, List.length(&2, F32, values),
              Shape.LE.from(List.length(&2, F32, values), 1048576n, Equal.sym(Bool, Nat.is_le(List.length(&2, F32, values), 1048576n), True{},
                Conversion.le_trans(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), 1048576n,
                  Conversion.lt_le(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)),
                  Equal.sym(Bool, True{}, Nat.is_le(Shape.logical_numel(Shape.dimensions(shape)), 1048576n), Nats.le_true(Shape.logical_numel(Shape.dimensions(shape)), 1048576n, capacity_of(shape)))))))),
            Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)))))}
    case False{}:
      Holds{neither_below(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision),
        Equal.trans(Bool, Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)), Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))), False{},
          {\{Holds: proof => proof} : Holds<{Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
            natural_presence(shape, tensor, values, listed, Shape.logical_numel(Shape.dimensions(shape)), capacity_of(shape))),
          below_self(Shape.logical_numel(Shape.dimensions(shape)))))}

Uses (26):
  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=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=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=Listed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=below_self
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=capacity_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=natural_presence
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=neither_below
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE.from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=lt_le