def bound_inside

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:586

import Base
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed

586def bound_inside(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
587  {Nat.add(U32.to_nat(Signed.bound(limit, Signed.Last{k})), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}:
588  %Equal.sym(Bool, U32.is_lt(k, limit), True{}, inside) :
589    {Nat.add(U32.to_nat(Bool.pick(U32, Bool.not(_), 0, Signed.wrap(limit, Signed.Last{k}))), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}
590  last_wrapped(limit, k, inside)