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: |
|---|---|---|
| updsel-02 | ⊦ (sb.log:= m0).indexaddr = sb.indexaddr | An Axiom |
| updsel-04 | ⊦ (sb.orph:= m1).indexaddr = sb.indexaddr | An Axiom |
| updsel-05 | ⊦ (sb.maxino:= m).main = sb.main | An Axiom |
| updsel-06 | ⊦ (sb.indexaddr:= adr).main = sb.main | An Axiom |
| updsel-08 | ⊦ (sb.orph:= m1).main = sb.main | An Axiom |
| updsel-10 | ⊦ (sb.log:= m0).main = sb.main | An Axiom |
| updsel-11 | ⊦ (sb.maxino:= m).log = sb.log | An Axiom |
| updsel-12 | ⊦ (sb.indexaddr:= adr).log = sb.log | An Axiom |
| updsel-14 | ⊦ (sb.log:= m0).maxino = sb.maxino | An Axiom |
| updsel-16 | ⊦ (sb.orph:= m1).maxino = sb.maxino | An Axiom |
| updsel-17 | ⊦ (sb.maxino:= m).lpt = sb.lpt | An Axiom |
| updsel-18 | ⊦ (sb.indexaddr:= adr).lpt = sb.lpt | An Axiom |
| updsel-20 | ⊦ (sb.orph:= m1).lpt = sb.lpt | An Axiom |
| updsel-22 | ⊦ (sb.log:= m0).lpt = sb.lpt | An Axiom |
| updsel-23 | ⊦ (sb.maxino:= m).orph = sb.orph | An Axiom |
| updsel-24 | ⊦ (sb.indexaddr:= adr).orph = sb.orph | An Axiom |
| updsel-26 | ⊦ (sb.log:= m0).log = m0 | An Axiom |
| updsel-28 | ⊦ (sb.orph:= m1).log = sb.log | An Axiom |
| updsel-29 | ⊦ (sb.maxino:= m).maxino = m | An Axiom |
| updsel-30 | ⊦ (sb.indexaddr:= adr).maxino = sb.maxino | An Axiom |
| updsel-32 | ⊦ (sb.orph:= m1).orph = m1 | An Axiom |
| updsel-34 | ⊦ (sb.log:= m0).orph = sb.orph | An Axiom |
| updsel-35 | ⊦ (sb.maxino:= m).indexaddr = sb.indexaddr | An Axiom |
| updsel-36 | ⊦ (sb.indexaddr:= adr).indexaddr = adr | An Axiom |
| inj | ⊦ mksb(adr, m, m0, m1, m2, m3, m4) = mksb(adr0, m5, m6, m7, m8, m9, m10) ↔ adr = adr0 ∧ m = m5 ∧ m0 = m6 ∧ m1 = m7 ∧ m2 = m8 ∧ m3 = m9 ∧ m4 = m10 | An Axiom |
| case | ⊦ mksb(sb.indexaddr, sb.maxino, sb.log, sb.orph, sb.orphsize, sb.lpt, sb.main) = sb | An Axiom |
| elim | ⊦ (((((adr = sb.indexaddr ∧ m = sb.maxino) ∧ m0 = sb.log) ∧ m1 = sb.orph) ∧ m2 = sb.orphsize) ∧ m3 = sb.lpt) ∧ m4 = sb.main ↔ sb = mksb(adr, m, m0, m1, m2, m3, m4) | An Axiom |
| gen | superblock freely generated by mksb; | An Axiom |
| updsel-37 | ⊦ (sb.orphsize:= m2).indexaddr = sb.indexaddr | An Axiom |
| updsel-38 | ⊦ (sb.lpt:= m3).indexaddr = sb.indexaddr | An Axiom |
| updsel-39 | ⊦ (sb.main:= m4).indexaddr = sb.indexaddr | An Axiom |
| updsel-40 | ⊦ (sb.orphsize:= m2).maxino = sb.maxino | An Axiom |
| updsel-41 | ⊦ (sb.lpt:= m3).maxino = sb.maxino | An Axiom |
| updsel-42 | ⊦ (sb.main:= m4).maxino = sb.maxino | An Axiom |
| updsel-43 | ⊦ (sb.orphsize:= m2).log = sb.log | An Axiom |
| updsel-44 | ⊦ (sb.lpt:= m3).log = sb.log | An Axiom |
| updsel-45 | ⊦ (sb.main:= m4).log = sb.log | An Axiom |
| updsel-46 | ⊦ (sb.orphsize:= m2).orph = sb.orph | An Axiom |
| updsel-47 | ⊦ (sb.lpt:= m3).orph = sb.orph | An Axiom |
| updsel-48 | ⊦ (sb.main:= m4).orph = sb.orph | An Axiom |
| updsel-49 | ⊦ (sb.indexaddr:= adr).orphsize = sb.orphsize | An Axiom |
| updsel-50 | ⊦ (sb.maxino:= m).orphsize = sb.orphsize | An Axiom |
| updsel-51 | ⊦ (sb.log:= m0).orphsize = sb.orphsize | An Axiom |
| updsel-52 | ⊦ (sb.orph:= m1).orphsize = sb.orphsize | An Axiom |
| updsel-53 | ⊦ (sb.orphsize:= m2).orphsize = m2 | An Axiom |
| updsel-54 | ⊦ (sb.lpt:= m3).orphsize = sb.orphsize | An Axiom |
| updsel-55 | ⊦ (sb.main:= m4).orphsize = sb.orphsize | An Axiom |
| updsel-56 | ⊦ (sb.orphsize:= m2).lpt = sb.lpt | An Axiom |
| updsel-57 | ⊦ (sb.lpt:= m3).lpt = m3 | An Axiom |
| updsel-58 | ⊦ (sb.main:= m4).lpt = sb.lpt | An Axiom |
| updsel-59 | ⊦ (sb.orphsize:= m2).main = sb.main | An Axiom |
| updsel-60 | ⊦ (sb.lpt:= m3).main = sb.main | An Axiom |
| updsel-61 | ⊦ (sb.main:= m4).main = m4 | An Axiom |
| upd-07 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).indexaddr:= adr0 = mksb(adr0, m, m0, m1, m2, m3, m4) | An Axiom |
| upd-08 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).maxino:= m5 = mksb(adr, m5, m0, m1, m2, m3, m4) | An Axiom |
| upd-09 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).log:= m6 = mksb(adr, m, m6, m1, m2, m3, m4) | An Axiom |
| upd-10 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orph:= m7 = mksb(adr, m, m0, m7, m2, m3, m4) | An Axiom |
| upd-11 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orphsize:= m8 = mksb(adr, m, m0, m1, m8, m3, m4) | An Axiom |
| upd-12 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).lpt:= m9 = mksb(adr, m, m0, m1, m2, m9, m4) | An Axiom |
| upd-13 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).main:= m10 = mksb(adr, m, m0, m1, m2, m3, m10) | An Axiom |
| sel-07 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).indexaddr = adr | An Axiom |
| sel-08 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).maxino = m | An Axiom |
| sel-09 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).log = m0 | An Axiom |
| sel-10 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orph = m1 | An Axiom |
| sel-11 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orphsize = m2 | An Axiom |
| sel-12 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).lpt = m3 | An Axiom |
| sel-13 | ⊦ mksb(adr, m, m0, m1, m2, m3, m4).main = m4 | An Axiom |