SignedLAWS.signed_capped_classifies: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend as SignedLAWS
Lines 269-278 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=269&end_line=278

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

# The inference never forms the exact sizes' product: capped classifies it
# against the input's element count, ZeroProduct, Within{p} with p at most
# the count, or Beyond, multiplying only numbers at most the count. So the
# inferred size is worked out from numbers at most 2^20, however large the
# exact sizes, as [-1, 2^24, 2^24] of an empty input, whose product 2^48 is
# past the native Nat limit.
law signed_capped_classifies:
  for +bound: Nat
  for +extents: List<&2, Signed.Extent>
  {Signed.capped(bound, extents) == classify(bound, Signed.exact_product(extents)) : Signed.Product}

Uses (8):
  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=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