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: |
|---|---|---|
| elems | ⊦ ar .elems = ar elems # ar | An Axiom |
| elems-base | ⊦ ar elems 0 = ∅ | An Axiom |
| elems-rec | n < # ar ⊦ ar elems (n + 1) = (ar elems n) ++ ar[n] | An Axiom |
| ar-elems-append | ⊦ (ar0 + ar1) .elems = ar0 .elems ∪ ar1 .elems | A User Theorem |
| ar-elems-append-lower-h | ⊦ n ≤ # ar0 → (ar0 + ar1) elems n = ar0 elems n | A User Theorem |
| ar-elems-append-not-lower-h | ⊦ n > # ar0 ∧ n ≤ # ar0 + # ar1 → (ar0 + ar1) elems n = (ar0 elems # ar0) ∪ (ar1 elems (n - # ar0)) | A User Theorem |
| ar-elems-extract1 | ⊦ n < # ar → ar .elems = (subarray(ar, 0, n) .elems ∪ subarray(ar, n + 1, # ar - n - 1) .elems) ++ ar[n] | A User Theorem |
| ar-elems-id-size | ⊦ ar0 .elems = ar1 .elems → # ar0 = # ar1 | A User Theorem |
| ar-elems-id-size1 | ⊦ ar0 .elems = ar1 .elems → (# ar0 < # ar1 ↔ false) | A User Theorem |
| ar-elems-in | ⊦ n < # ar → (¬ ar[n] ∈ ar .elems ↔ false) | A User Theorem |
| ar-elems-in-exists | ⊦ a ∈ ar .elems → (∃ n. n < # ar ∧ ar[n] = a) | A User Theorem |
| ar-elems-in-exists-h | ⊦ n ≤ # ar ∧ a ∈ ar elems n → (∃ n0. n0 < n ∧ ar[n0] = a) | A User Theorem |
| ar-elems-in-h | ⊦ n < n0 ∧ n0 ≤ # ar → (¬ ar[n] ∈ ar elems n0 ↔ false) | A User Theorem |
| ar-elems-size | ⊦ # ar .elems = # ar | A User Theorem |
| ar-elems-size-h | ⊦ n ≤ # ar → # (ar elems n) = n | A User Theorem |
| ar-elems-update | ⊦ n < # ar → ar[n, a] .elems = (ar .elems -- ar[n]) ++ a | A User Theorem |
| ar-elems-update-h | ⊦ n < n0 ∧ n0 ≤ # ar → ar[n, a] elems n0 = ((ar elems n0) -- ar[n]) ++ a | A User Theorem |
| ar-elems-update-h0 | ⊦ n < # ar ∧ n0 ≤ n → ar[n, a] elems n0 = ar elems n0 | A User Theorem |
| ar-elems1 | ⊦ # ar = 1 → ar .elems = ∅ ++ ar[0] | A User Theorem |