Theorem byte-law-neg

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: byte-law-sub-one-01,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 24
• Proof steps: 37
• Used lemmas: byte, num-i2b-equal, bib-pos-low, bib-upper, byte-equal, bib-pos-high, i2b-equal, byte-add-256-01, bib-neg-low, bib-neg-high, bib-in-01,
• Used spec theorems:
  • int-basic1/lsrec
• Used simplifier rules:
  • int-abs/Sub-def
  • int-abs/sub-le-01
  • int-div/mod-le-num
  • int-basic2/num-between
  • int-abs/sub-eq
  • int-abs/neg-15
  • int-abs/sub-eq-01
  • int-abs/lels-02
  • int-abs/num-between
  • int-abs/sub-ls-01
  • int-abs/minus-sub
  • int-div/mod-zero-02
  • int-div/modmod
  • int-abs/neg-05
  • int-abs/anti
  • int-abs/numleledel
  • int-basic1/numlslsdel-01
  • int-abs/forward-le-01
  • int-abs/zero-gels
  • int-abs/neg-03
  • int-abs/forward-lele
  • int-abs/numleledel-01
  • int-basic2/eq
  • int-abs/lels-04
  • int-basic2/succ-01
  • int-abs/forward-lels
  • int-div/mod-grz
  • int-basic1/forward-pos
  • int-abs/forward-le-05
  • int-abs/numle-02
  • int-abs/negle-13
  • int-abs/sub-le
  • int-abs/minus-add
  • int-abs/forward-lsle
  • int-abs/neg-12
  • int-abs/subsub
  • int-abs/negeq
  • int-abs/numadd-01
  • int-abs/zero-gels-03
  • int-abs/neg-13
  • int-abs/numls-02
  • int-div/mod-nle-02
  • int-abs/negle-07
  • int-basic2/add-zero
  • int-basic1/ls-01
  • int-div/mod-neg-01
  • int-abs/neg-07
  • int-abs/numls-03
  • int-basic1/numlslsdel
  • int-abs/zero-gels-01
  • int-div/mod-ls-zero
  • int-basic2/add-c
  • int-basic2/add-a
  • int-abs/lels-03
  • int-abs/lels
  • int-basic1/numlsf
  • int-basic1/lst
  • int-abs/lels-01