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: |
|---|---|---|
| Fill-zero | ⊦ fill(ar, a, m, 0) = ar | An Axiom |
| Fill-succ | ⊦ fill(ar, a, m, n + 1) = fill(ar, a, m, n)[m + n, a] | An Axiom |
| Fill-all | ⊦ fill(ar, a) = fill(ar, a, 0, # ar) | An Axiom |
| Copy-zero | ⊦ copy(ar, m, ar0, m0, 0) = ar0 | An Axiom |
| Copy-succ | ⊦ copy(ar, m, ar0, m0, n + 1) = copy(ar, m, ar0, m0, n)[m0 + n, ar[m + n]] | An Axiom |
| Subarray | ⊦ subarray(ar, m, n) = copy(ar, m, mkarray(n), 0, n) | An Axiom |
| Compare | ⊦ cmp(ar, m, ar0, m0, n) ↔ (∀ n0. n0 < n → ar[m + n0] = ar0[m0 + n0]) | An Axiom |
| Cmp-elem | ⊦ cmp(ar, a, m, n) ↔ (∀ n0. n0 < n → ar[m + n0] = a) | An Axiom |
| Idrange | ⊦ idrange(ar, m, n) ↔ (∀ n0. n0 < n → ar[m + n0] = ar[m]) | An Axiom |
| in | ⊦ a ∈ ar ↔ (∃ n. n < # ar ∧ ar[n] = a) | An Axiom |
| Idexcept | ⊦ id○(ar0, ar1, n) ↔ ¬ ¬(# ar0 = # ar1 ∧ (∀ m. m < # ar0 ∧ m ≠ n → ar0[m] = ar1[m])) | An Axiom |
| rev | ⊦ rev(ar) = rev(ar, # ar) | An Axiom |
| rev-rec | ⊦ n < # ar → rev(ar, n + 1) = rev(ar, n)[n, ar[# ar - n + 1]] | An Axiom |
| rev-base | ⊦ rev(ar, 0) = mkarray(# ar) | An Axiom |
| at-copy | ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0]) | A User Theorem |
| at-fill | ⊦ n < # ar → fill(ar, a)[n] = a | A User Theorem |
| at-fill-h | ⊦ n < # ar → fill(ar, a, m0, m1)[n] = (m0 ≤ n ∧ n < m0 + m1 ⊃ a;ar[n]) | A User Theorem |
| at-fill-h0 | ⊦ n < m ∧ n < # ar → fill(ar, a, 0, m)[n] = a | A User Theorem |
| at-fill-mkarray | ⊦ m < n → fill(mkarray(n), a)[m] = a | A User Theorem |
| at-fill-other | ⊦ n ≥ m ∧ n < # ar → fill(ar, a, 0, m)[n] = ar[n] | A User Theorem |
| at-subarray | ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0] | A User Theorem |
| copy-append | ⊦ copy(ar0, n + m1, copy(ar0, n, ar1, n1, m1), n1 + m1, m0) = copy(ar0, n, ar1, n1, m0 + m1) | A User Theorem |
| copy-coalesce | ⊦ m1 = # ar1 ∧ m0 ≤ m1 ∧ m0 + n ≤ # ar1 → copy(copy(ar0, n0, ar1, 0, m1), n, ar2, n2, m0) = copy(ar0, n0 + n, ar2, n2, m0) | A User Theorem |
| copy-exact | # ar0 = m, # ar1 = m ⊦ copy(ar0, 0, ar1, 0, m) = ar0 | A User Theorem |
| copy-is-subarray | # ar1 = n2 ⊦ copy(ar0, n0, ar1, 0, n2) = subarray(ar0, n0, n2) | A User Theorem |
| copy-other | ⊦ m0 + n0 ≤ m ∧ m + n ≤ # ar ∧ n ≤ # ar0 → copy(copy(ar0, 0, ar, m, n), m0, mkarray(n0), 0, n0) = copy(ar, m0, mkarray(n0), 0, n0) | A User Theorem |
| copy-other-weak | m0 + n0 ≤ m, m + n ≤ # ar, n0 ≤ # ar1, n ≤ # ar0 ⊦ copy(copy(ar0, 0, ar, m, n), m0, ar1, 0, n0) = copy(ar, m0, ar1, 0, n0) | A User Theorem |
| copy-rec | ⊦ copy(ar, m, ar0, m0, n + 1) = copy(ar, m + 1, ar0, m0 + 1, n)[m0, ar[m]] | A User Theorem |
| copy-self | ⊦ n < # ar → copy(ar, 0, ar, 0, n) = ar | A User Theorem |
| copy-subarray1-elim | n0 + n1 ≤ # ar0, m + m1 ≤ n1 ⊦ copy(subarray(ar0, n0, n1), m, ar1, m0, m1) = copy(ar0, n0 + m, ar1, m0, m1) | A User Theorem |
| copy-subarray2 | # ar1 ≥ m0 + m1 ⊦ copy(ar0, n0, subarray(ar1, m0, m1), n1, n2) = subarray(copy(ar0, n0, ar1, m0 + n1, n2), m0, m1) | A User Theorem |
| idexcept-comm | ⊦ id○(ar0, ar1, n) ↔ id○(ar1, ar0, n) | A User Theorem |
| idexcept-comm-simp | ⊦ id○(ar0, ar1, n) → (¬ id○(ar1, ar0, n) ↔ false) | A User Theorem |
| idexcept-extract-left | ⊦ ar0[n] = a → (id○(ar0, ar1, n) ↔ ar0 = ar1[n, a]) | A User Theorem |
| idexcept-extract-right | ⊦ ar1[n] = a → (id○(ar0, ar1, n) ↔ ar1 = ar0[n, a]) | A User Theorem |
| idexcept-refl | ⊦ ¬ id○(ar, ar, n) ↔ false | A User Theorem |
| idexcept-same | ⊦ a = ar0[n] ∧ a = ar1[n] → (id○(ar0, ar1, n) ↔ ar0 = ar1) | A User Theorem |
| idexcept-size | ⊦ id○(ar0, ar1, n) → # ar0 = # ar1 | A User Theorem |
| idexcept-trans | ⊦ id○(ar0, ar1, n) ∧ id○(ar1, ar2, n) → (¬ id○(ar0, ar2, n) ↔ false) | A User Theorem |
| idexcept-write-at | ⊦ ¬ id○(ar[n, a], ar, n) ↔ false | A User Theorem |
| idexcept-write-at-right | ⊦ ¬ id○(ar, ar[n, a], n) ↔ false | A User Theorem |
| idexcept-write-at0 | ⊦ id○(ar0[n, a], ar1, n) ↔ id○(ar0, ar1, n) | A User Theorem |
| idexcept-write-at0-right | ⊦ id○(ar0, ar1[n, a], n) ↔ id○(ar0, ar1, n) | A User Theorem |
| in-at | ⊦ n < # ar ∧ ar[n] = a → (¬ a ∈ ar ↔ false) | A User Theorem |
| rev-at | ⊦ n < # ar → rev(ar)[n] = ar[# ar - n + 1] | A User Theorem |
| rev-at-h | ⊦ m < n ∧ n ≤ # ar → rev(ar, n)[m] = ar[# ar - m + 1] | A User Theorem |
| rev-rev | ⊦ rev(rev(ar)) = ar | A User Theorem |
| rev-size | ⊦ # rev(ar) = # ar | A User Theorem |
| rev-size-h | ⊦ n ≤ # ar → # rev(ar, n) = # ar | A User Theorem |
| size-copy | ⊦ # copy(ar, m, ar0, m0, n) = # ar0 | A User Theorem |
| size-fill | ⊦ # fill(ar, a) = # ar | A User Theorem |
| size-fill-h | ⊦ # fill(ar, a, m, n) = # ar | A User Theorem |
| size-subarray | ⊦ # subarray(ar, m, n) = n | A User Theorem |
| subarray-at | ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0] | A User Theorem |
| subarray-copy | n1 ≥ m0, m0 + m1 ≤ # ar1 ⊦ subarray(copy(ar0, n0, ar1, n1, n2), m0, m1) = copy(ar0, n0, subarray(ar1, m0, m1), n1 - m0, n2) | A User Theorem |
| subarray-copy-elim | m1 + n ≤ # ar1 ⊦ n1 ≤ n → subarray(copy(ar0, m0, ar1, m1, n), m1, n1) = subarray(ar0, m0, n1) | A User Theorem |
| subarray-copy-elim-exact | m1 + n ≤ # ar1 ⊦ subarray(copy(ar0, m0, ar1, m1, n), m1, n) = subarray(ar0, m0, n) | A User Theorem |
| subarray-copy-higher | m0 + m1 ≤ n1, m0 + m1 ≤ # ar ⊦ subarray(copy(ar0, n0, ar, n1, n2), m0, m1) = subarray(ar, m0, m1) | A User Theorem |
| subarray-copy-lower | n1 + n2 ≤ m0, m0 + m1 ≤ # ar ⊦ subarray(copy(ar0, n0, ar, n1, n2), m0, m1) = subarray(ar, m0, m1) | A User Theorem |
| subarray-elim | # ar = n ⊦ subarray(ar, 0, n) = ar | A User Theorem |
| subarray-elim-simp | ⊦ subarray(ar, 0, # ar) = ar | A User Theorem |
| subarray-subarray-elim | ⊦ n0 + n1 ≤ # ar0 ∧ m0 + m1 ≤ n1 → subarray(subarray(ar0, n0, n1), m0, m1) = subarray(ar0, n0 + m0, m1) | A User Theorem |
| subarray-up-same | ⊦ n < # ar → subarray(ar[n, a], 0, n) = subarray(ar, 0, n) | A User Theorem |
| subarray-write-below | n < n0 ⊦ subarray(ar[n, a], n0, n1) = subarray(ar, n0, n1) | A User Theorem |
| subarray-zero | ⊦ subarray(ar, n, 0) = mkarray(0) | A User Theorem |