[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
string-append
,
nat
with
constants sortedchars : string;
comment: String containing all characters, used for < on chars/strings.;
functions # . : string → nat;
comment: length of string;
pos : char × string → nat;
comment: first occurence of char in string, 0 based (0 is also returned if no occurrence).;
predicates . < . : string × string;
comment: standard lexicographical order based on ASCII (char <).;
. < . : char × char;
comment: ASCII ordering of characters.;
variables char3 : char;
axioms Length-empty : ⊦ # "" = 0;
used for: s, ls;
Length-rec : ⊦ #(char ' + str) = # str + 1;
used for: s, ls;
Pos-empty : ⊦ pos(char, "") = 0;
used for: s, ls;
Pos-found : ⊦ pos(char, char ' + str) = 0;
used for: s, ls;
Pos-rec : ⊦ char1 ≠ char2 → pos(char1, char2 ' + str) = pos(char1, str) + 1;
used for: s, ls, lc;
Irreflexivity : ⊦ ¬ str < str;
used for: s, ls;
comment: needed for acutalizations;
Transitivity : ⊦ str1 < str2 ∧ str2 < str3 → str1 < str3;
used for: f, lf;
comment: needed for acutalizations;
Totality : ⊦ str1 < str2 ∨ str1 = str2 ∨ str2 < str1;
comment: needed for acutalizations;
Less-empty : ⊦ "" < char ' + str;
used for: s, ls;
Less-notempty : ⊦ ¬ str < "";
used for: s, ls;
Less-rec : ⊦ char1 ' + str1 < char2 ' + str2 ↔ char1 < char2 ∨ char1 = char2 ∧ str1 < str2;
used for: s, ls;
Char-irref : ⊦ ¬ char < char;
used for: s, ls;
comment: needed for acutalizations;
Char-trans : ⊦ char1 < char2 ∧ char2 < char3 → char1 < char3;
used for: f, lf;
comment: needed for acutalizations;
Char-total : ⊦ char1 < char2 ∨ char1 = char2 ∨ char2 < char1;
comment: needed for acutalizations;
Char-less : ⊦ char1 < char2 ↔ pos(char1, sortedchars) < pos(char2, sortedchars);
Sortedchars : ⊦ sortedchars = " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~";
comment: It is important that the characters are in ASCII order
because of predefined numeral function string<.
The position is also used for upcase and downcase.
9 is ascii 57, : is 58, semicolon is 59 (missing), < is 60.
A is 65, a is 97. Some missing chars: Space 32, backslash 92, semicolon 59,
all quotes 34, 39, 96.
;
end enrich