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-01 | ⊦ LP_FREE ≠ LP_GROUP_NODES | An Axiom |
| disj-02 | ⊦ LP_GROUP_NODES ≠ LP_INDEX_NODES | An Axiom |
| disj-03 | ⊦ LP_FREE ≠ LP_INDEX_NODES | An Axiom |
| updsel-01 | ⊦ (lp.flags:= lpf).flags = lpf | An Axiom |
| updsel-02 | ⊦ (lp.size:= m0).flags = lp.flags | An Axiom |
| updsel-03 | ⊦ (lp.ref-size:= m).flags = lp.flags | An Axiom |
| updsel-04 | ⊦ (lp.flags:= lpf).size = lp.size | An Axiom |
| updsel-05 | ⊦ (lp.size:= m0).size = m0 | An Axiom |
| updsel-06 | ⊦ (lp.ref-size:= m).size = lp.size | An Axiom |
| updsel-07 | ⊦ (lp.flags:= lpf).ref-size = lp.ref-size | An Axiom |
| updsel-08 | ⊦ (lp.size:= m0).ref-size = lp.ref-size | An Axiom |
| updsel-09 | ⊦ (lp.ref-size:= m).ref-size = m | An Axiom |
| inj | ⊦ mklp(m, m0, lpf, m1) = mklp(m2, m3, lpf0, m4) ↔ m = m2 ∧ m0 = m3 ∧ lpf = lpf0 ∧ m1 = m4 | An Axiom |
| case-02 | ⊦ lpf = LP_FREE ∨ lpf = LP_GROUP_NODES ∨ lpf = LP_INDEX_NODES | An Axiom |
| elim | ⊦ ((m = lp.ref-size ∧ m0 = lp.size) ∧ lpf = lp.flags) ∧ m1 = lp.gcheapidx ↔ lp = mklp(m, m0, lpf, m1) | An Axiom |
| gen | An Axiom | |
| case-03 | ⊦ mklp(lp.ref-size, lp.size, lp.flags, lp.gcheapidx) = lp | An Axiom |
| updsel-10 | ⊦ (lp.gcheapidx:= m1).ref-size = lp.ref-size | An Axiom |
| updsel-11 | ⊦ (lp.gcheapidx:= m1).size = lp.size | An Axiom |
| updsel-12 | ⊦ (lp.gcheapidx:= m1).flags = lp.flags | An Axiom |
| updsel-13 | ⊦ (lp.ref-size:= m).gcheapidx = lp.gcheapidx | An Axiom |
| updsel-14 | ⊦ (lp.size:= m0).gcheapidx = lp.gcheapidx | An Axiom |
| updsel-15 | ⊦ (lp.flags:= lpf).gcheapidx = lp.gcheapidx | An Axiom |
| updsel-16 | ⊦ (lp.gcheapidx:= m1).gcheapidx = m1 | An Axiom |
| upd-04 | ⊦ mklp(m, m0, lpf, m1).ref-size:= m2 = mklp(m2, m0, lpf, m1) | An Axiom |
| upd-05 | ⊦ mklp(m, m0, lpf, m1).size:= m3 = mklp(m, m3, lpf, m1) | An Axiom |
| upd-06 | ⊦ mklp(m, m0, lpf, m1).flags:= lpf0 = mklp(m, m0, lpf0, m1) | An Axiom |
| upd-07 | ⊦ mklp(m, m0, lpf, m1).gcheapidx:= m4 = mklp(m, m0, lpf, m4) | An Axiom |
| sel-04 | ⊦ mklp(m, m0, lpf, m1).ref-size = m | An Axiom |
| sel-05 | ⊦ mklp(m, m0, lpf, m1).size = m0 | An Axiom |
| sel-06 | ⊦ mklp(m, m0, lpf, m1).flags = lpf | An Axiom |
| sel-07 | ⊦ mklp(m, m0, lpf, m1).gcheapidx = m1 | An Axiom |