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: |
|---|---|---|
| lrs | ⊦ lrs(ar, n0, n1, n) ↔ ¬ ¬ (rs(ar, n0, n1, n) ∧ (∀ m0, m1, m. rs(ar, m0, m1, m) → m ≤ n)) | An Axiom |
| rs | ⊦ rs(ar, n0, n1, n) ↔ ¬ ¬ (n0 ≠ n1 ∧ n0 < # ar ∧ n1 ≤ # ar ∧ lcp(ar, n0, n1) = n) | An Axiom |
| suffix-lcp | ⊦ n0 ≤ # ar ∧ n1 ≤ # ar ∧ n2 ≤ # ar ∧ suffix(ar, n0) < suffix(ar, n1) ∧ suffix(ar, n1) < suffix(ar, n2) → (lcp(ar, n0, n1) < lcp(ar, n0, n2) ↔ false) | A User Theorem |