def cursor_exact

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:741

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

741def cursor_exact(+fuel: Nat, +shape: Shape.Shape, +cursor: Nat,
742  bound: Shape.LE(Nat.add(1n+fuel, cursor), Shape.elements(shape))) -> {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
743  Conversion.natural_word_exact(cursor, Shape.count(shape),
744    %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape)) : {Nat.is_le(cursor, _) == True{} : Bool}
745    Conversion.le_predecessor(cursor, Shape.elements(shape),
746      Equal.sym(Bool, True{}, Nat.is_le(1n+cursor, Shape.elements(shape)),
747        Nats.le_true(1n+cursor, Shape.elements(shape),
748          Nats.le_add_left(1n+cursor, fuel, Shape.elements(shape),
749            %add_comm(fuel, cursor) : Shape.LE(1n+_, Shape.elements(shape))
750            bound)))))