Theorem lookup-if

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: localsimp,
• Comment:
• Used by: at-mode, at-other, at-other-01, at-other-02, at-other-03, at-other-04, at-other-05, at-other-06, at-other-07, at-other-08, at-other-09, at-other-10, at-other-11, at-other-12, at-other-13, at-other-14, at-other-15, at-other-16, at-other-17, at-other-18, at-other-19, at-other-20, at-other-21, at-other-22, at-other-23, at-other-24, at-other-25, at-other-26, at-other-27, at-other-28, at-other-29, at-other-30, at-other-31, at-other-32, at-other-33, at-other-34, at-other-35, at-other-36, at-other-37, at-other-38, at-other-39, at-other-40, at-other-41, at-other-42, at-other-43, at-other-44, at-other-45, at-other-46, at-other-47, at-other-48, at-other-49, at-other-50, at-other-51, at-other-class, at-other-class-01, at-other-field, at-other-type, at-other-type-01, at-other-type-02, at-other-type-03, at-other-type-04, at-other-type-05, at-other-type-06, at-other-type-07, at-other-type-08, at-other-type-09, at-other-type-10, length-at, look-ins, look-ins-01, look-out, look-out-01, look-type, lookup-put-mode, type-at,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 1
• Used lemmas:
• Used spec theorems:
  • Used simplifier rules:
    • store/javastore/At-same
    • store/javastore/At-other