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 | ⊦ avidhdr(v, m, m0, m1, m2) = avidhdr(v0, m3, m4, m5, m6) ↔ v = v0 ∧ m = m3 ∧ m0 = m4 ∧ m1 = m5 ∧ m2 = m6 | An Axiom |
| case | ⊦ avhdr = empty ∨ avhdr = garbage ∨ avhdr = avidhdr(avhdr.vol, avhdr.leb, avhdr.sqn, avhdr.size, avhdr.checksum) | An Axiom |
| gen | avidheader freely generated by empty, garbage, avidhdr; | An Axiom |
| upd-06 | ⊦ avidhdr(v, m, m0, m1, m2).checksum:= m6 = avidhdr(v, m, m0, m1, m6) | An Axiom |
| upd-07 | ⊦ avidhdr(v, m, m0, m1, m2).size:= m5 = avidhdr(v, m, m0, m5, m2) | An Axiom |
| upd-08 | ⊦ avidhdr(v, m, m0, m1, m2).vol:= v0 = avidhdr(v0, m, m0, m1, m2) | An Axiom |
| upd-09 | ⊦ avidhdr(v, m, m0, m1, m2).sqn:= m4 = avidhdr(v, m, m4, m1, m2) | An Axiom |
| upd-10 | ⊦ avidhdr(v, m, m0, m1, m2).leb:= m3 = avidhdr(v, m3, m0, m1, m2) | An Axiom |
| sel-06 | ⊦ avidhdr(v, m, m0, m1, m2).vol = v | An Axiom |
| sel-07 | ⊦ avidhdr(v, m, m0, m1, m2).checksum = m2 | An Axiom |
| sel-08 | ⊦ avidhdr(v, m, m0, m1, m2).leb = m | An Axiom |
| sel-09 | ⊦ avidhdr(v, m, m0, m1, m2).size = m1 | An Axiom |
| sel-10 | ⊦ avidhdr(v, m, m0, m1, m2).sqn = m0 | An Axiom |
| disj-01 | ⊦ empty ≠ garbage | An Axiom |
| disj-02 | ⊦ empty ≠ avidhdr(v, m, m0, m1, m2) | An Axiom |
| disj-03 | ⊦ garbage ≠ avidhdr(v, m, m0, m1, m2) | An Axiom |
| elim | ⊦ avhdr.valid? → ((((v = avhdr.vol ∧ m = avhdr.leb) ∧ m0 = avhdr.sqn) ∧ m1 = avhdr.size) ∧ m2 = avhdr.checksum ↔ avhdr = avidhdr(v, m, m0, m1, m2)) | An Axiom |
| ex | ⊦ avhdr.valid? ↔ (∃ v, m, m0, m1, m2. avhdr = avidhdr(v, m, m0, m1, m2)) | An Axiom |
| test-01 | ⊦ ¬ empty.valid? | An Axiom |
| test-02 | ⊦ ¬ garbage.valid? | An Axiom |
| test-03 | ⊦ avidhdr(v, m, m0, m1, m2).valid? | An Axiom |
| updsel-01 | ⊦ avhdr.valid? → (avhdr.vol:= v).vol = v | An Axiom |
| updsel-02 | ⊦ avhdr.valid? → (avhdr.vol:= v).checksum = avhdr.checksum | An Axiom |
| updsel-03 | ⊦ avhdr.valid? → (avhdr.vol:= v).leb = avhdr.leb | An Axiom |
| updsel-04 | ⊦ avhdr.valid? → (avhdr.checksum:= m2).checksum = m2 | An Axiom |
| updsel-05 | ⊦ avhdr.valid? → (avhdr.vol:= v).sqn = avhdr.sqn | An Axiom |
| updsel-06 | ⊦ avhdr.valid? → (avhdr.leb:= m).checksum = avhdr.checksum | An Axiom |
| updsel-07 | ⊦ avhdr.valid? → (avhdr.vol:= v).size = avhdr.size | An Axiom |
| updsel-08 | ⊦ avhdr.valid? → (avhdr.checksum:= m2).size = avhdr.size | An Axiom |
| updsel-09 | ⊦ avhdr.valid? → (avhdr.sqn:= m0).checksum = avhdr.checksum | An Axiom |
| updsel-10 | ⊦ avhdr.valid? → (avhdr.checksum:= m2).sqn = avhdr.sqn | An Axiom |
| updsel-11 | ⊦ avhdr.valid? → (avhdr.leb:= m).vol = avhdr.vol | An Axiom |
| updsel-12 | ⊦ avhdr.valid? → (avhdr.size:= m1).checksum = avhdr.checksum | An Axiom |
| updsel-13 | ⊦ avhdr.valid? → (avhdr.leb:= m).leb = m | An Axiom |
| updsel-14 | ⊦ avhdr.valid? → (avhdr.size:= m1).size = m1 | An Axiom |
| updsel-15 | ⊦ avhdr.valid? → (avhdr.leb:= m).sqn = avhdr.sqn | An Axiom |
| updsel-16 | ⊦ avhdr.valid? → (avhdr.size:= m1).sqn = avhdr.sqn | An Axiom |
| updsel-17 | ⊦ avhdr.valid? → (avhdr.leb:= m).size = avhdr.size | An Axiom |
| updsel-18 | ⊦ avhdr.valid? → (avhdr.size:= m1).leb = avhdr.leb | An Axiom |
| updsel-19 | ⊦ avhdr.valid? → (avhdr.checksum:= m2).leb = avhdr.leb | An Axiom |
| updsel-20 | ⊦ avhdr.valid? → (avhdr.size:= m1).vol = avhdr.vol | An Axiom |
| updsel-21 | ⊦ avhdr.valid? → (avhdr.sqn:= m0).vol = avhdr.vol | An Axiom |
| updsel-22 | ⊦ avhdr.valid? → (avhdr.checksum:= m2).vol = avhdr.vol | An Axiom |
| updsel-23 | ⊦ avhdr.valid? → (avhdr.sqn:= m0).leb = avhdr.leb | An Axiom |
| updsel-24 | ⊦ avhdr.valid? → (avhdr.sqn:= m0).size = avhdr.size | An Axiom |
| updsel-25 | ⊦ avhdr.valid? → (avhdr.sqn:= m0).sqn = m0 | An Axiom |
| not-garbage-valid-imp-empty | ⊦ avhdr ≠ garbage → (avhdr.valid? ↔ avhdr ≠ empty) | A User Theorem |