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: |
|---|---|---|
| sort | An Axiom | |
| inv-outer | ⊦ inv-outer(ar, ar0, n, ⊑) ↔ ¬ ¬ (n ≤ # ar ∧ ar .elems = ar0 .elems ∧ sorted(ar, 0, n, ⊑) ∧ reflexive(⊑) ∧ transitive(⊑) ∧ total(⊑)) | An Axiom |
| inv-inner | ⊦ inv-inner(ar, ar0, n, m, ⊑) ↔ ¬ ¬ ( ar .elems = ar0 .elems ∧ n < # ar ∧ m ≤ n ∧ sorted(ar, 0, m, ⊑) ∧ sorted(ar, m, n + 1, ⊑) ∧ (m ≠ 0 ∧ m < n → ⊑(ar[m - 1], ar[m + 1])) ∧ reflexive(⊑) ∧ transitive(⊑) ∧ total(⊑)) | An Axiom |
| correctness-sort | ar = ar0, transitive(⊑), total(⊑), reflexive(⊑) ⊦ ⟪sort#(⊑; ar)⟫ (ar .elems = ar0 .elems ∧ sorted(ar, ⊑)) | A User Theorem |