Theorem sis-ls-same

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 6
• Proof steps: 11
• Used lemmas: sis-pos-low, sis-pos-high, sis-neg-low, sis-neg-high,
• Used spec theorems:
  • int-div/mod-zero-05
• Used simplifier rules:
  • int-abs/absle
  • int-abs/abs-16
  • int-basic1/numlslsdel
  • int-abs/forward-le-05
  • int-abs/lels-04
  • int-abs/sub-ls-01
  • int-div/mod-nls-01
  • int-abs/forward-le-01
  • int-abs/zero-gels
  • int-abs/numleledel-01
  • int-abs/forward-le-04
  • int-abs/forward-lele
  • int-abs/zero-gels-03
  • int-div/mod-nle-02
  • int-abs/abs-08
  • int-abs/neg-13
  • int-abs/numlsledel-01
  • int-basic1/irref
  • int-abs/zero-gels-01
  • int-div/mod-ls-zero
  • int-abs/numls-02
  • int-abs/forward-lsle
  • int-basic2/add-c
  • int-basic2/add-a
  • int-div/mod-lsz
  • int-abs/forward-le-02
  • int-basic1/numlsf
  • int-abs/forward-lels
  • int-abs/lels-01
  • int-abs/lels-03
  • int-abs/lels