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: |
|---|---|---|
| splice-copy | ⊦ n1 + m ≤ # ar1 ∧ m ≠ 0 → splice(ar0, n0, ar1, n1, m) = copy(ar0, n0, ar1, n1, m) | An Axiom |
| zarray-len | ⊦ # mkzarray(n) = n | An Axiom |
| zarray-at | ⊦ m < n → mkzarray(n)[m] = zero | An Axiom |
| resize-at | ⊦ m < n → resize(ar, n)[m] = (# ar ≤ m ∧ m < n ⊃ zero;ar[m]) | An Axiom |
| resize-len | ⊦ # resize(ar, n) = n | An Axiom |
| splice-resize | ⊦ # ar1 < n1 + m ∧ m ≠ 0 → splice(ar0, n0, ar1, n1, m) = copy(ar0, n0, resize(ar1, n1 + m), n1, m) | An Axiom |
| splice-0 | ⊦ splice(ar0, n0, ar1, n1, 0) = ar1 | An Axiom |
| range-eq-rec | ⊦ range=(ar0, n0, ar1, n1, m + 1) ↔ ar0[n0] = ar1[n1] ∧ range=(ar0, n0 + 1, ar1, n1 + 1, m) | An Axiom |
| range-eq-0 | ⊦ range=(ar0, n0, ar1, n1, 0) ↔ n0 ≤ # ar0 ∧ n1 ≤ # ar1 | An Axiom |
| append | ⊦ ar0 + ar1 = copy(ar1, 0, resize(ar0, # ar0 + # ar1), # ar0, # ar1) | An Axiom |
| emparray-at | ⊦ m < n → mkemparray(n)[m] = empty | An Axiom |
| emparray-len | ⊦ # mkemparray(n) = n | An Axiom |
| append-a | ⊦ (ar + ar0) + ar1 = ar + ar0 + ar1 | A User Theorem |
| append-at | ⊦ n < # ar0 + # ar1 → (ar0 + ar1)[n] = (n < # ar0 ⊃ ar0[n];ar1[n - # ar0]) | A User Theorem |
| append-at1 | ⊦ n < # ar0 → (ar0 + ar1)[n] = ar0[n] | A User Theorem |
| append-at2 | ⊦ # ar0 ≤ n ∧ n < # ar0 + # ar1 → (ar0 + ar1)[n] = ar1[n - # ar0] | A User Theorem |
| append-atp2 | ⊦ n < # ar1 → (ar0 + ar1)[# ar0 + n] = ar1[n] | A User Theorem |
| append-eq-emptyar | ⊦ ar0 + ar1 = mkarray(0) ↔ ar0 = mkarray(0) ∧ ar1 = mkarray(0) | A User Theorem |
| append-eq-left | ⊦ ar + ar0 = ar + ar1 ↔ ar0 = ar1 | A User Theorem |
| append-eq-right | ⊦ ar0 + ar = ar1 + ar ↔ ar0 = ar1 | A User Theorem |
| append-inj | ⊦ # ar0 = # ar1 → (ar0 + ar = ar1 + ar2 ↔ ar0 = ar1 ∧ ar = ar2) | A User Theorem |
| append-left-size0 | ⊦ # ar0 = 0 → ar0 + ar1 = ar1 | A User Theorem |
| append-len | ⊦ #(ar0 + ar1) = # ar0 + # ar1 | A User Theorem |
| append-prefix-left | ⊦ ar0 + ar1 = ar0 ↔ # ar1 = 0 | A User Theorem |
| append-right-size0 | ⊦ # ar1 = 0 → ar0 + ar1 = ar0 | A User Theorem |
| append-zero-left | ⊦ mkarray(0) + ar = ar | A User Theorem |
| append-zero-right | ⊦ ar + mkarray(0) = ar | A User Theorem |
| copy-append | # ar0 ≤ n, n + m1 ≤ # ar0 + # ar1 ⊦ copy(ar0 + ar1, n, ar2, m0, m1) = copy(ar1, n - # ar0, ar2, m0, m1) | A User Theorem |
| copy-exact-append | ⊦ # ar0 = # ar → copy(ar0 + ar1, 0, ar, 0, # ar0) = ar0 | A User Theorem |
| copy-shift-append | ⊦ m ≤ # ar1 → copy(ar0 + ar1, # ar0, ar, n, m) = copy(ar1, 0, ar, n, m) | A User Theorem |
| copy2append | ⊦ n0 + m ≤ # ar0 ∧ n1 + m ≤ # ar1 → copy(ar0, n0, ar1, n1, m) = subarray(ar1, 0, n1) + subarray(ar0, n0, m) + subarray(ar1, n1 + m, # ar1 - n1 - m) | A User Theorem |
| copy2append0 | ⊦ n1 ≤ # ar0 ∧ n0 + n1 ≤ # ar1 → copy(ar0, 0, ar1, n0, n1) = subarray(ar1, 0, n0) + subarray(ar0, 0, n1) + subarray(ar1, n0 + n1, # ar1 - n0 - n1) | A User Theorem |
| copy2append00 | ⊦ n ≤ # ar0 ∧ n ≤ # ar1 → copy(ar1, 0, ar0, 0, n) = subarray(ar1, 0, n) + subarray(ar0, n, # ar0 - n) | A User Theorem |
| fill2append | ⊦ n0 + n1 ≤ # ar → fill(ar, a, n0, n1) = subarray(ar, 0, n0) + fill(mkarray(n1), a) + subarray(ar, n0 + n1, # ar - n0 + n1) | A User Theorem |
| mkemparray-append | ⊦ mkemparray(n0) + mkemparray(n1) = mkemparray(n0 + n1) | A User Theorem |
| mkemparray-eq | ⊦ mkemparray(n) = mkemparray(m) ↔ n = m | A User Theorem |
| mkemparray0-append-left | ⊦ mkemparray(0) + ar = ar | A User Theorem |
| mkemparray0-append-right | ⊦ ar + mkemparray(0) = ar | A User Theorem |
| range-copy-drop | n0 + m0 ≤ n1 ∨ n1 + m1 ≤ n0, n + m0 ≤ # ar, n0 + m0 ≤ # ar0 ⊦ range=(ar2, n2, copy(ar, n, ar0, n0, m0), n1, m1) ↔ range=(ar2, n2, ar0, n1, m1) | A User Theorem |
| range-copy-inner | n1 ≤ n0, n0 + m0 ≤ n1 + m1, n + m0 ≤ # ar, n0 + m0 ≤ # ar0 ⊦ range=(ar2, n2, copy(ar, n, ar0, n0, m0), n1, m1) ↔ range=(ar2, n2, ar0, n1, n0 - n1) ∧ range=(ar2, n2 + n0 - n1, ar, n, m0) ∧ range=(ar2, n2 + n0 + m0 - n1, ar0, n0 + m0, m1 + n1 - m0 - n0) | A User Theorem |
| range-copy-lower | n0 ≤ n1, n1 ≤ n0 + m0, n0 + m0 ≤ n1 + m1, n + m0 ≤ # ar, n0 + m0 ≤ # ar0 ⊦ range=(ar2, n2, copy(ar, n, ar0, n0, m0), n1, m1) ↔ range=(ar2, n2, ar, n + (n1 - n0), m0 + n0 - n1) ∧ range=(ar2, n2 + n0 + m0 - n1, ar0, n0 + m0, m1 + n1 - m0 + n0) | A User Theorem |
| range-copy-outer | n0 ≤ n1, n1 + m1 ≤ n0 + m0, n + m0 ≤ # ar, n0 + m0 ≤ # ar0 ⊦ range=(ar2, n2, copy(ar, n, ar0, n0, m0), n1, m1) ↔ range=(ar2, n2, ar, n + (n1 - n0), m1) | A User Theorem |
| range-copy-upper | n1 ≤ n0, n0 ≤ n1 + m1, n1 + m1 ≤ n0 + m0, n + m0 ≤ # ar, n0 + m0 ≤ # ar0 ⊦ range=(ar2, n2, copy(ar, n, ar0, n0, m0), n1, m1) ↔ range=(ar2, n2, ar0, n1, n0 - n1) ∧ range=(ar2, n2 + n0 - n1, ar, n, m1 + n1 - n0) | A User Theorem |
| range-eq-append | ⊦ range=(ar0, n0, ar1, n1, m0 + m1) ↔ range=(ar0, n0, ar1, n1, m0) ∧ range=(ar0, n0 + m0, ar1, n1 + m0, m1) | A User Theorem |
| range-eq-bounds | ⊦ range=(ar0, n0, ar1, n1, m) → n0 + m ≤ # ar0 ∧ n1 + m ≤ # ar1 | A User Theorem |
| range-eq-cut | ⊦ n1 + m ≤ # ar1 → (range=(ar0, n0, ar1, n1, m) ↔ range=(ar0, n0, resize(ar1, n1 + m), n1, m)) | A User Theorem |
| range-eq-ext | ⊦ range=(ar0, n0, ar1, n1, m) ↔ n0 + m ≤ # ar0 ∧ n1 + m ≤ # ar1 ∧ (∀ n. n < m → ar0[n0 + n] = ar1[n1 + n]) | A User Theorem |
| range-eq-refl | ⊦ range=(ar, n, ar, n, m) ↔ n + m ≤ # ar | A User Theorem |
| range-eq-resize | ⊦ n ≤ # ar1 → (range=(ar0, n0, resize(ar1, n), n1, m) ↔ ¬ ¬ range=(ar0, n0, ar1, n1, m) ∧ m + n1 ≤ n) | A User Theorem |
| range-eq-splice-less | ⊦ m1 ≤ m0 ∧ n + m0 ≤ # ar ∧ # ar0 < n0 + m1 ∧ m1 ≠ 0 ∧ n1 ≤ n0 → (range=(ar2, n2, splice(ar, n, ar0, n0, m0), n1, m1) ↔ range=(ar2, n2, splice(ar, n, ar0, n0, m1), n1, m1)) | A User Theorem |
| range-eq-subarrays | ⊦ range=(ar0, n0, ar1, n1, m) ↔ n0 + m ≤ # ar0 ∧ n1 + m ≤ # ar1 ∧ subarray(ar0, n0, m) = subarray(ar1, n1, m) | A User Theorem |
| range-eq-sym | ⊦ range=(ar0, n0, ar1, n1, m) ↔ range=(ar1, n1, ar0, n0, m) | A User Theorem |
| range-eq-trans | ⊦ range=(ar0, n0, ar1, n1, m) ∧ range=(ar1, n1, ar2, n2, m) → (¬ range=(ar0, n0, ar2, n2, m) ↔ false) | A User Theorem |
| range-extend | n + m1 ≤ # ar, n0 + m0 + m1 ≤ # ar0 ⊦ range=(copy(ar, n, ar0, n0 + m0, m1), n0, ar1, n1, m0 + m1) ↔ range=(ar0, n0, ar1, n1, m0) ∧ range=(ar, n, ar1, n1 + m0, m1) | A User Theorem |
| resize-exact | ⊦ resize(ar, # ar) = ar | A User Theorem |
| resize-exact-n | ⊦ n = # ar → resize(ar, n) = ar | A User Theorem |
| resize-twice | ⊦ # ar ≤ n → resize(resize(ar, n), m) = resize(ar, m) | A User Theorem |
| same-size-append | ⊦ ar0 = ar1 + ar2 → (# ar0 = # ar1 ↔ ar2 = mkarray(0)) | A User Theorem |
| splice-len | ⊦ m ≠ 0 → # splice(ar0, n0, ar1, n1, m) = max(# ar1, n1 + m) | A User Theorem |
| splice-resize-less | ⊦ n1 ≤ m1 ∧ m0 ≠ 0 → resize(splice(ar0, n0, ar1, n1, m0), m1) = resize(splice(ar0, n0, ar1, n1, min(m0, m1 - n1)), m1) | A User Theorem |
| subarray-append-consec | ⊦ m0 + n0 + n1 ≤ # ar → subarray(ar, m0, n0) + subarray(ar, n0 + m0, n1) = subarray(ar, m0, n0 + n1) | A User Theorem |
| subarray-append-consec0 | ⊦ n0 + n1 ≤ # ar → subarray(ar, 0, n0) + subarray(ar, n0, n1) = subarray(ar, 0, n0 + n1) | A User Theorem |
| subarray-append-elim | ⊦ n = # ar0 ∧ m = # ar1 → subarray(ar0 + ar1, n, m) = ar1 | A User Theorem |
| subarray-append-elim-left | ⊦ # ar0 = n0 ∧ n1 + m ≤ # ar1 → subarray(ar0 + ar1, n0 + n1, m) = subarray(ar1, n1, m) | A User Theorem |
| subarray-append-elim-left0 | ⊦ n = # ar0 ∧ m ≤ # ar1 → subarray(ar0 + ar1, n, m) = subarray(ar1, 0, m) | A User Theorem |
| subarray-append-left | n = # ar0 ⊦ subarray(ar0 + ar1, 0, n) = ar0 | A User Theorem |
| subarray-append-left-01 | ⊦ m ≤ # ar0 → subarray(ar0 + ar1, 0, m) = subarray(ar0, 0, m) | A User Theorem |
| subarray-append-shift-right | ⊦ # ar0 ≤ m ∧ m ≤ # ar0 + # ar1 → subarray(ar0 + ar1, 0, m) = ar0 + subarray(ar1, 0, m - # ar0) | A User Theorem |
| subarray-same-ar-eq | ⊦ subarray(ar, n0, n1) ≠ subarray(ar, n0, n2) ↔ n1 ≠ n2 | A User Theorem |
| subarray-split-at | ⊦ n < # ar → ar = subarray(ar, 0, n) + subarray(ar, n, # ar - n) | A User Theorem |
| subarray-split-first | ⊦ n1 ≠ 0 ∧ n0 + n1 ≤ # ar → subarray(ar, n0, n1) = mkarray(1)[0, ar[n0]] + subarray(ar, n0 + 1, n1 - 1) | A User Theorem |