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: |
|---|---|---|
| suffix | n ≤ # ar ⊦ suffix(ar, n) = subarray(ar, n, # ar - n) | An Axiom |
| lexicographic | ⊦ ar0 < ar1 ↔ (∃ n. n ≤ # ar0 ∧ n ≤ # ar1 ∧ subarray(ar0, 0, n) = subarray(ar1, 0, n) ∧ (# ar0 = n → # ar1 > n) ∧ (# ar0 ≠ n → # ar1 ≠ n ∧ ar0[n] < ar1[n])) | An Axiom |
| array-exists-first-neq | ⊦ ∃ n. n ≤ # ar0 ∧ n ≤ # ar1 ∧ subarray(ar0, 0, n) = subarray(ar1, 0, n) ∧ (n ≠ # ar0 ∧ n ≠ # ar1 → ar0[n] ≠ ar1[n]) | A User Theorem |
| lexicographic-emparray | ⊦ ar < mkarray(0) ↔ false | A User Theorem |
| lexicographic-irrefl | ⊦ ¬ ar < ar | A User Theorem |
| lexicographic-suffix-next | ⊦ n0 < # ar ∧ n1 < # ar → (suffix(ar, n0) < suffix(ar, n1) ↔ ar[n0] < ar[n1] ∨ suffix(ar, n0 + 1) < suffix(ar, n1 + 1) ∧ ar[n0] = ar[n1]) | A User Theorem |
| lexicographic-total | ⊦ ¬ ar0 < ar1 ∧ ¬ ar1 < ar0 → ar0 = ar1 | A User Theorem |
| lexicographic-trans | ⊦ ar0 < ar1 ∧ ar1 < ar2 → ar0 < ar2 | A User Theorem |
| ls-at-subarray | n < m1, m0 + m1 ≤ # ar ⊦ (subarray(ar, m0, m1)[n]) = ar[m0 + n] | A User Theorem |
| suffix-end | ⊦ suffix(ar, # ar) = mkarray(0) | A User Theorem |
| suffix-same | n0 ≤ # ar, n1 ≤ # ar ⊦ suffix(ar, n0) = suffix(ar, n1) ↔ n0 = n1 | A User Theorem |