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: |
|---|---|---|
| valid | ⊦ valid(sar, ar) ↔ sar .elems = bag< # ar ∧ (∀ n0, n1. n0 < # sar ∧ n1 < # sar → (suffix(ar, sar[n0]) < suffix(ar, sar[n1]) ↔ n0 < n1)) | An Axiom |
| bagle-rec | ⊦ bag< (n + 1) = bag< n ++ n | An Axiom |
| bagle-base | ⊦ bag< 0 = ∅ | An Axiom |
| bagle-count | ⊦ count(n, bag< m) = ((n < m ⊃ 1; 0)) | A User Theorem |
| bagle-in | ⊦ m ∈ bag< n ↔ m < n | A User Theorem |
| bagle-size | ⊦ # bag< n = n | A User Theorem |
| sar-elems-bagle-ls | ⊦ sar .elems = bag< n ∧ n0 < # sar → sar[n0] < n | A User Theorem |
| sar-elems-bagle-size | ⊦ sar .elems = bag< n → # sar = n | A User Theorem |
| sar-elems-bagle-twice-same | ⊦ sar .elems = bag< # sar ∧ n < # sar ∧ m < # sar → (sar[n] = sar[m] ↔ n = m) | A User Theorem |
| valid-sar-at-le | n < # ar ⊦ valid(sar, ar) → (¬ sar[n] ≤ # ar ↔ false) | A User Theorem |
| valid-sar-at-ls | n < # ar ⊦ valid(sar, ar) → (¬ sar[n] < # ar ↔ false) | A User Theorem |
| valid-sar-index-exists | ⊦ valid(sar, ar) ∧ n < # ar → (∃ n0. n0 < # sar ∧ sar[n0] = n) | A User Theorem |
| valid-sar-size | ⊦ valid(sar, ar) → # sar = # ar | A User Theorem |
| valid-sar-twice-same | ⊦ valid(sar, ar) ∧ n < # ar ∧ m < # ar → (sar[n] = sar[m] ↔ n = m) | A User Theorem |
| valid-sar-twice-same1 | ⊦ valid(sar, ar) ∧ n + 1 < # ar → (sar[n] = sar[n + 1] ↔ false) | A User Theorem |
| valid-suffix-ls | ⊦ valid(sar, ar) ∧ n0 < # sar ∧ n1 < # sar → (¬ suffix(ar, sar[n0]) < suffix(ar, sar[n1]) ↔ ¬ n0 < n1) | A User Theorem |