This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| disj | ⊦ empty ≠ full(a) | An Axiom |
| sel | ⊦ full(a).elem = a | An Axiom |
| inj | ⊦ full(a) = full(a0) ↔ a = a0 | An Axiom |
| case | ⊦ slot = empty ∨ slot = full(slot.elem) | An Axiom |
| elim | ⊦ slot ≠ empty → (a = slot.elem ↔ slot = full(a)) | An Axiom |
| gen | An Axiom | |
| updsel | ⊦ slot ≠ empty → (slot.elem:= a).elem = a | An Axiom |
| upd | ⊦ full(a).elem:= a0 = full(a0) | An Axiom |