Theorem fits-law-shr

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 17
• Proof steps: 28
• Used lemmas: fits-law-div-stronger, byte-nls, bib-in-01, num-ibbi, byte-equal, ibi,
• Used spec theorems:
  • intops/intshiftrsign-band31
  • intops/intshiftrsign-2pot-pos
  • intops/intshiftrsign-2pot-neg-01
  • int-div/div-add1-negneg
  • int-div/le-abs-numerator
  • int-basic1/lf-01
  • int-div/div-zero-ngr
• Used simplifier rules:
  • int-abs/negeq
  • int-div/div-mone-01
  • int-abs/numlelsdel
  • int-basic1/numlslsdel-01
  • int-basic2/succ-01
  • int-basic2/zero-01
  • int-abs/mone-05
  • int-abs/numle-03
  • int-abs/negle-07
  • int-abs/succ-01
  • int-abs/neg-02
  • int-abs/subsub
  • int-abs/abs-08
  • int-abs/abs-05
  • int-pot/two-zero
  • int-basic1/numlsf
  • int-abs/sub-le
  • int-abs/sub-le-01
  • int-abs/zero-gels-01
  • int-abs/forward-lsle
  • int-abs/forward-le-01
  • int-abs/forward-lels
  • int-abs/minus-add
  • int-pot/zero
  • int-div/mod-neg-01
  • int-div/mod-same
  • int-abs/neg-05
  • int-pot/pot2-pos
  • int-abs/numls-03
  • int-abs/mone-08
  • int-abs/neg-06
  • int-div/neg-01
  • int-div/div-same
  • int-mult/minus-one-01
  • int-mult/associativity
  • int-mult/commutativity
  • int-abs/neg-15
  • int-abs/sub-add-01
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/sub-eq
  • int-abs/Sub-def
  • int-basic2/add-in
  • int-basic1/forward-pos
  • int-abs/sub-sub-04
  • int-abs/forward-le-05
  • int-abs/forward-le-02
  • int-abs/lels-03
  • intops/intshiftrsign-zero
  • int-abs/lels-02
  • intops/band-notneg
  • int-abs/forward-le-04
  • int-abs/zero-gels-04
  • intops/band-commutativity
  • intops/band-associativity
  • intops/band-max-05
  • int-abs/lels
  • int-abs/lels-01