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: |
|---|---|---|
| look | ⊦ look(bv, key, adr, ri) ↔ (bv ↔ key ∈ ri) ∧ (bv → adr = ri[key]) | An Axiom |
| range-last | ⊦ n ≠ 0 ∧ n < # zbrar → key-range(zbrar, n, n + 1, ri) = ri |> zbrar[n - 1].key | An Axiom |
| range-inner | ⊦ n ≠ 0 ∧ n + 1 < nused ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ri) = (ri |> zbrar[n - 1].key) |≤ zbrar[n].key | An Axiom |
| range-first | ⊦ nused ≠ 0 ∧ nused < # zbrar → key-range(zbrar, 0, nused + 1, ri) = ri |≤ zbrar[0].key | An Axiom |
| range-one | ⊦ key-range(zbrar, 0, 1, ri) = ri | An Axiom |
| keys-rec | ⊦ m < # zbrar → keys(zbrar, m, nused + 1) = keys(zbrar, m + 1, nused) ++ zbrar[m].key | An Axiom |
| keys-base | ⊦ keys(zbrar, m, 0) = ∅ | An Axiom |
| payload-rec | ⊦ m < # zbrar → payload(zbrar, m, nused + 1) = (zbrar[m].entry? ⊃ payload(zbrar, m + 1, nused)[zbrar[m].key, zbrar[m].adr];payload(zbrar, m + 1, nused)) | An Axiom |
| payload-base | ⊦ payload(zbrar, m, 0) = ∅ | An Axiom |
| ri-compatible | nused ≠ 0 ⊦ compatible(ri0, ri1, zbrar, n, nused) ↔ sorted(zbrar, 0, nused - 1) → (∀ m. m ≠ n ∧ m < nused → key-range(zbrar, m, nused, ri0) = key-range(zbrar, m, nused, ri1)) | An Axiom |
| unmodified | ⊦ unmodified(adr, znd, iast) ↔ ¬ znd.dirty → adr ∈ iast ∧ iast[adr] = save(znd) | An Axiom |
| nsze-underfull | ⊦ nsize(nused, underfull?) ↔ nused < BRANCH_SIZE | An Axiom |
| nsze-overfull | ⊦ nsize(nused, overfull?) ↔ nused ≤ BRANCH_SIZE | An Axiom |
| nsze-ok | ⊦ nsize(nused, ok) ↔ nused < BRANCH_SIZE | An Axiom |
| at-payload | m + nused ≤ # zbrar, n < nused, zbrar[m + n] = mkzentry(key, adr), ∀ n0. n0 < n ∧ zbrar[m + n0].entry? → zbrar[m + n0].key ≠ key ⊦ payload(zbrar, m, nused)[key] = adr | A User Theorem |
| at-range | ⊦ key ∈ key-range(zbrar, n, nused, ri) ∧ n < nused ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ri)[key] = ri[key] | A User Theorem |
| in-keyrange-in-ri | n < nused, nused ≤ # zbrar ⊦ key ∈ key-range(zbrar, n, nused, ri) → key ∈ ri | A User Theorem |
| in-keyrange-in-ri-data | n < nused, nused ≤ # zbrar ⊦ adr ∈ key-range(zbrar, n, nused, ri) → adr ∈ ri | A User Theorem |
| in-keys | m + nused ≤ # zbrar ⊦ key ∈ keys(zbrar, m, nused) ↔ (∃ n. n < nused ∧ zbrar[m + n].key = key) | A User Theorem |
| in-payload | m + nused ≤ # zbrar ⊦ key ∈ payload(zbrar, m, nused) ↔ (∃ n. n < nused ∧ zbrar[m + n].entry? ∧ zbrar[m + n].key = key) | A User Theorem |
| in-playload-data | n + m ≤ # zbrar ⊦ sorted(zbrar, 0, n + m) → (adr ∈ payload(zbrar, n, m) ↔ (∃ m0. n ≤ m0 ∧ m0 < n + m ∧ zbrar[m0].entry? ∧ zbrar[m0].adr = adr)) | A User Theorem |
| keep-range | ⊦ zbr.key = zbrar[m].key ∧ m < # zbrar ∧ n < nused ∧ nused ≤ # zbrar → key-range(zbrar[m, zbr], n, nused, ri) = key-range(zbrar, n, nused, ri) | A User Theorem |
| key-range-replace-branches | ⊦ n < m ∧ m ≤ # zbrar0 ∧ # zbrar0 = # zbrar1 ∧ (∀ n0. n0 ≤ n ∧ n0 ≤ m → zbrar0[n0].key = zbrar1[n0].key) → key-range(zbrar0, n, m, ri) = key-range(zbrar1, n, m, ri) | A User Theorem |
| keys-drop-lower | n ≠ 0, m + n + nused ≤ # zbrar ⊦ keys(zbrar[m, zbr], m + n, nused) = keys(zbrar, m + n, nused) | A User Theorem |
| keys-drop-upper | m + nused ≤ n, n ≤ # zbrar ⊦ keys(zbrar[n, zbr], m, nused) = keys(zbrar, m, nused) | A User Theorem |
| keys-mod | n < nused, m + nused ≤ # zbrar, zbrar[m + n].key = key, sorted(zbrar, m, nused) ⊦ keys(zbrar[m + n, mkzentry(key, adr)], m, nused) = keys(zbrar, m, nused) ++ key | A User Theorem |
| keys-mod-0 | n < nused, nused ≤ # zbrar, zbrar[n].key = key, sorted(zbrar, 0, nused) ⊦ keys(zbrar[n, mkzentry(key, adr)], 0, nused) = keys(zbrar, 0, nused) ++ key | A User Theorem |
| keys-shift-left | ⊦ n ≤ nused ∧ nused < # zbrar ∧ sorted(zbrar, 0, nused + 1) → keys(shl(zbrar, n, nused + 1), 0, nused) = keys(zbrar, 0, nused + 1) -- zbrar[n].key | A User Theorem |
| look-at | ⊦ look(true, key, adr, ri) → ri[key] = adr | A User Theorem |
| look-empty | ⊦ look(bv, key, adr, ∅) ↔ ¬ bv | A User Theorem |
| look-false | ⊦ look(false, key, adr, ri) ↔ ¬ key ∈ ri | A User Theorem |
| look-in | ⊦ look(true, key, adr, ri) → key ∈ ri | A User Theorem |
| look-scan-range | ⊦ len < # zbrar → (look(bv, key, adr, key-range(zbrar, scan(key, zbrar, 0, len), len + 1, ri)) ↔ look(bv, key, adr, ri)) | A User Theorem |
| look-subrange | n < nused ∧ nused ≤ # zbrar ⊦ look(bv, key, adr, key-range(zbrar, n, nused, ri)) ↔ (key ∈ key-range(zbrar, n, nused, ri) ⊃ look(bv, key, adr, ri);¬ bv) | A User Theorem |
| look-true | ⊦ look(true, key, adr, ri) ↔ key ∈ ri ∧ adr = ri[key] | A User Theorem |
| nsize-size | ⊦ nsize(m, nstat) → ¬ BRANCH_SIZE < m | A User Theorem |
| payload-copy-right-lower | m + nused + n < # zbrar ⊦ payload(copy(zbrar, m + nused, zbrar, m + nused + 1, n), m, nused) = payload(zbrar, m, nused) | A User Theorem |
| payload-copy-right-lower-0 | nused + n < # zbrar ⊦ payload(copy(zbrar, nused, zbrar, nused + 1, n), 0, nused) = payload(zbrar, 0, nused) | A User Theorem |
| payload-copy-right-upper | n + nused < # zbrar ⊦ payload(copy(zbrar, n, zbrar, n + 1, nused), n + 1, nused) = payload(zbrar, n, nused) | A User Theorem |
| payload-drop-lower | n ≠ 0, m + n + nused ≤ # zbrar ⊦ payload(zbrar[m, zbr], m + n, nused) = payload(zbrar, m + n, nused) | A User Theorem |
| payload-drop-upper | m + nused ≤ n, n ≤ # zbrar ⊦ payload(zbrar[n, zbr], m, nused) = payload(zbrar, m, nused) | A User Theorem |
| payload-keys | ⊦ key ∈ payload(zbrar, n, nused) ∧ nused + n ≤ # zbrar → key ∈ keys(zbrar, n, nused) | A User Theorem |
| payload-keys-0 | ⊦ key ∈ payload(zbrar, 0, nused) ∧ nused ≤ # zbrar → key ∈ keys(zbrar, 0, nused) | A User Theorem |
| payload-mod | n < nused, m + nused ≤ # zbrar, zbrar[m + n].key = key, sorted(zbrar, m, nused) ⊦ payload(zbrar[m + n, mkzentry(key, adr)], m, nused) = payload(zbrar, m, nused)[key, adr] | A User Theorem |
| payload-mod-0 | n < nused, nused ≤ # zbrar, zbrar[n].key = key, sorted(zbrar, 0, nused) ⊦ payload(zbrar[n, mkzentry(key, adr)], 0, nused) = payload(zbrar, 0, nused)[key, adr] | A User Theorem |
| payload-one | ⊦ m < # zbrar → payload(zbrar, m, 1) = (zbrar[m].entry? ⊃ (∅)[zbrar[m].key, zbrar[m].adr];∅) | A User Theorem |
| payload-save-load-same | # zbrar = BRANCH_SIZE, nused ≤ BRANCH_SIZE ⊦ payload(load(save(zbrar, 0, nused), 0, nused), 0, nused) = payload(zbrar, 0, nused) | A User Theorem |
| payload-shift-left | ⊦ n ≤ nused ∧ nused < # zbrar ∧ sorted(zbrar, 0, nused + 1) → payload(shl(zbrar, n, nused + 1), 0, nused) = (zbrar[n].entry? ⊃ payload(zbrar, 0, nused + 1) -- zbrar[n].key;payload(zbrar, 0, nused + 1)) | A User Theorem |
| payload-split | n ≤ nused, m + nused ≤ # zbrar ⊦ payload(zbrar, m, nused) = payload(zbrar, m, n) ⊕ payload(zbrar, m + n, nused - n) | A User Theorem |
| range | ⊦ n < nused ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ri) = (n = 0 ⊃ (nused = 1 ⊃ ri;ri |≤ zbrar[0].key);(n + 1 = nused ⊃ ri |> zbrar[n - 1].key;(ri |> zbrar[n - 1].key) |≤ zbrar[n].key)) | A User Theorem |
| range-emp | ⊦ n < nused ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ∅) = ∅ | A User Theorem |
| range-gt | ⊦ n ≠ 0 ∧ n < nused ∧ key ≤ zbrar[n - 1].key ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ri |> key) = key-range(zbrar, n, nused, ri) | A User Theorem |
| range-last-2 | ⊦ n + 1 < # zbrar → key-range(zbrar, n + 1, n + 2, ri) = ri |> zbrar[n].key | A User Theorem |
| range-le | ⊦ n + 1 < nused ∧ zbrar[n].key ≤ key ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ri |≤ key) = key-range(zbrar, n, nused, ri) | A User Theorem |
| range-load-save | ⊦ n < nused ∧ nused ≤ # zbrar ∧ # zbrar = BRANCH_SIZE → key-range(load(save(zbrar, 0, nused), 0, nused), n, nused, ri) = key-range(zbrar, n, nused, ri) | A User Theorem |
| range-put | n < nused, nused ≤ # zbrar, n ≠ 0 → zbrar[n - 1].key < key, nused ≠ 0 → key ≤ zbrar[n].key ⊦ key-range(zbrar, n, nused, ri[key, adr]) = key-range(zbrar, n, nused, ri)[key, adr] | A User Theorem |
| save-same-payload-same | ⊦ # zbrar0 = # zbrar1 ∧ n + m ≤ # zbrar0 ∧ # zbrar0 = BRANCH_SIZE ∧ save(zbrar0, n, m) = save(zbrar1, n, m) → payload(zbrar0, n, m) = payload(zbrar1, n, m) | A User Theorem |
| sorted-shift-left | n ≤ nused, nused < # zbrar, sorted(zbrar, 0, nused + 1) ⊦ sorted(shl(zbrar, n, nused + 1), 0, nused) | A User Theorem |
| unmodified-clean-eq-adr-subseteq | n < nused, nused ≤ BRANCH_SIZE, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ iast0 ⊆ iast1 ∧ zbrar0[n] = mkzbranch(key0, adr0, r0) ∧ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast0) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv, false, nused), iast1) ∧ zbrar1[n] = mkzbranch(key1, adr1, r1) → key1 = key0 ∧ adr1 = adr0 | A User Theorem |
| unmodified-clean-eq-keys | n < nused, nused ≤ BRANCH_SIZE, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv, false, nused), iast) → (zbrar1[n].key = zbrar0[n].key ↔ true) | A User Theorem |
| unmodified-clean-eq-keys-subseteq | n < nused, nused ≤ BRANCH_SIZE, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ iast0 ⊆ iast1 ∧ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast0) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv, false, nused), iast1) → (zbrar1[n].key = zbrar0[n].key ↔ true) | A User Theorem |
| unmodified-clean-fwd-zbrar | n < nused, nused ≤ BRANCH_SIZE, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ zbrar0[n] = mkzbranch(key, adr0, r2) ∧ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv, false, nused), iast) → (∃ r0. zbrar1[n] = mkzbranch(key, adr0, r0)) | A User Theorem |
| unmodified-clean-fwd-zbrar2 | n < nused, nused ≤ BRANCH_SIZE, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ zbrar0[n] = mkzentry(key, adr0) ∧ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv, false, nused), iast) → zbrar1[n] = mkzentry(key, adr0) | A User Theorem |
| unmodified-clean-leaf | ⊦ unmodified(adr, mkznode(rp0, zbrar0, bv0, false, nused0), iast) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv1, false, nused1), iast) → (bv0 ↔ bv1) ∧ nused0 = nused1 | A User Theorem |
| unmodified-clean-leaf-subseteq | ⊦ iast0 ⊆ iast1 ∧ unmodified(adr, mkznode(rp0, zbrar0, bv0, false, nused0), iast0) ∧ unmodified(adr, mkznode(rp1, zbrar1, bv1, false, nused1), iast1) → (bv0 ↔ bv1) ∧ nused0 = nused1 | A User Theorem |
| unmodified-dirty | ⊦ unmodified(adr, mkznode(rp, zbrar, bv, true, nused), iast) | A User Theorem |
| unmodified-key-range-node | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ n ≤ nused ∧ nused < BRANCH_SIZE ∧ # zbrar = BRANCH_SIZE ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused + 1), iast) → key-range(load(brar, 0, nused + 1), n, nused + 1, ri) = key-range(zbrar, n, nused + 1, ri) | A User Theorem |
| unmodified-load | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ unmodified(adr, mkznode(rp1, zbrar, bv1, false, nused), iast) → load(rp0, indexnode(brar, bv0, m)) = mkznode(rp0, load(brar, 0, nused), bv1, false, nused) | A User Theorem |
| unmodified-load-adr-node | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ n ≤ nused ∧ nused < BRANCH_SIZE ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused + 1), iast) → load(brar[n]).adr = zbrar[n].adr | A User Theorem |
| unmodified-load-key-leaf | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ n < nused ∧ nused ≤ BRANCH_SIZE ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused), iast) → load(brar[n]).key = zbrar[n].key | A User Theorem |
| unmodified-load-key-node | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ n < nused ∧ nused < BRANCH_SIZE ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused + 1), iast) → load(brar[n]).key = zbrar[n].key | A User Theorem |
| unmodified-payload | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ nused ≤ BRANCH_SIZE ∧ BRANCH_SIZE = # zbrar ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused), iast) ∧ sorted(zbrar, 0, nused) → payload(load(brar, 0, nused), 0, nused) = payload(zbrar, 0, nused) | A User Theorem |
| unmodified-reload | nused ≤ BRANCH_SIZE ⊦ iast[adr] = indexnode(brar, boolvar0, nused) ∧ unmodified(adr, mkznode(rp0, zbrar, boolvar, false, nused), iast) → unmodified(adr, mkznode(rp0, load(brar, 0, nused), boolvar, false, nused), iast) | A User Theorem |
| unmodified-same-payload | nused ≤ # zbrar0, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast) ∧ unmodified(adr, mkznode(rp2, zbrar1, bv, false, nused), iast) → (payload(zbrar0, 0, nused) = payload(zbrar1, 0, nused) ↔ true) | A User Theorem |
| unmodified-same-payload-subseteq | nused ≤ # zbrar0, # zbrar0 = # zbrar1, # zbrar0 = BRANCH_SIZE ⊦ iast0 ⊆ iast1 ∧ unmodified(adr, mkznode(rp0, zbrar0, bv, false, nused), iast0) ∧ unmodified(adr, mkznode(rp2, zbrar1, bv, false, nused), iast1) → (payload(zbrar0, 0, nused) = payload(zbrar1, 0, nused) ↔ true) | A User Theorem |
| unmodified-save | ⊦ unmodified(adr, mkznode(r0, zbrar, boolvar, false, m0), iast[adr, save(mkznode(r0, zbrar, boolvar, true, m0))]) | A User Theorem |
| unmodified-sorted-leaf | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ nused ≤ BRANCH_SIZE ∧ BRANCH_SIZE = # zbrar ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused), iast) → (sorted(load(brar, 0, nused), 0, nused) ↔ sorted(zbrar, 0, nused)) | A User Theorem |
| unmodified-sorted-node | ⊦ iast[adr] = indexnode(brar, bv0, m) ∧ nused < BRANCH_SIZE ∧ BRANCH_SIZE = # zbrar ∧ unmodified(adr, mkznode(rp, zbrar, bv1, false, nused + 1), iast) → (sorted(load(brar, 0, nused + 1), 0, nused) ↔ sorted(zbrar, 0, nused)) | A User Theorem |
| unmodified-write-dirty | ⊦ unmodified(adr0, mkznode(rp0, zbrar, boolvar, true, height), iast[adr, ind]) ↔ unmodified(adr0, mkznode(rp0, zbrar, boolvar, true, height), iast) | A User Theorem |
| unmodified-write-other | adr ≠ adr0 ⊦ unmodified(adr0, znd, iast[adr, ind]) ↔ unmodified(adr0, znd, iast) | A User Theorem |