Theorem int2bits-len-mon

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: bits2int-nls, int2bits-less-2pot-01,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 17
• Proof steps: 32
• Used lemmas: int2bits-len-neg-01, uint2bits-len-mon-02, uint2bits-empty, int2bits-pos, int2bits-not-empty,
• Used spec theorems:
  • int-abs/Abs-neg
• Used simplifier rules:
  • int-abs/sub-add-09
  • int-abs/sub-le-01
  • int-basic2/add-zero
  • int-abs/sub-ls-01
  • int-abs/neg-15
  • int-abs/numls-03
  • int-abs/negle-13
  • int-abs/numle-02
  • int-basic1/lst
  • int-abs/abs-03
  • int-abs/numlsf-01
  • int-basic2/ls-02
  • int-basic2/ls-01
  • int-basic2/succ-01
  • int-basic1/trans
  • int-basic1/lf-01
  • int-abs/neg-13
  • int-abs/lels-03
  • int-abs/negle-07
  • int-abs/numle-03
  • int-abs/mone-05
  • int-abs/lels-02
  • int-abs/subsub
  • int-basic2/add-c
  • int-basic2/add-a
  • int-basic2/ls
  • int-abs/forward-lsle
  • int-abs/neg-07
  • int-abs/neg-06
  • int-basic1/ls-01
  • int-basic1/lst-01
  • int-abs/lels-01
  • int-abs/lels-04
  • int-abs/abs-06
  • int-abs/forward-lels
  • int-abs/lels
  • int-abs/Abs-pos
  • list-data/bitlista/l
  • nat-basic1/f
  • nat/lels-01