Theorem subset-is-union

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 9
• Proof steps: 21
• Used lemmas: int-empty, unadd, unin, int-rax, del-e-02, int-del-rew, uninsert, delete-insert, undel-03, Delete, unin-01, insdel-sub, int-c, int-a, int-e, une-01, unc, una, unsub,
• Used spec theorems:
  • set-basic/eq
  • set-basic/sub-insert
  • set-basic/Extension
• Used simplifier rules:
  • set-basic/subset-empty
  • set-basic/in-03
  • set-basic/sub-in
  • set-basic/size-one-01
  • set-basic/ne
  • set-basic/size-zero
  • set-basic/one-size
  • set-basic/in-04
  • set-basic/size-zero-01
  • set-basic/ne-01