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: |
|---|---|---|
| allNull-def | ⊦ allNull(s) ↔ (∀ str, ag. s(state(str), ag) = null) ∧ (∀ cmd, ag. s(Mailbox(cmd), ag) = null) | An Axiom |
| stateNotNull-def | ⊦ stateNotNull(s) ↔ (∀ str, ag. s(state(str), ag) ≠ null → (∀ str0, ag0. ag ≠ ag0 ∨ str0 ≠ str → s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. s(Mailbox(cmd0), ag0) = null)) | An Axiom |
| mailboxNotNull-def | ⊦ mailboxNotNull(s) ↔ (∀ cmd, ag. s(Mailbox(cmd), ag) ≠ null → (∀ str0, ag0. s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. ag ≠ ag0 ∨ cmd0 ≠ cmd → s(Mailbox(cmd0), ag0) = null)) | An Axiom |
| maxOneNotNull-def | ⊦ maxOneNotNull(s) ↔ (∀ str, ag. s(state(str), ag) ≠ null → (∀ str0, ag0. ag ≠ ag0 ∨ str0 ≠ str → s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. s(Mailbox(cmd0), ag0) = null)) ∧ (∀ cmd, ag. s(Mailbox(cmd), ag) ≠ null → (∀ str0, ag0. s(state(str0), ag0) = null) ∧ (∀ cmd0, ag0. ag ≠ ag0 ∨ cmd0 ≠ cmd → s(Mailbox(cmd0), ag0) = null)) | An Axiom |
| maxOneNotNull-other-def | ⊦ maxOneNotNull(s) ↔ stateNotNull(s) ∧ mailboxNotNull(s) | An Axiom |
| allNull-maxOneNotNull | ⊦ allNull(s) → maxOneNotNull(s) | An Axiom |
| maxOneNotNull-locvar | ⊦ maxOneNotNull(s(locVar(str), ag ; d)) ↔ maxOneNotNull(s) | An Axiom |
| maxOneNotNull-locvar-01 | ⊦ maxOneNotNull(s(locVar(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-02 | ⊦ maxOneNotNull(s(declassify-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-04 | ⊦ maxOneNotNull(s(User-GetInput-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-05 | ⊦ maxOneNotNull(s(User-GetInput(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-06 | ⊦ maxOneNotNull(s(User-GetSingleSelection-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-07 | ⊦ maxOneNotNull(s(User-GetSingleSelection(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-08 | ⊦ maxOneNotNull(s(User-ConfirmRelease-count(str), ag ; d)) ↔ maxOneNotNull(s) | An Axiom |
| maxOneNotNull-misc-09 | ⊦ maxOneNotNull(s(User-ConfirmedRelease-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-misc-10 | ⊦ maxOneNotNull(s(User-ConfirmRelease-count(str), ag ; d)(nam, ag0 ; d0)) ↔ maxOneNotNull(s(nam, ag0 ; d0)) | An Axiom |
| maxOneNotNull-next | ⊦ s(Mailbox(cmd), ag) = wrapMessage2Data(msg) ∧ maxOneNotNull(s) → maxOneNotNull(s(Mailbox(cmd), ag ; null)(state(str0), ag0 ; wrapBoolean2Data(mkBoolean(true)))) | An Axiom |
| maxOneNotNull-next-01 | ⊦ maxOneNotNull(s) ∧ s(state(str0), ag0) ≠ null → maxOneNotNull(s(state(str0), ag0 ; null)(Mailbox(cmd), ag ; d)) | An Axiom |
| maxOneNotNull-next-02 | ⊦ maxOneNotNull(s) ∧ s(state(str0), ag0) ≠ null → maxOneNotNull(s(state(str0), ag0 ; null)(state(str), ag ; d)) | An Axiom |
| maxOneNotNull-next-03 | ⊦ s(Mailbox(cmd), ag) = wrapMessage2Data(msg) ∧ maxOneNotNull(s) → maxOneNotNull(s(Mailbox(cmd), ag ; null)(Mailbox(cmd0), ag0 ; d)) | An Axiom |
| maxOneNotNull-null | ⊦ maxOneNotNull(s) → maxOneNotNull(s(Mailbox(cmd), ag ; null)) | An Axiom |