Theorem and-rec-04

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: and-com, and-first, and-insgn, and-notempty, and-onesin, and-sgn, and-true, and-zero-01, and-zero-02, and-zerosin, band-011x-pos, band-max, band-zero, bitsand-false, or-invandinv,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 2
• Used lemmas: bitsand-zerol,
• Used spec theorems:
  • list/bitlista/lastdiv-rew
• Used simplifier rules:
  • list/bitlista/a
  • list/bitlista/c-04