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 | ⊦ mkfile(m, mode, m0).ino = m | An Axiom |
| upd | ⊦ mkfile(m, mode, m0).ino:= m1 = mkfile(m1, mode, m0) | An Axiom |
| inj | ⊦ mkfile(m, mode, m0) = mkfile(m1, mode0, m2) ↔ m = m1 ∧ mode = mode0 ∧ m0 = m2 | An Axiom |
| case | ⊦ mkfile(file.ino, file.mode, file.pos) = file | An Axiom |
| elim | ⊦ (m = file.ino ∧ mode = file.mode) ∧ m0 = file.pos ↔ file = mkfile(m, mode, m0) | An Axiom |
| gen | An Axiom | |
| updsel-01 | ⊦ (file.ino:= m).ino = m | An Axiom |
| updsel-02 | ⊦ (file.pos:= m0).ino = file.ino | An Axiom |
| updsel-03 | ⊦ (file.ino:= m).pos = file.pos | An Axiom |
| updsel-04 | ⊦ (file.pos:= m0).pos = m0 | An Axiom |
| updsel-05 | ⊦ (file.mode:= mode).ino = file.ino | An Axiom |
| updsel-06 | ⊦ (file.ino:= m).mode = file.mode | An Axiom |
| updsel-07 | ⊦ (file.mode:= mode).mode = mode | An Axiom |
| updsel-08 | ⊦ (file.pos:= m0).mode = file.mode | An Axiom |
| updsel-09 | ⊦ (file.mode:= mode).pos = file.pos | An Axiom |
| upd-02 | ⊦ mkfile(m, mode, m0).mode:= mode0 = mkfile(m, mode0, m0) | An Axiom |
| upd-03 | ⊦ mkfile(m, mode, m0).pos:= m2 = mkfile(m, mode, m2) | An Axiom |
| sel-02 | ⊦ mkfile(m, mode, m0).mode = mode | An Axiom |
| sel-03 | ⊦ mkfile(m, mode, m0).pos = m0 | An Axiom |