Theorem inv-append

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: bitsinvert-size, inv-empty, inv-false-01, inv-fill, inv-in, inv-inv, inv-last, inv-last-03, inv-len, inv-sgn, inv-true-01, succ-exinv, succ-inv2x, succ-succ,
• Used by units in proved state: intops, int2bits, bytes, byte,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 3
• Used lemmas: inv-rec, invert-base,
• Used spec theorems:
  • Used simplifier rules:
    • list/bitlista/app-01
    • list/bitlista/c
    • list/bitlista/Nil
    • list/bitlista/a