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: |
|---|---|---|
| Irreflexivity | ⊦ ¬ str < str | An Axiom |
| Transitivity | ⊦ str1 < str2 ∧ str2 < str3 → str1 < str3 | An Axiom |
| Totality | ⊦ str1 < str2 ∨ str1 = str2 ∨ str2 < str1 | An Axiom |
| Less-empty | ⊦ "" < char ' + str | An Axiom |
| Less-notempty | ⊦ ¬ str < "" | An Axiom |
| Less-rec | ⊦ char1 ' + str1 < char2 ' + str2 ↔ char1 < char2 ∨ char1 = char2 ∧ str1 < str2 | An Axiom |
| Char-irref | ⊦ ¬ char < char | An Axiom |
| Char-trans | ⊦ char1 < char2 ∧ char2 < char3 → char1 < char3 | An Axiom |
| Char-total | ⊦ char1 < char2 ∨ char1 = char2 ∨ char2 < char1 | An Axiom |
| Char-less | ⊦ char1 < char2 ↔ pos(char1, sortedchars) < pos(char2, sortedchars) | An Axiom |
| Sortedchars | ⊦ sortedchars = " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~" | An Axiom |
| Length-rec | ⊦ #(char ' + str) = # str + 1 | An Axiom |
| Length-empty | ⊦ # "" = 0 | An Axiom |
| Pos-rec | ⊦ char1 ≠ char2 → pos(char1, char2 ' + str) = pos(char1, str) + 1 | An Axiom |
| Pos-found | ⊦ pos(char, char ' + str) = 0 | An Axiom |
| Pos-empty | ⊦ pos(char, "") = 0 | An Axiom |
| append-eqlen | ⊦ # str = # str1 → (str + str0 = str1 + str2 ↔ str = str1 ∧ str0 = str2) | A User Theorem |
| append-eqlen-01 | ⊦ # str0 = # str2 → (str + str0 = str1 + str2 ↔ str = str1 ∧ str0 = str2) | A User Theorem |
| eq-one | # str = 1, # str0 = 1 ⊦ (* str) = (* str0) + str1 ↔ str = str0 ∧ str1 = "" | A User Theorem |
| eqpos | ⊦ pos(char1, str) < # str → (pos(char1, str) = pos(char2, str) ↔ char1 = char2) | A User Theorem |
| exlarger | ⊦ ∃ str. str0 < str | A User Theorem |
| insorted | ⊦ ¬ pos(char, sortedchars) < # sortedchars ↔ false | A User Theorem |
| len-app | ⊦ #(str + str0) = # str + # str0 | A User Theorem |
| len-str | ⊦ str ≠ "" → # (* str) = # str.rstring + 1 | A User Theorem |
| len-str-01 | str ≠ "" ⊦ # (* str) = # str.rstring + 1 | A User Theorem |
| len-zero | ⊦ # str = 0 ↔ str = "" | A User Theorem |
| length-one | ⊦ # char ' = 1 | A User Theorem |
| less-append | ⊦ str < str + str0 ↔ str0 ≠ "" | A User Theorem |
| less-empty | ⊦ "" < str ↔ str ≠ "" | A User Theorem |
| neq-length | ⊦ # str ≠ # str0 → str ≠ str0 | A User Theorem |
| neq-one | # str = 1, 1 < # str0 ⊦ (* str) ≠ (* str0) + str1 | A User Theorem |
| pos-0 | ⊦ pos(`0`, sortedchars) = 13 | A User Theorem |
| pos-1 | ⊦ pos(`1`, sortedchars) = 14 | A User Theorem |
| pos-2 | ⊦ pos(`2`, sortedchars) = 15 | A User Theorem |
| pos-a | ⊦ pos(`a`, sortedchars) = 59 | A User Theorem |
| pos-b | ⊦ pos(`b`, sortedchars) = 60 | A User Theorem |
| pos-c | ⊦ pos(`c`, sortedchars) = 61 | A User Theorem |
| pos-capital-a | ⊦ pos(`A`, sortedchars) = 29 | A User Theorem |
| pos-capital-b | ⊦ pos(`B`, sortedchars) = 30 | A User Theorem |
| pos-capital-c | ⊦ pos(`C`, sortedchars) = 31 | A User Theorem |
| pos-capital-z | ⊦ pos(`Z`, sortedchars) = 54 | A User Theorem |
| pos-one | ⊦ pos(char, char ') = 0 | A User Theorem |
| pos-range | ⊦ pos(char, str) ≤ # str | A User Theorem |
| pos-str | ⊦ str ≠ "" ∧ char = str.char1 → pos((* char), (* str)) = 0 | A User Theorem |
| pos-str-01 | ⊦ str ≠ "" ∧ char ≠ str.char1 → pos((* char), (* str)) = pos(char, str.rstring) + 1 | A User Theorem |
| pos-str-02 | str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1 | A User Theorem |
| pos-str-03 | str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0 | A User Theorem |
| pos-z | ⊦ pos(`z`, sortedchars) = 84 | A User Theorem |
| sortedchars-divided | ⊦ sortedchars = " !#$%&()*+-" + "./0123456789:<=>?@" + "ABCDEFGHIJKLM" + "NOPQRSTUVWXYZ" + "[]^_abcdefghi" + "jklmnopqrs" + "tuvwxyz|~" | A User Theorem |
| val-irref | ⊦ ¬ str1 < str1 | A User Theorem |
| val-irref-01 | ⊦ ¬ char1 < char1 | A User Theorem |
| val-total | ⊦ str < str2 ∨ str = str2 ∨ str2 < str | A User Theorem |
| val-total-01 | ⊦ char < char2 ∨ char = char2 ∨ char2 < char | A User Theorem |
| val-trans | ⊦ str < str2 ∧ str2 < str3 → str < str3 | A User Theorem |
| val-trans-01 | ⊦ char < char2 ∧ char2 < char3 → char < char3 | A User Theorem |