Theorem divide-by-10

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment: used in java.lang.Integer. Based on a paper by Montgomery (see Montgomery multiplication). 52429 = 2 ^ 16 - 1 - (10 - 8) * (2 ^ 16 / 10), we want to divide by 10, and actually divide by 8.
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 15
• Proof steps: 24
• Used lemmas: shiftright-pos-div, shiftzero-pos, band-commutativity, band-associativity, band-31-pos, intshiftzero-def-unbounded,
• Used spec theorems:
  • int-mult/exdivmodpos
  • int-div/div-add1-pospos
  • int-abs/zero-gs
  • int-div/div-zero
  • int-abs/forward-lele
• Used simplifier rules:
  • int-abs/numlsledel-01
  • int-abs/numle-03
  • int-abs/numleledel
  • int-abs/forward-le-04
  • int-abs/forward-le-03
  • int-abs/numlsledel
  • int-div/nummult-le-02
  • int-abs/numle-02
  • int-abs/le-add
  • int-div/nummult-le
  • int-basic2/num-between
  • int-abs/numleledel-01
  • int-div/div-eq-zero
  • int-abs/forward-le
  • int-abs/lels
  • int-basic2/eq
  • int-mult/one
  • int-div/div-mult-num
  • int-abs/zero-gels-01
  • int-abs/forward-le-02
  • int-abs/forward-lsle
  • int-div/mod-zero-num
  • int-mult/dist-rmerge
  • int-mult/eq-dist
  • int-mult/eq-pos
  • int-mult/zero-ge-add
  • int-basic2/add-c
  • int-basic2/add-a
  • int-div/div-mult-pos
  • int-abs/zero-gels-04
  • int-mult/zero-ge
  • int-abs/lels-01
  • int-abs/lels-04
  • int-mult/associativity
  • int-mult/commutativity
  • int-abs/forward-le-01