Theorem int2bytes-last-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: int2bytes-butlast, int2bytes-len-one, int2bytes-len-one-01, int2bytes-not-neg, int2bytes-one, int2bytes-rec-shift, no-leading-zero-04, rightshift-8, rightshift-8-01, rightshift-8-02,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 14
• Proof steps: 35
• Used lemmas: int2bytes-le255, int2bytes-le127, int2bytes-byte-neg, int2bytes-byte, int2bytes-rec-case,
• Used spec theorems:
  • int-div/modex
  • byte/byte-add-256
• Used simplifier rules:
  • int-div/div-elim-pospos
  • int-abs/Sub-def
  • int-abs/forward-lsle
  • int-abs/numlelsdel-01
  • int-div/mod256
  • int-basic1/numlslsdel-01
  • int-abs/forward-le-05
  • int-div/mod-zero
  • int-abs/lels-04
  • int-abs/numlsledel-01
  • int-abs/lels-02
  • int-abs/anti
  • byte/byte-mult-256
  • int-div/div-elim-negpos
  • int-abs/numleledel
  • int-abs/numle-03
  • int-abs/negle-07
  • int-abs/abs-08
  • int-div/mod-ls-same-02
  • int-div/mod-nle-02
  • int-abs/numlelsdel
  • int-abs/zero-gels-01
  • int-div/mod-ls-zero
  • int-basic1/numlsf
  • int-div/mod-ngez
  • int-abs/lels-03
  • byte/byte-mult
  • int-mult/associativity
  • int-mult/commutativity
  • byte/num-i2b-equal
  • int-abs/zero-gels-03
  • int-abs/forward-le-03
  • int-abs/forward-le-04
  • int-basic1/numlslsdel
  • int-basic1/ls-01
  • byte/byte-add-256
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/elim-sub
  • int-basic1/forward-pos
  • int-abs/forward-le
  • int-abs/forward-le-01
  • int-abs/forward-lels
  • int-abs/numleledel-01
  • list/bytelist/a
  • list-last/bytelist/last-def
  • list-last/bytelist/l
  • int-abs/lels
  • int-abs/lels-01