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: |
|---|---|---|
| sorted-sub | ⊦ sorted(ar, n0, n1, ⊑) ↔ (∀ n, m. n0 ≤ n ∧ n < m ∧ m < n1 → ⊑(ar[n], ar[m])) | An Axiom |
| sorted-entire | ⊦ sorted(ar, ⊑) ↔ (∀ n, m. n < m ∧ m < # ar → ⊑(ar[n], ar[m])) | An Axiom |
| sorted-0 | ⊦ sorted(ar, n, n, ⊑) | A User Theorem |
| sorted-1 | ⊦ sorted(ar, n, n + 1, ⊑) | A User Theorem |
| sorted-exchange | ⊦ n < # ar ∧ m < n ∧ sorted(ar, m + 1, n + 1, ⊑) ∧ (m + 1 < n → ⊑(ar[m], ar[m + 2])) ∧ ¬ ⊑(ar[m], ar[m + 1]) ∧ total(⊑) ∧ reflexive(⊑) ∧ transitive(⊑) → (¬ sorted(ar[m + 1, ar[m]][m, ar[m + 1]], m, n + 1, ⊑) ↔ false) | A User Theorem |
| sorted-last2 | ⊦ sorted(ar, 0, m + 2, ⊑) → (¬ ⊑(ar[m], ar[m + 1]) ↔ false) | A User Theorem |
| sorted-sub-change-above | n ≥ m1 ⊦ sorted(ar[n, a], m0, m1, ⊑) ↔ sorted(ar, m0, m1, ⊑) | A User Theorem |
| sorted-sub-entire | n = # ar ⊦ sorted(ar, 0, n, ⊑) → (¬ sorted(ar, ⊑) ↔ false) | A User Theorem |
| sorted-sub-less1 | ⊦ sorted(ar, m, n + 1, ⊑) → (¬ sorted(ar, m, n, ⊑) ↔ false) | A User Theorem |
| sorted-sub-merge | ⊦ ⊑(ar[n], ar[n + 1]) ∧ sorted(ar, n + 1, m + 1, ⊑) ∧ sorted(ar, 0, n + 1, ⊑) ∧ transitive(⊑) → (¬ sorted(ar, 0, m + 1, ⊑) ↔ false) | A User Theorem |