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: |
|---|---|---|
| s2l-empty | ⊦ s→l("") = [] | An Axiom |
| s2l-rec | ⊦ s→l(char ' + str) = char ' + s→l(str) | An Axiom |
| l2s-empty | ⊦ l→s([]) = "" | An Axiom |
| l2s-rec | ⊦ l→s(char ' + chars) = char + l→s(chars) | An Axiom |
| at-eq | ⊦ m < # chars ∧ n < # chars ∧ ¬ dups(chars) → (chars[m] ' = chars[n] ' ↔ m = n) | A User Theorem |
| inject-s2l | ⊦ s→l(str) = s→l(str0) ↔ str = str0 | A User Theorem |
| l2s-app | ⊦ l→s(chars + chars0) = l→s(chars) + l→s(chars0) | A User Theorem |
| l2s-length | ⊦ # l→s(chars) = # chars | A User Theorem |
| l2s-one | ⊦ l→s(char ') = char ' | A User Theorem |
| length-at | ⊦ # chars[m] ' = 1 | A User Theorem |
| pos-at | ⊦ n < # str ∧ ¬ dups(s→l(str)) → pos(s→l(str)[n], str) = n | A User Theorem |
| s2l-app | ⊦ s→l(str + str0) = s→l(str) + s→l(str0) | A User Theorem |
| s2l-empty-01 | ⊦ s→l(str) = [] ↔ str = "" | A User Theorem |
| s2l-length | ⊦ # s→l(str) = # str | A User Theorem |
| s2l-one | ⊦ s→l(char ') = char ' | A User Theorem |
| s2l-rec-01 | str ≠ "" ⊦ s→l((* str)) = str.char1 ' + s→l(str.rstring) | A User Theorem |
| sortedchars-no-dups | ⊦ ¬ dups(s→l(sortedchars)) | A User Theorem |
| string2string | ⊦ l→s(s→l(str)) = str | A User Theorem |