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: |
|---|---|---|
| issorted-le-all-def | ⊦ issorted(ar) ↔ (∀ m, n. m ≤ n ∧ n < # ar → ¬ ar[n] < ar[m]) | An Axiom |
| isperm-def | ⊦ isperm(ar0, ar1) ↔ perm(arr2list(ar0, # ar0 - 1), arr2list(ar1, # ar1 - 1)) | An Axiom |
| arr2list-rec | ⊦ n + 1 < # ar → arr2list(ar, n + 1) = arr2list(ar, n) + ar[n + 1] ' | An Axiom |
| arr2list-base | ⊦ 0 ≠ # ar → arr2list(ar, 0) = ar[0] ' | An Axiom |
| bool-less | ⊦ bv < bv0 ↔ ¬ ¬ (¬ bv ∧ bv0) | An Axiom |
| arr2list-get | ⊦ m < # ar ∧ n ≤ m → (arr2list(ar, m)[n] ↔ ar[n]) | A User Theorem |
| arr2list-len | ⊦ m < # ar → # arr2list(ar, m) = m + 1 | A User Theorem |
| arr2list-mod-high | ⊦ n < m ∧ m < # ar → arr2list(ar[m, bv], n) = arr2list(ar, n) | A User Theorem |
| arr2list-put | ⊦ m < # ar ∧ n ≤ m → (arr2list(ar, m)[n, bv]) = arr2list(ar[n, bv], m) | A User Theorem |