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: |
|---|---|---|
| updsel-01 | ⊦ (adr.pos:= m0).pos = m0 | An Axiom |
| updsel-02 | ⊦ (adr.lnum:= m).pos = adr.pos | An Axiom |
| updsel-03 | ⊦ (adr.pos:= m0).lnum = adr.lnum | An Axiom |
| updsel-04 | ⊦ (adr.lnum:= m).lnum = m | An Axiom |
| inj | ⊦ @(m, m0, m1) = @(m2, m3, m4) ↔ m = m2 ∧ m0 = m3 ∧ m1 = m4 | An Axiom |
| case | ⊦ @(adr.lnum, adr.pos, adr.size) = adr | An Axiom |
| elim | ⊦ (m = adr.lnum ∧ m0 = adr.pos) ∧ m1 = adr.size ↔ adr = @(m, m0, m1) | An Axiom |
| gen | An Axiom | |
| updsel-05 | ⊦ (adr.size:= m1).lnum = adr.lnum | An Axiom |
| updsel-06 | ⊦ (adr.size:= m1).pos = adr.pos | An Axiom |
| updsel-07 | ⊦ (adr.lnum:= m).size = adr.size | An Axiom |
| updsel-08 | ⊦ (adr.pos:= m0).size = adr.size | An Axiom |
| updsel-09 | ⊦ (adr.size:= m1).size = m1 | An Axiom |
| upd-03 | ⊦ @(m, m0, m1).lnum:= m2 = @(m2, m0, m1) | An Axiom |
| upd-04 | ⊦ @(m, m0, m1).pos:= m3 = @(m, m3, m1) | An Axiom |
| upd-05 | ⊦ @(m, m0, m1).size:= m4 = @(m, m0, m4) | An Axiom |
| sel-03 | ⊦ @(m, m0, m1).lnum = m | An Axiom |
| sel-04 | ⊦ @(m, m0, m1).pos = m0 | An Axiom |
| sel-05 | ⊦ @(m, m0, m1).size = m1 | An Axiom |