introduces: character , character of _ , code _ .

includes:   Instant/Partial Order ( character for s , _ is _ , _ is less than _ ) .

needs:      Numbers/Naturals .
character = ž .
character of _ :: natural -> character (partial, injective) . 
code _ :: character -> natural (total, injective) .
(1)  character of code c:character = c .
(2)  c:character is c':character = code c is code c' .
(3)  c:character is less than c':character = code c is less than code c' .

open .

introduces:  digit , letter , lowercase _ , uppercase _ . 

character >= digit | letter  (disjoint) .
digit = `0'|`1'|`2'|`3'|`4'|`5'|`6'|`7'|`8'|`9'  (individual) .
letter = lowercase letter | uppercase letter (disjoint) . 
lowercase letter = `a'|...|`z' (individual) .
uppercase letter = `A'|...|`Z' (individual) .
lowercase _  :: character -> character (total) . 
uppercase _ :: character -> character (total) . 

needs:	Tuples .  character <= component .

(1) distinct (d:digit, l:lowercase letter, u:uppercase letter) = true .
(2) strictly-increasing (`0', `1', ..., `9') = true ;
(3) strictly-increasing (`a', `b', ..., `z') = true ;
(4) strictly-increasing (`A', `B', ..., `Z') = true .
(5) uppercase `a' = `A' ; lowercase `A' = `a' ;
     	...
     	uppercase `z' = `Z' . lowercase `Z' = `z' .
(6) lowercase lowercase l:letter = lowercase l ; 
          	uppercase uppercase l:letter = uppercase l .
(7) c&letter = nothing => lowercase c:character = c ; uppercase c:character = c .

open .

introduces:  graphic-character , control _ , control-character , format-effector .

needs:      Strings/Alphanumerics .
code _ :: character -> natural [max octal``177''] (total, injective) . 
character =  graphic-character | control-character .
graphic-character =
        ` '   |  `!'   |  `"'  | `#'  | `$'  | `%'   |  `&' | `''  | 
        `('   |  `)'   |  `*'  |  `+' | `,'  |  `--' |  `.' |  `/' |  
        digit |  `:'   |  `;'  | `<'  |  `=' |  `>'  | `?'  |  
        `@'   |  uppercase letter | `['  |  `\'   |  `]'   |  `^'  | `_'  |         
	  `''   |  lowercase letter | `{'   |  `|'   |  `}'  | `~' (individual) .
control _ :: `@' |uppercase letter|`['|`\'|`]'|`^'|`_'|`?' ->
	control-character (total, injective) . 
format-effector = control (`I'|`J'|`K'|`L'|`M') .
(1) c&(`@'|uppercase letter|`['|`\'|`]'|`^'|`_'|`?') = nothing =>
       		control c:character = nothing .
(2) code control`M' = control`@' = octal``000'' ;	control`A' = octal``001'' ; ...
 	code ` ' = octal``040'' ; ...
 	code `~' = octal``176'' ; code control`?' = octal``177'' .

closed .