This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| inj | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar) = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0) ↔ aehdr = aehdr0 ∧ avhdr = avhdr0 ∧ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0) | An Axiom |
| case | ⊦ mkpeb(apeb.echdr, apeb.vidhdr, apeb.data, apeb.fill, apeb.bad) = apeb | An Axiom |
| elim | ⊦ (((aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar) | An Axiom |
| gen | apeb freely generated by mkpeb; | An Axiom |
| updsel-10 | ⊦ (apeb.echdr:= aehdr).echdr = aehdr | An Axiom |
| updsel-11 | ⊦ (apeb.vidhdr:= avhdr).echdr = apeb.echdr | An Axiom |
| updsel-12 | ⊦ (apeb.data:= buf).echdr = apeb.echdr | An Axiom |
| updsel-13 | ⊦ (apeb.fill:= m).echdr = apeb.echdr | An Axiom |
| updsel-14 | ⊦ (apeb.bad:= boolvar).echdr = apeb.echdr | An Axiom |
| updsel-15 | ⊦ (apeb.echdr:= aehdr).vidhdr = apeb.vidhdr | An Axiom |
| updsel-16 | ⊦ (apeb.vidhdr:= avhdr).vidhdr = avhdr | An Axiom |
| updsel-17 | ⊦ (apeb.data:= buf).vidhdr = apeb.vidhdr | An Axiom |
| updsel-18 | ⊦ (apeb.fill:= m).vidhdr = apeb.vidhdr | An Axiom |
| updsel-19 | ⊦ (apeb.bad:= boolvar).vidhdr = apeb.vidhdr | An Axiom |
| updsel-20 | ⊦ (apeb.echdr:= aehdr).data = apeb.data | An Axiom |
| updsel-21 | ⊦ (apeb.vidhdr:= avhdr).data = apeb.data | An Axiom |
| updsel-22 | ⊦ (apeb.data:= buf).data = buf | An Axiom |
| updsel-23 | ⊦ (apeb.fill:= m).data = apeb.data | An Axiom |
| updsel-24 | ⊦ (apeb.bad:= boolvar).data = apeb.data | An Axiom |
| updsel-25 | ⊦ (apeb.echdr:= aehdr).fill = apeb.fill | An Axiom |
| updsel-26 | ⊦ (apeb.vidhdr:= avhdr).fill = apeb.fill | An Axiom |
| updsel-27 | ⊦ (apeb.data:= buf).fill = apeb.fill | An Axiom |
| updsel-28 | ⊦ (apeb.fill:= m).fill = m | An Axiom |
| updsel-29 | ⊦ (apeb.bad:= boolvar).fill = apeb.fill | An Axiom |
| updsel-30 | ⊦ (apeb.echdr:= aehdr).bad ↔ apeb.bad | An Axiom |
| updsel-31 | ⊦ (apeb.vidhdr:= avhdr).bad ↔ apeb.bad | An Axiom |
| updsel-32 | ⊦ (apeb.data:= buf).bad ↔ apeb.bad | An Axiom |
| updsel-33 | ⊦ (apeb.fill:= m).bad ↔ apeb.bad | An Axiom |
| updsel-34 | ⊦ (apeb.bad:= boolvar).bad ↔ boolvar | An Axiom |
| upd-04 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr:= aehdr0 = mkpeb(aehdr0, avhdr, buf, m, boolvar) | An Axiom |
| upd-05 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr:= avhdr0 = mkpeb(aehdr, avhdr0, buf, m, boolvar) | An Axiom |
| upd-06 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data:= buf0 = mkpeb(aehdr, avhdr, buf0, m, boolvar) | An Axiom |
| upd-07 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill:= m0 = mkpeb(aehdr, avhdr, buf, m0, boolvar) | An Axiom |
| upd-08 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad:= boolvar0 = mkpeb(aehdr, avhdr, buf, m, boolvar0) | An Axiom |
| sel-04 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr | An Axiom |
| sel-05 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr | An Axiom |
| sel-06 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf | An Axiom |
| sel-07 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m | An Axiom |
| sel-08 | ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar | An Axiom |