SignedLAWS.signed_capped_within: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend as SignedLAWS
Lines 280-285 of bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend&start_line=280&end_line=285

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

law signed_capped_within:
  for +bound: Nat
  for +extents: List<&2, Signed.Extent>
  for +product: Nat
  for within: {Signed.capped(bound, extents) == Signed.Within{product} : Signed.Product}
  {Nat.is_le(product, bound) == True{} : Bool}

Uses (13):
  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=Equal.trans
  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.is_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=Extent
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=Product
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=capped
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=exact_product
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend&name=classify
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=capped_classifies
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend&name=classify_within