introduces: string , string of_ , characters_ , " " , _^_ .

includes:  Instant/Distinction ( string for s , _ is _ ) .

needs:     Tuples/Basics, Lists/Flat . character <= item .

 string		= flat-list [character] .
 string of_	:: character* -> string (total, injective) .
characters_	:: string -> character* (total, injective) .
 " "		::  string .
_^_		:: string, string -> string  (total, associative, unit is " ") .
_is_		:: string, string -> truth-value (total) .
(1) "" = empty-list .
(2) string of c:character* = list of c .
(3) characters s:string = items s .
(4) (s1:string)^(s2:string) = concatenation (s1, s2) .

introduces: lowercase_ , uppercase_ , decimal_ , octal-digit , octal _ . 

needs:      Tuples/Basics, Numbers/Naturals .
 lowercase_ 	:: string -> string (total) . 
 uppercase_  	:: string -> string (total) .
 decimal_  		:: string of digit+ -> natural (total) . 
 octal _ 		:: string of octal-digit+ -> natural (total) .
 octal-digit 	=  ` 0 ' | ` 1 ' | ` 2 ' | ` 3 ' | ` 4 ' | ` 5 ' | ` 6 ' | ` 7 '  .
(1) lowercase " " = " " ; lowercase string of c:character = string of lowercase c;
     	lowercase (s1:string ^ s2:string) = lowercase s1 ^ lowercase s2 .
(2) uppercase "" = "" ; uppercase string of c:character = string of uppercase c;
     	uppercase (s1:string ^ s2:string) = uppercase s1 ^ uppercase s2 .
(3) decimal "0" = 0 ; decimal "1" = 1 ; decimal "2" = 2 ; 
    	decimal "3" = 3 ; decimal "4" = 4 ; decimal "5" = 5 ; 
    	decimal "6" = 6 ; decimal "7" = 7 ; decimal "8" = 8 ; 
    	decimal "9" = 9 ;
    	decimal (s:string of digit+ ^ string of d:digit) = 
 	    	sum (product (10, decimal s), decimal (string of d)) .
(4) octal (string of d:octal-digit) = decimal (string of d) ; 
    	octal "8" = nothing ;  octal "9" = nothing ; 
    	octal (s:string of octal-digit+ ^ string of d:octal-digit)=
 	    	sum (product (8, octal s), octal (string of d)) .