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 | ⊦ mk(ar, i, i0, i1) .len = i1 | An Axiom |
| sel-02 | ⊦ mk(ar, i, i0, i1) .first = i0 | An Axiom |
| sel-03 | ⊦ mk(ar, i, i0, i1) .size = i | An Axiom |
| sel-04 | ⊦ mk(ar, i, i0, i1) .data = ar | An Axiom |
| inj | ⊦ mk(ar, i, i0, i1) = mk(ar0, i2, i3, i4) ↔ ar = ar0 ∧ i = i2 ∧ i0 = i3 ∧ i1 = i4 | An Axiom |
| case | ⊦ mk(buf .data, buf .size, buf .first, buf .len) = buf | An Axiom |
| elim | ⊦ ar = buf .data ∧ i = buf .size ∧ i0 = buf .first ∧ i1 = buf .len ↔ buf = mk(ar, i, i0, i1) | An Axiom |
| gen | An Axiom | |
| updsel-01 | ⊦ (buf .data:= ar) .data = ar | An Axiom |
| updsel-02 | ⊦ (buf .size:= i) .data = buf .data | An Axiom |
| updsel-03 | ⊦ (buf .first:= i0) .data = buf .data | An Axiom |
| updsel-04 | ⊦ (buf .len:= i1) .data = buf .data | An Axiom |
| updsel-05 | ⊦ (buf .data:= ar) .size = buf .size | An Axiom |
| updsel-06 | ⊦ (buf .size:= i) .size = i | An Axiom |
| updsel-07 | ⊦ (buf .first:= i0) .size = buf .size | An Axiom |
| updsel-08 | ⊦ (buf .len:= i1) .size = buf .size | An Axiom |
| updsel-09 | ⊦ (buf .data:= ar) .first = buf .first | An Axiom |
| updsel-10 | ⊦ (buf .size:= i) .first = buf .first | An Axiom |
| updsel-11 | ⊦ (buf .first:= i0) .first = i0 | An Axiom |
| updsel-12 | ⊦ (buf .len:= i1) .first = buf .first | An Axiom |
| updsel-13 | ⊦ (buf .data:= ar) .len = buf .len | An Axiom |
| updsel-14 | ⊦ (buf .size:= i) .len = buf .len | An Axiom |
| updsel-15 | ⊦ (buf .first:= i0) .len = buf .len | An Axiom |
| updsel-16 | ⊦ (buf .len:= i1) .len = i1 | An Axiom |
| upd-01 | ⊦ mk(ar, i, i0, i1) .data:= ar0 = mk(ar0, i, i0, i1) | An Axiom |
| upd-02 | ⊦ mk(ar, i, i0, i1) .size:= i2 = mk(ar, i2, i0, i1) | An Axiom |
| upd-03 | ⊦ mk(ar, i, i0, i1) .first:= i3 = mk(ar, i, i3, i1) | An Axiom |
| upd-04 | ⊦ mk(ar, i, i0, i1) .len:= i4 = mk(ar, i, i0, i4) | An Axiom |