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: |
|---|---|---|
| sel-01 | ⊦ vidhdr(v, m, m0, m1, m2).checksum = m2 | An Axiom |
| sel-02 | ⊦ vidhdr(v, m, m0, m1, m2).size = m1 | An Axiom |
| sel-03 | ⊦ vidhdr(v, m, m0, m1, m2).vol = v | An Axiom |
| sel-04 | ⊦ vidhdr(v, m, m0, m1, m2).sqn = m0 | An Axiom |
| sel-05 | ⊦ vidhdr(v, m, m0, m1, m2).leb = m | An Axiom |
| upd-01 | ⊦ vidhdr(v, m, m0, m1, m2).vol:= v0 = vidhdr(v0, m, m0, m1, m2) | An Axiom |
| upd-02 | ⊦ vidhdr(v, m, m0, m1, m2).checksum:= m6 = vidhdr(v, m, m0, m1, m6) | An Axiom |
| upd-03 | ⊦ vidhdr(v, m, m0, m1, m2).leb:= m3 = vidhdr(v, m3, m0, m1, m2) | An Axiom |
| upd-04 | ⊦ vidhdr(v, m, m0, m1, m2).size:= m5 = vidhdr(v, m, m0, m5, m2) | An Axiom |
| upd-05 | ⊦ vidhdr(v, m, m0, m1, m2).sqn:= m4 = vidhdr(v, m, m4, m1, m2) | An Axiom |
| updsel-01 | ⊦ (vhdr.vol:= v).vol = v | An Axiom |
| updsel-02 | ⊦ (vhdr.checksum:= m2).vol = vhdr.vol | An Axiom |
| updsel-03 | ⊦ (vhdr.leb:= m).vol = vhdr.vol | An Axiom |
| updsel-04 | ⊦ (vhdr.checksum:= m2).checksum = m2 | An Axiom |
| updsel-05 | ⊦ (vhdr.sqn:= m0).vol = vhdr.vol | An Axiom |
| updsel-06 | ⊦ (vhdr.checksum:= m2).leb = vhdr.leb | An Axiom |
| updsel-07 | ⊦ (vhdr.size:= m1).vol = vhdr.vol | An Axiom |
| updsel-08 | ⊦ (vhdr.size:= m1).checksum = vhdr.checksum | An Axiom |
| updsel-09 | ⊦ (vhdr.checksum:= m2).sqn = vhdr.sqn | An Axiom |
| updsel-10 | ⊦ (vhdr.sqn:= m0).checksum = vhdr.checksum | An Axiom |
| updsel-11 | ⊦ (vhdr.vol:= v).leb = vhdr.leb | An Axiom |
| updsel-12 | ⊦ (vhdr.checksum:= m2).size = vhdr.size | An Axiom |
| updsel-13 | ⊦ (vhdr.leb:= m).leb = m | An Axiom |
| updsel-14 | ⊦ (vhdr.size:= m1).size = m1 | An Axiom |
| updsel-15 | ⊦ (vhdr.sqn:= m0).leb = vhdr.leb | An Axiom |
| updsel-16 | ⊦ (vhdr.sqn:= m0).size = vhdr.size | An Axiom |
| updsel-17 | ⊦ (vhdr.size:= m1).leb = vhdr.leb | An Axiom |
| updsel-18 | ⊦ (vhdr.leb:= m).size = vhdr.size | An Axiom |
| updsel-19 | ⊦ (vhdr.leb:= m).checksum = vhdr.checksum | An Axiom |
| updsel-20 | ⊦ (vhdr.vol:= v).size = vhdr.size | An Axiom |
| updsel-21 | ⊦ (vhdr.vol:= v).sqn = vhdr.sqn | An Axiom |
| updsel-22 | ⊦ (vhdr.vol:= v).checksum = vhdr.checksum | An Axiom |
| updsel-23 | ⊦ (vhdr.leb:= m).sqn = vhdr.sqn | An Axiom |
| updsel-24 | ⊦ (vhdr.size:= m1).sqn = vhdr.sqn | An Axiom |
| updsel-25 | ⊦ (vhdr.sqn:= m0).sqn = m0 | An Axiom |
| inj | ⊦ vidhdr(v, m, m0, m1, m2) = vidhdr(v0, m3, m4, m5, m6) ↔ v = v0 ∧ m = m3 ∧ m0 = m4 ∧ m1 = m5 ∧ m2 = m6 | An Axiom |
| case | ⊦ vidhdr(vhdr.vol, vhdr.leb, vhdr.sqn, vhdr.size, vhdr.checksum) = vhdr | An Axiom |
| elim | ⊦ (((v = vhdr.vol ∧ m = vhdr.leb) ∧ m0 = vhdr.sqn) ∧ m1 = vhdr.size) ∧ m2 = vhdr.checksum ↔ vhdr = vidhdr(v, m, m0, m1, m2) | An Axiom |
| gen | vidheader freely generated by vidhdr; | An Axiom |