Theorem subseteq-restrict

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by: btree-istore-reduce,
• 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:
• Used spec theorems:
  • store/index-store-address-store/Subset
• Used simplifier rules:
  • store+set/index-store-address-store/restrict-in
  • store+set/index-store-address-store/restrict-at
  • store/index-store-address-store/subset-elem-eq-02
  • store/index-store-address-store/superset-elem-in-01