Theorem inv-flashsize-size

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: ss, lss,
• Comment:
• Used by: at-store-inv, in-store-inv, inv-alloc, inv-diff-n, inv-reduce, inv-reduce-rem, inv-remove-refsize0, inv-remove-refsize0-diff, inv-set-refsize, inv-set-sizes,
• Used by units in proved state: apersistence-base,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 3
• Used lemmas: inv-flashsize,
• Used spec theorems:
  • Used simplifier rules: