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-01 | ⊦ (znd.dirty:= boolvar0).dirty ↔ boolvar0 | An Axiom |
| updsel-02 | ⊦ (znd.leaf:= boolvar).parent = znd.parent | An Axiom |
| updsel-03 | ⊦ (znd.zbranches:= zbrar).parent = znd.parent | An Axiom |
| updsel-05 | ⊦ (znd.parent:= r).dirty ↔ znd.dirty | An Axiom |
| updsel-06 | ⊦ (znd.leaf:= boolvar).dirty ↔ znd.dirty | An Axiom |
| updsel-08 | ⊦ (znd.zbranches:= zbrar).dirty ↔ znd.dirty | An Axiom |
| updsel-09 | ⊦ (znd.dirty:= boolvar0).leaf ↔ znd.leaf | An Axiom |
| updsel-10 | ⊦ (znd.leaf:= boolvar).zbranches = znd.zbranches | An Axiom |
| updsel-12 | ⊦ (znd.leaf:= boolvar).leaf ↔ boolvar | An Axiom |
| updsel-13 | ⊦ (znd.parent:= r).zbranches = znd.zbranches | An Axiom |
| updsel-14 | ⊦ (znd.dirty:= boolvar0).zbranches = znd.zbranches | An Axiom |
| updsel-17 | ⊦ (znd.parent:= r).leaf ↔ znd.leaf | An Axiom |
| updsel-18 | ⊦ (znd.zbranches:= zbrar).leaf ↔ znd.leaf | An Axiom |
| updsel-21 | ⊦ (znd.dirty:= boolvar0).parent = znd.parent | An Axiom |
| updsel-23 | ⊦ (znd.zbranches:= zbrar).zbranches = zbrar | An Axiom |
| updsel-25 | ⊦ (znd.parent:= r).parent = r | An Axiom |
| inj | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m) = mkznode(r0, zbrar0, boolvar1, boolvar2, m0) ↔ r = r0 ∧ zbrar = zbrar0 ∧ (boolvar ↔ boolvar1) ∧ (boolvar0 ↔ boolvar2) ∧ m = m0 | An Axiom |
| case | ⊦ mkznode(znd.parent, znd.zbranches, znd.leaf, znd.dirty, znd.usedsize) = znd | An Axiom |
| elim | ⊦ (((r = znd.parent ∧ zbrar = znd.zbranches) ∧ (boolvar ↔ znd.leaf)) ∧ (boolvar0 ↔ znd.dirty)) ∧ m = znd.usedsize ↔ znd = mkznode(r, zbrar, boolvar, boolvar0, m) | An Axiom |
| gen | znode freely generated by mkznode; | An Axiom |
| updsel-26 | ⊦ (znd.usedsize:= m).parent = znd.parent | An Axiom |
| updsel-28 | ⊦ (znd.usedsize:= m).zbranches = znd.zbranches | An Axiom |
| updsel-29 | ⊦ (znd.usedsize:= m).leaf ↔ znd.leaf | An Axiom |
| updsel-30 | ⊦ (znd.usedsize:= m).dirty ↔ znd.dirty | An Axiom |
| updsel-31 | ⊦ (znd.parent:= r).usedsize = znd.usedsize | An Axiom |
| updsel-33 | ⊦ (znd.zbranches:= zbrar).usedsize = znd.usedsize | An Axiom |
| updsel-34 | ⊦ (znd.leaf:= boolvar).usedsize = znd.usedsize | An Axiom |
| updsel-35 | ⊦ (znd.dirty:= boolvar0).usedsize = znd.usedsize | An Axiom |
| updsel-36 | ⊦ (znd.usedsize:= m).usedsize = m | An Axiom |
| upd-01 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).parent:= r0 = mkznode(r0, zbrar, boolvar, boolvar0, m) | An Axiom |
| upd-02 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).zbranches:= zbrar0 = mkznode(r, zbrar0, boolvar, boolvar0, m) | An Axiom |
| upd-03 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).leaf:= boolvar1 = mkznode(r, zbrar, boolvar1, boolvar0, m) | An Axiom |
| upd-04 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).dirty:= boolvar2 = mkznode(r, zbrar, boolvar, boolvar2, m) | An Axiom |
| upd-05 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).usedsize:= m0 = mkznode(r, zbrar, boolvar, boolvar0, m0) | An Axiom |
| sel-01 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).parent = r | An Axiom |
| sel-02 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).zbranches = zbrar | An Axiom |
| sel-03 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).leaf ↔ boolvar | An Axiom |
| sel-04 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).dirty ↔ boolvar0 | An Axiom |
| sel-05 | ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).usedsize = m | An Axiom |