Theorem in-uni

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: at-uni, del-uni, disj-distr-uni, exin-uni, size-uni, subset-uni, uni-ass, uni-com, uni-inj,
• Used by units in proved state: linked-list-aux, embed-aux, heap-sep, linked-list, separation-rg, separation, heap-fun, maplet,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 6
• Proof steps: 9
• Used lemmas: size-alloc, size-write, uni-alloc, in-write-strong, uni-write, in-alloc, disj-write, disj-alloc, sanity, exin, ext, in-emp, uni-emp-r,
• Used spec theorems:
  • Used simplifier rules:
    • nat-basic2/s
    • nat-basic1/ref-1
    • nat-basic2/a
    • nat-basic2/c