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: |
|---|---|---|
| decl | An Axiom | |
| correctness-create_suffixarray | ⊦ ⟪create_suffixarray#(ar; sar)⟫ valid(sar, ar) | A User Theorem |