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: |
|---|---|---|
| in-def | ⊦ char ∈ str ↔ char ∈ s→l(str) | An Axiom |
| last-def | ⊦ str.last = s→l(str).last | An Axiom |
| butlast-def | ⊦ str.butlast = l→s(s→l(str).butlast) | An Axiom |
| left-trim-empty | ⊦ string-left-trim(str1, "") = "" | An Axiom |
| left-trim-done | ⊦ ¬ str2.char1 ∈ str1 ∧ str2 ≠ "" → string-left-trim(str1, str2) = str2 | An Axiom |
| left-trim-rec | ⊦ str2.char1 ∈ str1 ∧ str2 ≠ "" → string-left-trim(str1, str2) = string-left-trim(str1, str2.rstring) | An Axiom |
| right-trim-empty | ⊦ string-right-trim(str1, "") = "" | An Axiom |
| right-trim-done | ⊦ ¬ str2.last ∈ str1 ∧ str2 ≠ "" → string-right-trim(str1, str2) = str2 | An Axiom |
| right-trim-rec | ⊦ str2.last ∈ str1 ∧ str2 ≠ "" → string-right-trim(str1, str2) = string-right-trim(str1, str2.butlast) | An Axiom |
| trim-number | ⊦ trim-number(str) = string-right-trim("0123456789", str) | An Axiom |
| prefix-def | ⊦ str ⊑ str0 ↔ s→l(str) ⊑ s→l(str0) | An Axiom |
| String-upcaseFirst-def | ⊦ upcaseFirst(char + str) = upcase(char) + str | An Axiom |
| String-upcaseFirst-empty | ⊦ upcaseFirst("") = "" | An Axiom |
| String-downcaseFirst-def | ⊦ downcaseFirst(char + str) = downcase(char) + str | An Axiom |
| String-downcaseFirst-empty | ⊦ downcaseFirst("") = "" | An Axiom |
| Char-upcase-no | ⊦ ¬(pos('a', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('z', sortedchars)) → upcase(char) = char | An Axiom |
| Char-upcase-yes | ⊦ pos('a', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('z', sortedchars) → upcase(char) = s→l(sortedchars)[pos(char, sortedchars) - (pos('a', sortedchars) - pos('A', sortedchars))] | An Axiom |
| Char-downcase-no | ⊦ ¬(pos('A', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('Z', sortedchars)) → downcase(char) = char | An Axiom |
| Char-downcase-yes | ⊦ pos('A', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('Z', sortedchars) → downcase(char) = s→l(sortedchars)[pos(char, sortedchars) + (pos('a', sortedchars) - pos('A', sortedchars))] | An Axiom |
| String-upcase-rec | ⊦ upcase(char + str) = upcase(char) + upcase(str) | An Axiom |
| String-upcase-empty | ⊦ upcase("") = "" | An Axiom |
| String-downcase-rec | ⊦ downcase(char + str) = downcase(char) + downcase(str) | An Axiom |
| String-downcase-empty | ⊦ downcase("") = "" | An Axiom |
| substring-def | ⊦ substring(str, m, n) = l→s(sublist(m, n, s→l(str))) | An Axiom |
| butlast-app | ⊦ str1 ≠ "" → (str0 + str1).butlast = str0 + str1.butlast | A User Theorem |
| butlast-in | ⊦ ¬ char ∈ str ∧ str ≠ "" → ¬ char ∈ str.butlast | A User Theorem |
| butlast-length | ⊦ str ≠ "" → # str.butlast = # str - 1 | A User Theorem |
| char-in | ⊦ char ∈ l→s(chars) ↔ char ∈ chars | A User Theorem |
| char-in-01 | ⊦ char ∈ s→l(str) ↔ char ∈ str | A User Theorem |
| char-in-app | ⊦ char ∈ str + str0 ↔ char ∈ str ∨ char ∈ str0 | A User Theorem |
| char-in-empty | ⊦ ¬ char ∈ "" | A User Theorem |
| char-in-one | ⊦ char ∈ char0 ' ↔ char = char0 | A User Theorem |
| char-in-rec | ⊦ char ∈ char0 ' + str ↔ char = char0 ∨ char ∈ str | A User Theorem |
| downcase-A | ⊦ downcase('A') = 'a' | A User Theorem |
| downcase-B | ⊦ downcase('B') = 'b' | A User Theorem |
| downcase-C | ⊦ downcase('C') = 'c' | A User Theorem |
| downcase-lower-a | ⊦ downcase('a') = 'a' | A User Theorem |
| downcase-rec | ⊦ str ≠ "" → downcase(str) = downcase(str.char1) + downcase(str.rstring) | A User Theorem |
| last-app | ⊦ str1 ≠ "" → (str0 + str1).last = str1.last | A User Theorem |
| last-in | ⊦ str ≠ "" → str.last ∈ str | A User Theorem |
| natstring-chars | ⊦ ¬ char ∈ "0123456789" → ¬ char ∈ n→s(m) | A User Theorem |
| prefix-empty | ⊦ "" ⊑ str | A User Theorem |
| prefix-empty-01 | ⊦ str ⊑ "" ↔ str = "" | A User Theorem |
| prefix-num | str.char1 = str0.char1, str ≠ "", str0 ≠ "" ⊦ (* str) ⊑ (* str0) ↔ str.rstring ⊑ str0.rstring | A User Theorem |
| prefix-num-01 | str.char1 ≠ str0.char1, str ≠ "", str0 ≠ "" ⊦ ¬ (* str) ⊑ (* str0) | A User Theorem |
| prefix-reflexive | ⊦ str ⊑ str | A User Theorem |
| right-trim-app | ∀ char. char ∈ str1 → char ∈ str ⊦ string-right-trim(str, str0 + str1) = string-right-trim(str, str0) | A User Theorem |
| right-trim-trim | ⊦ string-right-trim(str, string-right-trim(str, str0)) = string-right-trim(str, str0) | A User Theorem |
| substring-all | ⊦ # str = n → substring(str, 0, n) = str | A User Theorem |
| substring-app-rec | ⊦ # str ≤ m → substring(str + str0, m, n) = substring(str0, m - # str, n) | A User Theorem |
| substring-offset-rec | ⊦ m ≠ 0 ∧ str ≠ "" → substring(str, m, n) = substring(str.rstring, m -1, n) | A User Theorem |
| substring-zero-rec | ⊦ n ≠ 0 ∧ str ≠ "" → substring(str, 0, n) = str.char1 + substring(str.rstring, 0, n -1) | A User Theorem |
| test-downcaseFirst | ⊦ downcaseFirst("ABCabc012") = "aBCabc012" | A User Theorem |
| trim-number-01 | ⊦ trim-number(str + n→s(m)) = trim-number(str) | A User Theorem |
| trim-number-02 | ⊦ trim-number(trim-number(str)) = trim-number(str) | A User Theorem |
| upcase-a | ⊦ upcase('a') = 'A' | A User Theorem |