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: |
|---|---|---|
| sel-01 | ⊦ @(m, m0).size = m0 | An Axiom |
| sel-02 | ⊦ @(m, m0).off = m | An Axiom |
| upd-01 | ⊦ @(m, m0).size:= m2 = @(m, m2) | An Axiom |
| upd-02 | ⊦ @(m, m0).off:= m1 = @(m1, m0) | An Axiom |
| updsel-01 | ⊦ (ladr.size:= m0).size = m0 | An Axiom |
| updsel-02 | ⊦ (ladr.off:= m).size = ladr.size | An Axiom |
| updsel-03 | ⊦ (ladr.size:= m0).off = ladr.off | An Axiom |
| updsel-04 | ⊦ (ladr.off:= m).off = m | An Axiom |
| inj | ⊦ @(m, m0) = @(m1, m2) ↔ m = m1 ∧ m0 = m2 | An Axiom |
| case | ⊦ @(ladr.off, ladr.size) = ladr | An Axiom |
| elim | ⊦ m = ladr.off ∧ m0 = ladr.size ↔ ladr = @(m, m0) | An Axiom |
| gen | An Axiom |