Theorem int2bytes-first-neg-01

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 12
• Proof steps: 28
• Used lemmas: int2bytes-empty, int2bytes-byte, int2bytes-rec255-neg,
• Used spec theorems:
  • byte/i2b-equal
  • byte/bib-in-01
  • list-last/bytelist/splitlasteq
  • int-abs/Abs-neg
  • int-abs/zero-ge-01
• Used simplifier rules:
  • byte/notequal
  • int-abs/mone-06
  • int-abs/numlsledel-01
  • int-abs/zero-gels-01
  • int-abs/numls-02
  • int-abs/lels-02
  • int-abs/numle-02
  • int-mult/zero-ge
  • int-div/nummult-ls-01
  • int-basic2/add-zero
  • int-abs/anti
  • int-mult/zero-ls
  • int-abs/zero-gels-04
  • int-basic2/ls-01
  • int-abs/forward-lele
  • int-abs/forward-lsle
  • int-abs/forward-le-01
  • int-mult/commutativity
  • int-mult/associativity
  • int-mult/succ-rmerge
  • int-mult/numle-12
  • int-abs/lels-03
  • int-div/div-elim-negpos
  • int-abs/sub-le
  • int-abs/neg-15
  • int-abs/neg-06
  • int-abs/Abs-pos
  • int-abs/forward-le-04
  • int-abs/neg-13
  • int-div/neg-01
  • int-abs/abs-08
  • int-div/abs
  • intnat/labs
  • int-div/div-ls-zero
  • int-abs/numle-03
  • list/bytelist/e-02
  • list-last/bytelist/last-elim
  • list-last/bytelist/lin-01
  • list-last/bytelist/l-02
  • list-last/bytelist/bapp
  • list/bytelist/app
  • list-last/bytelist/b
  • list/bytelist/e-01
  • list/bytelist/app-02-ant
  • list/bytelist/e
  • int-basic1/numlsf
  • int-basic2/add-c
  • int-basic2/add-a
  • int-abs/numls-03
  • int-abs/elim-sub
  • list/bytelist/in-15
  • list/bytelist/in-append
  • int-abs/lels-01
  • int-basic1/lst
  • byte/byte
  • list/bytelist/in-17
  • list/bytelist/c-03
  • int-abs/numleledel-01
  • int-basic1/numlslsdel
  • int-abs/forward-lels
  • int-abs/lels
  • int-abs/forward-le-02
  • list/bytelist/a
  • list/bytelist/in-14