ReductionPROOF.cursor_bounds: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 732-739 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=732&end_line=739

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

def cursor_bounds(+fuel: Nat, +cursor: Nat, +limit: Nat,
  bound: Shape.LE(Nat.add(1n+fuel, cursor), limit)) -> {Nat.is_lt(cursor, limit) == True{} : Bool}:
  Conversion.le_successor_lt(cursor, limit,
    Equal.sym(Bool, True{}, Nat.is_le(1n+cursor, limit),
      Nats.le_true(1n+cursor, limit,
        Nats.le_add_left(1n+cursor, fuel, limit,
          %add_comm(fuel, cursor) : Shape.LE(1n+_, limit)
          bound))))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_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/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_add_left
  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/tensor/reduction_PROOF.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_successor_lt