Theorem equality-any

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: eq-zero,
• Used by units in proved state: decimal-simple-ops,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 34
• Proof steps: 63
• Used lemmas: eq-same, mkDecimal-zero, scale-base, scale-zero, intvalue-zero, getint-zero, intvalue-base, Equality, mkDecimal-rec,
• Used spec theorems:
  • int-pot/pot-eq-sub
  • int-div/mod-zero-num
  • int-mult/zero-eq
  • int-pot/Pot-pos
  • int-div/modex
• Used simplifier rules:
  • int-mult/eq-same-01
  • int-abs/abs-07
  • int-abs/lels-01
  • int-abs/sub-sub
  • int-div/mod-zero-num
  • int-abs/sub-ls-01
  • int-basic1/ls-01
  • int-abs/lels-02
  • int-abs/sub-eq-01
  • int-abs/abs-03
  • int-abs/lenls
  • int-basic2/add-c
  • int-basic2/add-a
  • int-basic2/add-zero
  • int-abs/sub-ls
  • nat-basic2/c
  • nat-basic2/a
  • int-div/abs-div10-le
  • int-abs/lels
  • int-div/abs
  • intnat/labs
  • nat-basic2/l
  • int-abs/abs-abs
  • int-abs/abs-06
  • int-abs/sub-pred
  • int-div/div-mult-num
  • int-mult/one
  • int-mult/eq-nonzero
  • int-mult/Mult-zero
  • int-mult/associativity
  • int-mult/commutativity
  • int-mult/zero-eq
  • int-pot/pot-zero-01
  • int-abs/absls