%[% [ ] % %[

]%

%[ ]%

]%

%[ ]%

free type Nat ::= 0 | suc(pre:? Nat)

preds __ <= __, __ < __,

__ >= __, __ > __: Nat * Nat;

odd, even: Nat

ops min, max: Nat * Nat ->? Nat;

ops __ + __, __ * __: Nat * Nat -> Nat;

__ ^ __: Nat * Nat -> Nat;

min, max: Nat * Nat -> Nat;

+__: Nat -> Nat;

abs: Nat -> Nat;

__! : Nat -> Nat;

__ -?__: Nat * Nat ->? Nat;

__ /? __: Nat * Nat ->? Nat;

__ div __, __ mod __ , __ quot __, __ rem __ :Nat * Nat ->? Nat; %()%

%% Operations to represent natural numbers with digits:

1,2,3,4,5,6,7,8,9: Nat;

__ @@ __ : Nat * Nat -> Nat

forall m,n,r,s: Nat

. 0 <= n %(Nat_leq_def1)%

. not (suc(n) <= 0) %(Nat_leq_def2)%

. suc(m) <= suc(n) <=> m <= n %(Nat_leq_def3)%

. m >= n <=> n <= m %(Nat_geq_def)%

. m < n <=> (m <= n /\ not (m=n)) %(Nat_less_def)%

. m > n <=> m < n %(Nat_greater_def)%

. 0 + m = m %(Nat_add_0)%

. suc(n) + m = suc(n + m) %(Nat_add_suc)%

. 0 * m = 0 %(Nat_mult_0)%

. suc(n) * m = (n * m) + m %(Nat_mult_suc)%

. m ^ 0 = 1 %(Nat_power_0)%

. m ^ suc(n) = m * m ^ n %(Nat_power_suc)%

. min(m,n) = m when m <= n else n %(Nat_min_def)%

. max(m,n) = n when m <= n else m %(Nat_max_def)%

. + m = m %(plus_def)%

. abs(n) = n %(Nat_abs)%

. odd(m) <=> not even(m) %(Nat_odd_def)%

. even(0) %(Nat_even_0)%

. even(suc(m)) <=> odd(m) %(Nat_even_suc)%

. 0! = 1 %(Nat_factorial_0)%

. suc(n)! =suc(n)*n! %(Nat_factorial_suc)%

. m -? n = r <=> m = r + n %(Nat_sub_def)%

. not def(m /? 0) %(Nat_divide_0)%

. ( m /? n = r <=> m = r * n ) if n>0 %(Nat_divide_Pos)%

. m div n = r <=>

(exists s: Nat . m = n*r + s /\ s < n) %(Nat_div)%

. m mod n = s <=>

(exists r: Nat . m = n*r + s /\ s < n) %(Nat_mod)%

. m quot n = m div n %(Nat_quot)%

. m rem n = m mod n %(Nat_rem)%

. 1 = suc (0) %(Nat_1_def)%

. 2 = suc (1) %(Nat_2_def)%

. 3 = suc (2) %(Nat_3_def)%

. 4 = suc (3) %(Nat_4_def)%

. 5 = suc (4) %(Nat_5_def)%

. 6 = suc (5) %(Nat_6_def)%

. 7 = suc (6) %(Nat_7_def)%

. 8 = suc (7) %(Nat_8_def)%

. 9 = suc (8) %(Nat_9_def)%

. m @@ n = (m * suc(9)) + n %(Nat_decimal_def)%

%% then %def

sort Pos = { p: Nat . p > 0 }

op 1: Pos = suc(0); %(Nat_1_as_Pos_def)%

__*__: Pos * Pos -> Pos;

__+__: Pos * Nat -> Pos;

__+__: Nat * Pos -> Pos;

suc: Nat -> Pos

%% then %implies

ops min, max: Nat * Nat -> Nat, comm, assoc

forall x,m,n,r,s,t: Nat; p: Pos

. def(m-?n) <=> m >= n %(Nat_sub_dom)%

. def(m /? n) <=> m mod n = 0 %(Nat_divide_dom)%

. def ( m div n ) <=> not (n=0) %(Nat_div_dom)%

. def ( m mod n ) <=> not (n=0) %(Nat_mod_dom)%

. def ( m quot n ) <=> not (n=0) %(Nat_quot_dom)%

. def ( m rem n ) <=> not (n=0) %(Nat_rem_dom)%

. (r + s) * t = (r * t) + (s * t) %(Nat_distr)%

. max(m,0)=m %(Nat_max_unit)%

. min(m,0)=0 %(Nat_min_0)%

%% end

%[spec Int =

Nat

then %def

]%

generated type Int ::= __ - __(Nat;Nat)

forall a,b,c,d: Nat

. a - b = c - d <=> a + d = c + b %(Int_equality)%

%% then

sort Nat < Int

forall a: Nat

. a = a - 0 %(Int_Nat_embedding)%

preds __ <= __, __ < __,

__ >= __, __ > __: Int * Int;

odd, even: Int

ops 0,1: Int;

__ + __, __ - __,__ * __: Int * Int -> Int;

__ ^ __: Int * Nat -> Int;

+ __, - __, sign: Int -> Int;

min, max: Int * Int -> Int;

abs: Int -> Nat;

__ /? __,

__ div __, __ quot __, __ rem __ : Int * Int ->? Int;

__ mod __: Int * Int ->? Nat

forall m,n,r,s: Int; a,b,c,d: Nat

. (a - b) + (c - d) = (a + c) - (b + d) %(Int_add_def)%

. (a - b) * (c - d) =

(a * c + b * d) - (b * c + a * d) %(Int_mult_def)%

. m - n = m + ( - n ) %(Int_sub_def)%

. + m = m %(Int_pos_def)%

. - (a - b) = b - a %(Int_neg_def)%

. sign(m) = 0 when m = 0

else (1 when m > 0 else -1) %(Int_sign_def)%

. m <= n <=> n - m in Nat %(Int_leq_def)%

. m >= n <=> n <= m %(Int_geq_def)%

. m < n <=> (m <= n /\ not (m=n)) %(Int_less_def)%

. m > n <=> m < n %(Int_greater_def)%

. min(m,n) = m when m <= n else n %(Int_min_def)%

. max(m,n) = n when m <= n else m %(Int_max_def)%

. abs(m) = - m if m < 0 %(Int_abs_def)%

. (- 1) ^ a = 1 when even(a) else - 1 %(Int_neg1_power_def)%

. m ^ a = sign(m)^a * abs(m)^a %(Int_power_def)%

. even(m) <=> even(abs(m)) %(Int_even_def)%

. odd(m) <=> not(even(m)) %(Int_odd_def)%

. m /? n =

sign(m) * sign(n) * (abs(m) /? abs(n)) %(Int_divide)%

. m mod n < abs(n) if not n = 0 %(Int_mod_range)%

. m = (m div n) * n + (m mod n) if not n = 0

%(Int_mod__div_def)%

. not def m mod 0 %(Int_mod_zero)%

. not def m div 0 %(Int_div_zero)%

. m quot n =

sign(m) * sign(n) * (abs(m) quot abs(n)) %(Int_quot_def)%

. m rem n =

sign(m) * sign(n) * (abs(m) rem abs(n)) %(Int_rem_def)%

%% then %implies

%[ this is not legal, since -__:Nat->Int is not in the signature!

generated type Int::= Nat | -__ (Nat) ]%

forall m,n,r: Int; a,b: Nat

. def(a -? b) => a -? b = a - b %(Int_Nat_sub_compat)%

. m = sign(m) * abs(m) %(Int_abs_decomp)%

. odd(m) <=> odd(abs(m)) %(Int_odd_alt)%

. m /? n = r <=> not n = 0 /\ n * r = n %(Int_divide_dom1)%

. def (m /? n) <=> m mod n = 0 %(Int_divide_dom2)%

. def (m mod n) <=> not n = 0 %(Int_mod_dom)%

. m mod n = m mod abs(n) %(Int_mod_abs)%

. def (m div n) <=> not n = 0 %(Int_div_dom)%

. def (m quot n) <=> not n = 0 %(Int_quot_dom)%

. def (m rem n) <=> not n = 0 %(Int_rem_dom)%

. m = (m quot n) * n + (m rem n) if not n = 0 %(Int_quot_rem)%

%% end

%[spec Rat =

Int

then %def

]%

generated type Rat ::= __ / __ (Int;Pos)

forall i,j: Int; p,q: Pos

. i / p = j / q <=> i*q = j*p %(Rat_equality)%

sort Int < Rat

forall i:Int

. i / 1 = i %(embeddingIntToRat)%

%% then

preds __ <= __, __ < __,

__ >= __, __ > __: Rat * Rat;

ops 0,1: Rat;

__ + __,__ - __, __ * __ : Rat * Rat -> Rat;

__ / __ : Rat * Rat ->? Rat;

+__, -__, abs: Rat -> Rat;

__ ^ __: Rat * Int -> Rat;

min,max: Rat * Rat -> Rat;

forall p,q:Pos; n:Nat; i,j: Int; x,y,z: Rat

. (i / p <= j / q <=> i * q <= j * p ) %(Rat_leq_def)%

. x >= y <=> y <= x %(Rat_geq_def)%

. x < y <=> (x <= y /\ not (x=y)) %(Rat_less_def)%

. x > y <=> y < x %(Rat_greater_def)%

. (i / p) + (j / q) =

(i * q + j * p) / (p * q) %(Rat_add_def)%

. x-y = x + (-y) %(Rat_sub_def)%

. (i / p) * (j / q) =

(i * j) / (p * q) %(Rat_mult_def)%

. not def x/0 %(Rat_divide_def1)%

. (x/y=z <=> z=x*y)

if not y = 0 %(Rat_divide_def2)%

. + x = x %(Rat_plus_def)%

. - (i/p) = (-i)/p %(Rat_minus_def)%

. abs(i / p)= abs(i) / p %(Rat_abs_def)%

. x ^ 0 = 1 %(Rat_power_0)%

. x ^ suc(n) = x * x ^ n %(Rat_power_suc)%

. x ^ (-p) = 1 / (x ^ p) %(Rat_power_neg)%

. min(x,y) = x when x <= y else y %(Rat_min_def)%

. max(x,y) = y when x <= y else x %(Rat_max_def)%

%% then %implies

forall i,j: Int; p,q:Pos

. (i / p) - (j / q) =

(i * q - j * p) / (p * q) %(Rat_sub_rule)%

. (i / p) / (j / q) =

(i / p) * (q / j) if not j=0 %(Rat_divide_rule)%

pred __ < __ : a * a

op __a: b; c: b

sort s, t < s ;

. a = a

vars a:t; a,b:s

vars a:t; a,b:s ;

. a = a

. a = a

forall a:t; a,b:s

. a = a

. a = a

axioms a = a ;

a = a ;

axiom a = a

; a = a

type s ::= sort s2,s1 | c | c(a; a,b:t; a,d:t) | c(a)?

free type s ::= sort s2,s1 | c | c(a; a,b:t; d:t) | c(a)?

generated type s ::= sort s2,s1 | c | c(a; a,b:t; d:t) | c(a)?

generated {

pred __ < __ : a * a

op a: b; c: b

sort s, t < s ;

type s ::= sort s2,s1 | c | c(a) | c(a; a,b:t; d:t) | c(a)?

%(bla1)%

}

%(sort)%

sort %(after-sort)%

s; %(bla2)%

t

%(op)%

op a:b; %(bla4)%

c:d %(bla5)%

%(bla6)%

vars a:t;

a,b:s ; %(bla8-ignored)%

%(type)%

type t ::= %(c)% c %(c)% | e %(e)% | d %(9)%

%(axiom)%

axioms

a = a; %(a1)%

a = a; %(a2)%

%(formula)%

. a = a %(f1)%

. a = a ; %(f1)%

sort s

sorts s,

abcdefghijlklmnopqrstuvwxyz,

ABCDEFGHIJKLMONOPQRSTUVWXYZ,

x0123456789,

ÀÁÂÃÄÅÆÇÈÉÊËÌÍÎÏÑÒÓÔÕÖØÙÚÛÜÝßàáâãäåæçèéêëìíîïñòóôõöøùúûüýÿ,

abc, a_b_c, ab2, ab_2_3_a, a', a'b''2 %[WORDS]%

%[.abc, .a_b_c, .ab2, .ab_2_3_a, .a', .a'b''2, DOT-WORDS]%

op __+-*/\&=<>!?:.$@#^~¡¿×÷£©±¶§¹²³·¢¬°|__ : s*s->s %% NO-BRACKET-SIGNs

ops 'a','"','\\','\n','\000','\255',

'\x00','\xFF','\o000','\o377',

'^','1','2','3','4','5','6','7','8','9','0',

'ß','!','§','$','&','/','(',')','=','?','\\' : s; %%characters

%[. def "^1234567890ß!§$&/()=?"; ]%

%[ strings ´°%\\\" does not work yet!]%

ops 1,2,3,4 : s;

- : s->s;

__@@__,__exp__,__frac__ : s*s->s;

. def 12 . def 12E34 . def 12E-34 . def 12.34 %%numbers

. def 12.34E34 . def 12.34E+34 . def 12.34E-34 %%fractions

. true %(The true formula)%

. true %(and this

also goes

along several lines!

and with special stuff: -*/\&=<>BCDEFGHIJKLM!% )%

sort s;

op __and'__:s

sort a;

sorts a,b,c;

sort a<b;

sorts a,b,c,d < e;

sorts a=b=c=d=e;

sort a = {x:b . true}

sorts s,t;

op a:s;

op b:s->s;

ops c:s*s->s, assoc, comm, idem, unit a;

c:s*s*s->s;

op a: ?s; %[ Should be: op a:?s ]%

op b:s->?s;

op c:s*s->?s, assoc, comm, idem, unit a;

op c:s*s*s->?s;

op a:s=a;

op c(x,y:s;z:t):s = a;

op a:?s=a;

op c(x,y:s;z:t):?s = a;

%[op a: ?s=a;

op c(x,y:s;z:t): ?s = a; ]%

sorts s,t;

pred a:();

pred b:s;

preds c:s*s;

c:s*s*s;

%[pred a:()<=> true;

pred c(x,y:s;z:t)<=>false;

pred a: () <=> true; ]%

pred c(x,y:s;z:t) <=> false;

type Data1 ::= a | b | c;

type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1

type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?

Data1)

type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:

?Data1)?

sorts Data1, Data2, Data3

types Tree ::= Leaf (Data1) | Forest;

Forest ::= Nil | Cons (Tree;Forest)

free type List ::= Nil | Cons(Data1; List)

generated type Set ::= Mt | Add(Data1; Set)

generated {type Set ::= Mt | Add(Data1; Set)}

generated {sort nat; ops 0:nat; succ:nat->nat; }

sorts s<t

ops f,g:s->?s;

g:s->t;

__+__,__-__,__*__,__/__ : s*s->s;

{}:s;

{__} : s->s

preds p:(); q:s

vars x,y,z:s; r1,r2:t

. false

var x:s . true

. not p /\ not q(x) /\ q(x)

. not p \/ not q(x) \/ q(x)

. not p /\ not q(x) /\ q(x) => not p \/ not q(x) \/ q(x) => not p /\ not q(x) /\ q(x)

. not p /\ not q(x) /\ q(x) if not p \/ not q(x) \/ q(x) if not p /\ not q(x) /\ q(x)

%[. not p /\ not q(x) /\ q(x) <=> not p \/ not q(x) \/ q(x) <=> not p /\ not q(x) /\ q(x)]%

forall x:s . not p /\ not q(x) /\ q(x)

<=> exists x:s . not p \/ not q(x) \/ q(x) <=> exists! x:s . not p /\ not q(x) /\ q(x)

. def f(x)

. f(x) =e= g(x)

. f(x) = g(x)

. r1 in s

. def g(x):t

. def g(x) as s

. def (op f:s->?s)(x) %[ (var x:s) ]%

. def (op g:s->t)(x)

. (pred p:())

. (pred q:s)(x)

. def x*y*z+z*y*x

. def {}

. def {x}

axioms true ;exists! x:s.e;

forall x:s.e

%[spec Boolean =

]%

free type Boolean ::= True | False

ops Not__ : Boolean -> Boolean;

__And__, __Or__ : Boolean * Boolean -> Boolean

forall x,y,z:Boolean

. Not(False) = True %(Not_False)%

. Not(True) = False %(Not_True)%

. False And False = False %(And_def1)%

. False And True = False %(And_def2)%

. True And False = False %(And_def3)%

. True And True = True %(And_def4)%

. x Or y = Not(Not(x) And Not(y)) %(Or_def)%

sort Char

ops chr : Nat ->? Char;

ord : Char -> Nat;

forall n:Nat; c:Char

. def chr(n) <=> n <= 255 %(chr_dom)%

. chr(ord(c))=c %(chr_def)%

. ord(chr(n))=n if n <= 255 %(ord_def)%

%% definition of individual characters:

ops '\000' : Char = chr(0); %(slash_000)%

'\001' : Char = chr(1); %(slash_001)%

'\002' : Char = chr(2); %(slash_002)%

'\003' : Char = chr(3); %(slash_003)%

'\004' : Char = chr(4); %(slash_004)%

'\005' : Char = chr(5); %(slash_005)%

'\006' : Char = chr(6); %(slash_006)%

'\007' : Char = chr(7); %(slash_007)%

'\008' : Char = chr(8); %(slash_008)%

'\009' : Char = chr(9); %(slash_009)%

'\010' : Char = chr(10); %(slash_010)%

'\011' : Char = chr(11); %(slash_011)%

'\012' : Char = chr(12); %(slash_012)%

'\013' : Char = chr(13); %(slash_013)%

'\014' : Char = chr(14); %(slash_014)%

'\015' : Char = chr(15); %(slash_015)%

'\016' : Char = chr(16); %(slash_016)%

'\017' : Char = chr(17); %(slash_017)%

'\018' : Char = chr(18); %(slash_018)%

'\019' : Char = chr(19); %(slash_019)%

'\020' : Char = chr(20); %(slash_020)%

'\021' : Char = chr(21); %(slash_021)%

'\022' : Char = chr(22); %(slash_022)%

'\023' : Char = chr(23); %(slash_023)%

'\024' : Char = chr(24); %(slash_024)%

'\025' : Char = chr(25); %(slash_025)%

'\026' : Char = chr(26); %(slash_026)%

'\027' : Char = chr(27); %(slash_027)%

'\028' : Char = chr(28); %(slash_028)%

'\029' : Char = chr(29); %(slash_029)%

'\030' : Char = chr(30); %(slash_030)%

'\031' : Char = chr(31); %(slash_031)%

'\032' : Char = chr(32); %(slash_032)%

'\033' : Char = chr(33); %(slash_033)%

'\034' : Char = chr(34); %(slash_034)%

'\035' : Char = chr(35); %(slash_035)%

'\036' : Char = chr(36); %(slash_036)%

'\037' : Char = chr(37); %(slash_037)%

'\038' : Char = chr(38); %(slash_038)%

'\039' : Char = chr(39); %(slash_039)%

'\040' : Char = chr(40); %(slash_040)%

'\041' : Char = chr(41); %(slash_041)%

'\042' : Char = chr(42); %(slash_042)%

'\043' : Char = chr(43); %(slash_043)%

'\044' : Char = chr(44); %(slash_044)%

'\045' : Char = chr(45); %(slash_045)%

'\046' : Char = chr(46); %(slash_046)%

'\047' : Char = chr(47); %(slash_047)%

'\048' : Char = chr(48); %(slash_048)%

'\049' : Char = chr(49); %(slash_049)%

'\050' : Char = chr(50); %(slash_050)%

'\051' : Char = chr(51); %(slash_051)%

'\052' : Char = chr(52); %(slash_052)%

'\053' : Char = chr(53); %(slash_053)%

'\054' : Char = chr(54); %(slash_054)%

'\055' : Char = chr(55); %(slash_055)%

'\056' : Char = chr(56); %(slash_056)%

'\057' : Char = chr(57); %(slash_057)%

'\058' : Char = chr(58); %(slash_058)%

'\059' : Char = chr(59); %(slash_059)%

'\060' : Char = chr(60); %(slash_060)%

'\061' : Char = chr(61); %(slash_061)%

'\062' : Char = chr(62); %(slash_062)%

'\063' : Char = chr(63); %(slash_063)%

'\064' : Char = chr(64); %(slash_064)%

'\065' : Char = chr(65); %(slash_065)%

'\066' : Char = chr(66); %(slash_066)%

'\067' : Char = chr(67); %(slash_067)%

'\068' : Char = chr(68); %(slash_068)%

'\069' : Char = chr(69); %(slash_069)%

'\070' : Char = chr(70); %(slash_070)%

'\071' : Char = chr(71); %(slash_071)%

'\072' : Char = chr(72); %(slash_072)%

'\073' : Char = chr(73); %(slash_073)%

'\074' : Char = chr(74); %(slash_074)%

'\075' : Char = chr(75); %(slash_075)%

'\076' : Char = chr(76); %(slash_076)%

'\077' : Char = chr(77); %(slash_077)%

'\078' : Char = chr(78); %(slash_078)%

'\079' : Char = chr(79); %(slash_079)%

'\080' : Char = chr(80); %(slash_080)%

'\081' : Char = chr(81); %(slash_081)%

'\082' : Char = chr(82); %(slash_082)%

'\083' : Char = chr(83); %(slash_083)%

'\084' : Char = chr(84); %(slash_084)%

'\085' : Char = chr(85); %(slash_085)%

'\086' : Char = chr(86); %(slash_086)%

'\087' : Char = chr(87); %(slash_087)%

'\088' : Char = chr(88); %(slash_088)%

'\089' : Char = chr(89); %(slash_089)%

'\090' : Char = chr(90); %(slash_090)%

'\091' : Char = chr(91); %(slash_091)%

'\092' : Char = chr(92); %(slash_092)%

'\093' : Char = chr(93); %(slash_093)%

'\094' : Char = chr(94); %(slash_094)%

'\095' : Char = chr(95); %(slash_095)%

'\096' : Char = chr(96); %(slash_096)%

'\097' : Char = chr(97); %(slash_097)%

'\098' : Char = chr(98); %(slash_098)%

'\099' : Char = chr(99); %(slash_099)%

'\100' : Char = chr(100); %(slash_100)%

'\101' : Char = chr(101); %(slash_101)%

'\102' : Char = chr(102); %(slash_102)%

'\103' : Char = chr(103); %(slash_103)%

'\104' : Char = chr(104); %(slash_104)%

'\105' : Char = chr(105); %(slash_105)%

'\106' : Char = chr(106); %(slash_106)%

'\107' : Char = chr(107); %(slash_107)%

'\108' : Char = chr(108); %(slash_108)%

'\109' : Char = chr(109); %(slash_109)%

'\110' : Char = chr(110); %(slash_110)%

'\111' : Char = chr(111); %(slash_111)%

'\112' : Char = chr(112); %(slash_112)%

'\113' : Char = chr(113); %(slash_113)%

'\114' : Char = chr(114); %(slash_114)%

'\115' : Char = chr(115); %(slash_115)%

'\116' : Char = chr(116); %(slash_116)%

'\117' : Char = chr(117); %(slash_117)%

'\118' : Char = chr(118); %(slash_118)%

'\119' : Char = chr(119); %(slash_119)%

'\120' : Char = chr(120); %(slash_120)%

'\121' : Char = chr(121); %(slash_121)%

'\122' : Char = chr(122); %(slash_122)%

'\123' : Char = chr(123); %(slash_123)%

'\124' : Char = chr(124); %(slash_124)%

'\125' : Char = chr(125); %(slash_125)%

'\126' : Char = chr(126); %(slash_126)%

'\127' : Char = chr(127); %(slash_127)%

'\128' : Char = chr(128); %(slash_128)%

'\129' : Char = chr(129); %(slash_129)%

'\130' : Char = chr(130); %(slash_130)%

'\131' : Char = chr(131); %(slash_131)%

'\132' : Char = chr(132); %(slash_132)%

'\133' : Char = chr(133); %(slash_133)%

'\134' : Char = chr(134); %(slash_134)%

'\135' : Char = chr(135); %(slash_135)%

'\136' : Char = chr(136); %(slash_136)%

'\137' : Char = chr(137); %(slash_137)%

'\138' : Char = chr(138); %(slash_138)%

'\139' : Char = chr(139); %(slash_139)%

'\140' : Char = chr(140); %(slash_140)%

'\141' : Char = chr(141); %(slash_141)%

'\142' : Char = chr(142); %(slash_142)%

'\143' : Char = chr(143); %(slash_143)%

'\144' : Char = chr(144); %(slash_144)%

'\145' : Char = chr(145); %(slash_145)%

'\146' : Char = chr(146); %(slash_146)%

'\147' : Char = chr(147); %(slash_147)%

'\148' : Char = chr(148); %(slash_148)%

'\149' : Char = chr(149); %(slash_149)%

'\150' : Char = chr(150); %(slash_150)%

'\151' : Char = chr(151); %(slash_151)%

'\152' : Char = chr(152); %(slash_152)%

'\153' : Char = chr(153); %(slash_153)%

'\154' : Char = chr(154); %(slash_154)%

'\155' : Char = chr(155); %(slash_155)%

'\156' : Char = chr(156); %(slash_156)%

'\157' : Char = chr(157); %(slash_157)%

'\158' : Char = chr(158); %(slash_158)%

'\159' : Char = chr(159); %(slash_159)%

'\160' : Char = chr(160); %(slash_160)%

'\161' : Char = chr(161); %(slash_161)%

'\162' : Char = chr(162); %(slash_162)%

'\163' : Char = chr(163); %(slash_163)%

'\164' : Char = chr(164); %(slash_164)%

'\165' : Char = chr(165); %(slash_165)%

'\166' : Char = chr(166); %(slash_166)%

'\167' : Char = chr(167); %(slash_167)%

'\168' : Char = chr(168); %(slash_168)%

'\169' : Char = chr(169); %(slash_169)%

'\170' : Char = chr(170); %(slash_170)%

'\171' : Char = chr(171); %(slash_171)%

'\172' : Char = chr(172); %(slash_172)%

'\173' : Char = chr(173); %(slash_173)%

'\174' : Char = chr(174); %(slash_174)%

'\175' : Char = chr(175); %(slash_175)%

'\176' : Char = chr(176); %(slash_176)%

'\177' : Char = chr(177); %(slash_177)%

'\178' : Char = chr(178); %(slash_178)%

'\179' : Char = chr(179); %(slash_179)%

'\180' : Char = chr(180); %(slash_180)%

'\181' : Char = chr(181); %(slash_181)%

'\182' : Char = chr(182); %(slash_182)%

'\183' : Char = chr(183); %(slash_183)%

'\184' : Char = chr(184); %(slash_184)%

'\185' : Char = chr(185); %(slash_185)%

'\186' : Char = chr(186); %(slash_186)%

'\187' : Char = chr(187); %(slash_187)%

'\188' : Char = chr(188); %(slash_188)%

'\189' : Char = chr(189); %(slash_189)%

'\190' : Char = chr(190); %(slash_190)%

'\191' : Char = chr(191); %(slash_191)%

'\192' : Char = chr(192); %(slash_192)%

'\193' : Char = chr(193); %(slash_193)%

'\194' : Char = chr(194); %(slash_194)%

'\195' : Char = chr(195); %(slash_195)%

'\196' : Char = chr(196); %(slash_196)%

'\197' : Char = chr(197); %(slash_197)%

'\198' : Char = chr(198); %(slash_198)%

'\199' : Char = chr(199); %(slash_199)%

'\200' : Char = chr(200); %(slash_200)%

'\201' : Char = chr(201); %(slash_201)%

'\202' : Char = chr(202); %(slash_202)%

'\203' : Char = chr(203); %(slash_203)%

'\204' : Char = chr(204); %(slash_204)%

'\205' : Char = chr(205); %(slash_205)%

'\206' : Char = chr(206); %(slash_206)%

'\207' : Char = chr(207); %(slash_207)%

'\208' : Char = chr(208); %(slash_208)%

'\209' : Char = chr(209); %(slash_209)%

'\210' : Char = chr(210); %(slash_210)%

'\211' : Char = chr(211); %(slash_211)%

'\212' : Char = chr(212); %(slash_212)%

'\213' : Char = chr(213); %(slash_213)%

'\214' : Char = chr(214); %(slash_214)%

'\215' : Char = chr(215); %(slash_215)%

'\216' : Char = chr(216); %(slash_216)%

'\217' : Char = chr(217); %(slash_217)%

'\218' : Char = chr(218); %(slash_218)%

'\219' : Char = chr(219); %(slash_219)%

'\220' : Char = chr(220); %(slash_220)%

'\221' : Char = chr(221); %(slash_221)%

'\222' : Char = chr(222); %(slash_222)%

'\223' : Char = chr(223); %(slash_223)%

'\224' : Char = chr(224); %(slash_224)%

'\225' : Char = chr(225); %(slash_225)%

'\226' : Char = chr(226); %(slash_226)%

'\227' : Char = chr(227); %(slash_227)%

'\228' : Char = chr(228); %(slash_228)%

'\229' : Char = chr(229); %(slash_229)%

'\230' : Char = chr(230); %(slash_230)%

'\231' : Char = chr(231); %(slash_231)%

'\232' : Char = chr(232); %(slash_232)%

'\233' : Char = chr(233); %(slash_233)%

'\234' : Char = chr(234); %(slash_234)%

'\235' : Char = chr(235); %(slash_235)%

'\236' : Char = chr(236); %(slash_236)%

'\237' : Char = chr(237); %(slash_237)%

'\238' : Char = chr(238); %(slash_238)%

'\239' : Char = chr(239); %(slash_239)%

'\240' : Char = chr(240); %(slash_240)%

'\241' : Char = chr(241); %(slash_241)%

'\242' : Char = chr(242); %(slash_242)%

'\243' : Char = chr(243); %(slash_243)%

'\244' : Char = chr(244); %(slash_244)%

'\245' : Char = chr(245); %(slash_245)%

'\246' : Char = chr(246); %(slash_246)%

'\247' : Char = chr(247); %(slash_247)%

'\248' : Char = chr(248); %(slash_248)%

'\249' : Char = chr(249); %(slash_249)%

'\250' : Char = chr(250); %(slash_250)%

'\251' : Char = chr(251); %(slash_251)%

'\252' : Char = chr(252); %(slash_252)%

'\253' : Char = chr(253); %(slash_253)%

'\254' : Char = chr(254); %(slash_254)%

'\255' : Char = chr(255); %(slash_255)%

%% definition of the printable characters:

ops ' ' : Char = '\032'; %(printable_32)%

'!' : Char = '\033'; %(printable_33)%

'\"' : Char = '\034'; %(printable_34)%

'#' : Char = '\035'; %(printable_35)%

'$' : Char = '\036'; %(printable_36)%

'%' : Char = '\037'; %(printable_37)%

'&' : Char = '\038'; %(printable_38)%

'\'' : Char = '\039'; %(printable_39)%

'(' : Char = '\040'; %(printable_40)%

')' : Char = '\041'; %(printable_41)%

'*' : Char = '\042'; %(printable_42)%

'+' : Char = '\043'; %(printable_43)%

',' : Char = '\044'; %(printable_44)%

'-' : Char = '\045'; %(printable_45)%

'.' : Char = '\046'; %(printable_46)%

'/' : Char = '\047'; %(printable_47)%

'0' : Char = '\048'; %(printable_48)%

'1' : Char = '\049'; %(printable_49)%

'2' : Char = '\050'; %(printable_50)%

'3' : Char = '\051'; %(printable_51)%

'4' : Char = '\052'; %(printable_52)%

'5' : Char = '\053'; %(printable_53)%

'6' : Char = '\054'; %(printable_54)%

'7' : Char = '\055'; %(printable_55)%

'8' : Char = '\056'; %(printable_56)%

'9' : Char = '\057'; %(printable_57)%

':' : Char = '\058'; %(printable_58)%

';' : Char = '\059'; %(printable_59)%

'<' : Char = '\060'; %(printable_60)%

'=' : Char = '\061'; %(printable_61)%

'>' : Char = '\062'; %(printable_62)%

'?' : Char = '\063'; %(printable_63)%

'@' : Char = '\064'; %(printable_64)%

'A' : Char = '\065'; %(printable_65)%

'B' : Char = '\066'; %(printable_66)%

'C' : Char = '\067'; %(printable_67)%

'D' : Char = '\068'; %(printable_68)%

'E' : Char = '\069'; %(printable_69)%

'F' : Char = '\070'; %(printable_70)%

'G' : Char = '\071'; %(printable_71)%

'H' : Char = '\072'; %(printable_72)%

'I' : Char = '\073'; %(printable_73)%

'J' : Char = '\074'; %(printable_74)%

'K' : Char = '\075'; %(printable_75)%

'L' : Char = '\076'; %(printable_76)%

'M' : Char = '\077'; %(printable_77)%

'N' : Char = '\078'; %(printable_78)%

'O' : Char = '\079'; %(printable_79)%

'P' : Char = '\080'; %(printable_80)%

'Q' : Char = '\081'; %(printable_81)%

'R' : Char = '\082'; %(printable_82)%

'S' : Char = '\083'; %(printable_83)%

'T' : Char = '\084'; %(printable_84)%

'U' : Char = '\085'; %(printable_85)%

'V' : Char = '\086'; %(printable_86)%

'W' : Char = '\087'; %(printable_87)%

'X' : Char = '\088'; %(printable_88)%

'Y' : Char = '\089'; %(printable_89)%

'Z' : Char = '\090'; %(printable_90)%

'[' : Char = '\091'; %(printable_91)%

'\\' : Char = '\092'; %(printable_92)%

']' : Char = '\093'; %(printable_93)%

'^' : Char = '\094'; %(printable_94)%

'_' : Char = '\095'; %(printable_95)%

'`' : Char = '\096'; %(printable_96)%

'a' : Char = '\097'; %(printable_97)%

'b' : Char = '\098'; %(printable_98)%

'c' : Char = '\099'; %(printable_99)%

'd' : Char = '\100' ; %(printable_100)%

'e' : Char = '\101' ; %(printable_101)%

'f' : Char = '\102' ; %(printable_102)%

'g' : Char = '\103' ; %(printable_103)%

'h' : Char = '\104' ; %(printable_104)%

'i' : Char = '\105' ; %(printable_105)%

'j' : Char = '\106' ; %(printable_106)%

'k' : Char = '\107' ; %(printable_107)%

'l' : Char = '\108' ; %(printable_108)%

'm' : Char = '\109' ; %(printable_109)%

'n' : Char = '\110' ; %(printable_110)%

'o' : Char = '\111' ; %(printable_111)%

'p' : Char = '\112' ; %(printable_112)%

'q' : Char = '\113' ; %(printable_113)%

'r' : Char = '\114' ; %(printable_114)%

's' : Char = '\115' ; %(printable_115)%

't' : Char = '\116' ; %(printable_116)%

'u' : Char = '\117' ; %(printable_117)%

'v' : Char = '\118' ; %(printable_118)%

'w' : Char = '\119' ; %(printable_119)%

'x' : Char = '\120' ; %(printable_120)%

'y' : Char = '\121' ; %(printable_121)%

'z' : Char = '\122' ; %(printable_122)%

'{' : Char = '\123' ; %(printable_123)%

'|' : Char = '\124' ; %(printable_124)%

'}' : Char = '\125' ; %(printable_125)%

'~' : Char = '\126' ; %(printable_126)%

' ' : Char = '\160' ; %(printable_160)%

'¡' : Char = '\161' ; %(printable_161)%

'¢' : Char = '\162' ; %(printable_162)%

'£' : Char = '\163' ; %(printable_163)%

'¤' : Char = '\164' ; %(printable_164)%

'¥' : Char = '\165' ; %(printable_165)%

'¦' : Char = '\166' ; %(printable_166)%

'§' : Char = '\167' ; %(printable_167)%

'¨' : Char = '\168' ; %(printable_168)%

'©' : Char = '\169' ; %(printable_169)%

'ª' : Char = '\170' ; %(printable_170)%

'«' : Char = '\171' ; %(printable_171)%

'¬' : Char = '\172' ; %(printable_172)%

'­' : Char = '\173' ; %(printable_173)%

'®' : Char = '\174' ; %(printable_174)%

'¯' : Char = '\175' ; %(printable_175)%

'°' : Char = '\176' ; %(printable_176)%

'±' : Char = '\177' ; %(printable_177)%

'²' : Char = '\178' ; %(printable_178)%

'³' : Char = '\179' ; %(printable_179)%

'´' : Char = '\180' ; %(printable_180)%

'µ' : Char = '\181' ; %(printable_181)%

'¶' : Char = '\182' ; %(printable_182)%

'·' : Char = '\183' ; %(printable_183)%

'¸' : Char = '\184' ; %(printable_184)%

'¹' : Char = '\185' ; %(printable_185)%

'º' : Char = '\186' ; %(printable_186)%

'»' : Char = '\187' ; %(printable_187)%

'¼' : Char = '\188' ; %(printable_188)%

'½' : Char = '\189' ; %(printable_189)%

'¾' : Char = '\190' ; %(printable_190)%

'¿' : Char = '\191' ; %(printable_191)%

'À' : Char = '\192' ; %(printable_192)%

'Á' : Char = '\193' ; %(printable_193)%

'Â' : Char = '\194' ; %(printable_194)%

'Ã' : Char = '\195' ; %(printable_195)%

'Ä' : Char = '\196' ; %(printable_196)%

'Å' : Char = '\197' ; %(printable_197)%

'Æ' : Char = '\198' ; %(printable_198)%

'Ç' : Char = '\199' ; %(printable_199)%

'È' : Char = '\200' ; %(printable_200)%

'É' : Char = '\201' ; %(printable_201)%

'Ê' : Char = '\202' ; %(printable_202)%

'Ë' : Char = '\203' ; %(printable_203)%

'Ì' : Char = '\204' ; %(printable_204)%

'Í' : Char = '\205' ; %(printable_205)%

'Î' : Char = '\206' ; %(printable_206)%

'Ï' : Char = '\207' ; %(printable_207)%

'Ð' : Char = '\208' ; %(printable_208)%

'Ñ' : Char = '\209' ; %(printable_209)%

'Ò' : Char = '\210' ; %(printable_210)%

'Ó' : Char = '\211' ; %(printable_211)%

'Ô' : Char = '\212' ; %(printable_212)%

'Õ' : Char = '\213' ; %(printable_213)%

'Ö' : Char = '\214' ; %(printable_214)%

'×' : Char = '\215' ; %(printable_215)%

'Ø' : Char = '\216' ; %(printable_216)%

'Ù' : Char = '\217' ; %(printable_217)%

'Ú' : Char = '\218' ; %(printable_218)%

'Û' : Char = '\219' ; %(printable_219)%

'Ü' : Char = '\220' ; %(printable_220)%

'Ý' : Char = '\221' ; %(printable_221)%

'Þ' : Char = '\222' ; %(printable_222)%

'ß' : Char = '\223' ; %(printable_223)%

'à' : Char = '\224' ; %(printable_224)%

'á' : Char = '\225' ; %(printable_225)%

'â' : Char = '\226' ; %(printable_226)%

'ã' : Char = '\227' ; %(printable_227)%

'ä' : Char = '\228' ; %(printable_228)%

'å' : Char = '\229' ; %(printable_229)%

'æ' : Char = '\230' ; %(printable_230)%

'ç' : Char = '\231' ; %(printable_231)%

'è' : Char = '\232' ; %(printable_232)%

'é' : Char = '\233' ; %(printable_233)%

'ê' : Char = '\234' ; %(printable_234)%

'ë' : Char = '\235' ; %(printable_235)%

'ì' : Char = '\236' ; %(printable_236)%

'í' : Char = '\237' ; %(printable_237)%

'î' : Char = '\238' ; %(printable_238)%

'ï' : Char = '\239' ; %(printable_239)%

'ð' : Char = '\240' ; %(printable_240)%

'ñ' : Char = '\241' ; %(printable_241)%

'ò' : Char = '\242' ; %(printable_242)%

'ó' : Char = '\243' ; %(printable_243)%

'ô' : Char = '\244' ; %(printable_244)%

'õ' : Char = '\245' ; %(printable_245)%

'ö' : Char = '\246' ; %(printable_246)%

'÷' : Char = '\247' ; %(printable_247)%

'ø' : Char = '\248' ; %(printable_248)%

'ù' : Char = '\249' ; %(printable_249)%

'ú' : Char = '\250' ; %(printable_250)%

'û' : Char = '\251' ; %(printable_251)%

'ü' : Char = '\252' ; %(printable_252)%

'ý' : Char = '\253' ; %(printable_253)%

'þ' : Char = '\254' ; %(printable_254)%

'ÿ' : Char = '\255' ; %(printable_255)%

preds isLetter(c:Char) <=> (

(ord('A') <= ord(c) /\ ord(c) <= ord('Z')) \/

(ord('a') <= ord(c) /\ ord(c) <= ord('z')) ); %(isLetter_def)%

isDigit(c:Char) <=> ord('0') <= ord(c) /\ ord(c) <= ord('9'); %(isDigit_def)%

isPrintable(c:Char) <=> (

(ord(' ') <= ord(c) /\ ord(c) <= ord('~') ) \/

(ord(' ') <= ord(c) /\ ord(c) <= ord('ÿ')) ) %(isPrintable_def)%

%% alternative definition of characters as '\o ppp',

%% where p in {0,1,...,7} :

ops '\o000' : Char = '\000'; %(slash_o000)%

'\o001' : Char = '\001'; %(slash_o001)%

'\o002' : Char = '\002'; %(slash_o002)%

'\o003' : Char = '\003'; %(slash_o003)%

'\o004' : Char = '\004'; %(slash_o004)%

'\o005' : Char = '\005'; %(slash_o005)%

'\o006' : Char = '\006'; %(slash_o006)%

'\o007' : Char = '\007'; %(slash_o007)%

'\o010' : Char = '\008'; %(slash_o010)%

'\o011' : Char = '\009'; %(slash_o011)%

'\o012' : Char = '\010'; %(slash_o012)%

'\o013' : Char = '\011'; %(slash_o013)%

'\o014' : Char = '\012'; %(slash_o014)%

'\o015' : Char = '\013'; %(slash_o015)%

'\o016' : Char = '\014'; %(slash_o016)%

'\o017' : Char = '\015'; %(slash_o017)%

'\o020' : Char = '\016'; %(slash_o020)%

'\o021' : Char = '\017'; %(slash_o021)%

'\o022' : Char = '\018'; %(slash_o022)%

'\o023' : Char = '\019'; %(slash_o023)%

'\o024' : Char = '\020'; %(slash_o024)%

'\o025' : Char = '\021'; %(slash_o025)%

'\o026' : Char = '\022'; %(slash_o026)%

'\o027' : Char = '\023'; %(slash_o027)%

'\o030' : Char = '\024'; %(slash_o030)%

'\o031' : Char = '\025'; %(slash_o031)%

'\o032' : Char = '\026'; %(slash_o032)%

'\o033' : Char = '\027'; %(slash_o033)%

'\o034' : Char = '\028'; %(slash_o034)%

'\o035' : Char = '\029'; %(slash_o035)%

'\o036' : Char = '\030'; %(slash_o036)%

'\o037' : Char = '\031'; %(slash_o037)%

'\o040' : Char = '\032'; %(slash_o040)%

'\o041' : Char = '\033'; %(slash_o041)%

'\o042' : Char = '\034'; %(slash_o042)%

'\o043' : Char = '\035'; %(slash_o043)%

'\o044' : Char = '\036'; %(slash_o044)%

'\o045' : Char = '\037'; %(slash_o045)%

'\o046' : Char = '\038'; %(slash_o046)%

'\o047' : Char = '\039'; %(slash_o047)%

'\o050' : Char = '\040'; %(slash_o050)%

'\o051' : Char = '\041'; %(slash_o051)%

'\o052' : Char = '\042'; %(slash_o052)%

'\o053' : Char = '\043'; %(slash_o053)%

'\o054' : Char = '\044'; %(slash_o054)%

'\o055' : Char = '\045'; %(slash_o055)%

'\o056' : Char = '\046'; %(slash_o056)%

'\o057' : Char = '\047'; %(slash_o057)%

'\o060' : Char = '\048'; %(slash_o060)%

'\o061' : Char = '\049'; %(slash_o061)%

'\o062' : Char = '\050'; %(slash_o062)%

'\o063' : Char = '\051'; %(slash_o063)%

'\o064' : Char = '\052'; %(slash_o064)%

'\o065' : Char = '\053'; %(slash_o065)%

'\o066' : Char = '\054'; %(slash_o066)%

'\o067' : Char = '\055'; %(slash_o067)%

'\o070' : Char = '\056'; %(slash_o070)%

'\o071' : Char = '\057'; %(slash_o071)%

'\o072' : Char = '\058'; %(slash_o072)%

'\o073' : Char = '\059'; %(slash_o073)%

'\o074' : Char = '\060'; %(slash_o074)%

'\o075' : Char = '\061'; %(slash_o075)%

'\o076' : Char = '\062'; %(slash_o076)%

'\o077' : Char = '\063'; %(slash_o077)%

'\o100' : Char = '\064'; %(slash_o100)%

'\o101' : Char = '\065'; %(slash_o101)%

'\o102' : Char = '\066'; %(slash_o102)%

'\o103' : Char = '\067'; %(slash_o103)%

'\o104' : Char = '\068'; %(slash_o104)%

'\o105' : Char = '\069'; %(slash_o105)%

'\o106' : Char = '\070'; %(slash_o106)%

'\o107' : Char = '\071'; %(slash_o107)%

'\o110' : Char = '\072'; %(slash_o110)%

'\o111' : Char = '\073'; %(slash_o111)%

'\o112' : Char = '\074'; %(slash_o112)%

'\o113' : Char = '\075'; %(slash_o113)%

'\o114' : Char = '\076'; %(slash_o114)%

'\o115' : Char = '\077'; %(slash_o115)%

'\o116' : Char = '\078'; %(slash_o116)%

'\o117' : Char = '\079'; %(slash_o117)%

'\o120' : Char = '\080'; %(slash_o120)%

'\o121' : Char = '\081'; %(slash_o121)%

'\o122' : Char = '\082'; %(slash_o122)%

'\o123' : Char = '\083'; %(slash_o123)%

'\o124' : Char = '\084'; %(slash_o124)%

'\o125' : Char = '\085'; %(slash_o125)%

'\o126' : Char = '\086'; %(slash_o126)%

'\o127' : Char = '\087'; %(slash_o127)%

'\o130' : Char = '\088'; %(slash_o130)%

'\o131' : Char = '\089'; %(slash_o131)%

'\o132' : Char = '\090'; %(slash_o132)%

'\o133' : Char = '\091'; %(slash_o133)%

'\o134' : Char = '\092'; %(slash_o134)%

'\o135' : Char = '\093'; %(slash_o135)%

'\o136' : Char = '\094'; %(slash_o136)%

'\o137' : Char = '\095'; %(slash_o137)%

'\o140' : Char = '\096'; %(slash_o140)%

'\o141' : Char = '\097'; %(slash_o141)%

'\o142' : Char = '\098'; %(slash_o142)%

'\o143' : Char = '\099'; %(slash_o143)%

'\o144' : Char = '\100'; %(slash_o144)%

'\o145' : Char = '\101'; %(slash_o145)%

'\o146' : Char = '\102'; %(slash_o146)%

'\o147' : Char = '\103'; %(slash_o147)%

'\o150' : Char = '\104'; %(slash_o150)%

'\o151' : Char = '\105'; %(slash_o151)%

'\o152' : Char = '\106'; %(slash_o152)%

'\o153' : Char = '\107'; %(slash_o153)%

'\o154' : Char = '\108'; %(slash_o154)%

'\o155' : Char = '\109'; %(slash_o155)%

'\o156' : Char = '\110'; %(slash_o156)%

'\o157' : Char = '\111'; %(slash_o157)%

'\o160' : Char = '\112'; %(slash_o160)%

'\o161' : Char = '\113'; %(slash_o161)%

'\o162' : Char = '\114'; %(slash_o162)%

'\o163' : Char = '\115'; %(slash_o163)%

'\o164' : Char = '\116'; %(slash_o164)%

'\o165' : Char = '\117'; %(slash_o165)%

'\o166' : Char = '\118'; %(slash_o166)%

'\o167' : Char = '\119'; %(slash_o167)%

'\o170' : Char = '\120'; %(slash_o170)%

'\o171' : Char = '\121'; %(slash_o171)%

'\o172' : Char = '\122'; %(slash_o172)%

'\o173' : Char = '\123'; %(slash_o173)%

'\o174' : Char = '\124'; %(slash_o174)%

'\o175' : Char = '\125'; %(slash_o175)%

'\o176' : Char = '\126'; %(slash_o176)%

'\o177' : Char = '\127'; %(slash_o177)%

'\o200' : Char = '\128'; %(slash_o200)%

'\o201' : Char = '\129'; %(slash_o201)%

'\o202' : Char = '\130'; %(slash_o202)%

'\o203' : Char = '\131'; %(slash_o203)%

'\o204' : Char = '\132'; %(slash_o204)%

'\o205' : Char = '\133'; %(slash_o205)%

'\o206' : Char = '\134'; %(slash_o206)%

'\o207' : Char = '\135'; %(slash_o207)%

'\o210' : Char = '\136'; %(slash_o210)%

'\o211' : Char = '\137'; %(slash_o211)%

'\o212' : Char = '\138'; %(slash_o212)%

'\o213' : Char = '\139'; %(slash_o213)%

'\o214' : Char = '\140'; %(slash_o214)%

'\o215' : Char = '\141'; %(slash_o215)%

'\o216' : Char = '\142'; %(slash_o216)%

'\o217' : Char = '\143'; %(slash_o217)%

'\o220' : Char = '\144'; %(slash_o220)%

'\o221' : Char = '\145'; %(slash_o221)%

'\o222' : Char = '\146'; %(slash_o222)%

'\o223' : Char = '\147'; %(slash_o223)%

'\o224' : Char = '\148'; %(slash_o224)%

'\o225' : Char = '\149'; %(slash_o225)%

'\o226' : Char = '\150'; %(slash_o226)%

'\o227' : Char = '\151'; %(slash_o227)%

'\o230' : Char = '\152'; %(slash_o230)%

'\o231' : Char = '\153'; %(slash_o231)%

'\o232' : Char = '\154'; %(slash_o232)%

'\o233' : Char = '\155'; %(slash_o233)%

'\o234' : Char = '\156'; %(slash_o234)%

'\o235' : Char = '\157'; %(slash_o235)%

'\o236' : Char = '\158'; %(slash_o236)%

'\o237' : Char = '\159'; %(slash_o237)%

'\o240' : Char = '\160'; %(slash_o240)%

'\o241' : Char = '\161'; %(slash_o241)%

'\o242' : Char = '\162'; %(slash_o242)%

'\o243' : Char = '\163'; %(slash_o243)%

'\o244' : Char = '\164'; %(slash_o244)%

'\o245' : Char = '\165'; %(slash_o245)%

'\o246' : Char = '\166'; %(slash_o246)%

'\o247' : Char = '\167'; %(slash_o247)%

'\o250' : Char = '\168'; %(slash_o250)%

'\o251' : Char = '\169'; %(slash_o251)%

'\o252' : Char = '\170'; %(slash_o252)%

'\o253' : Char = '\171'; %(slash_o253)%

'\o254' : Char = '\172'; %(slash_o254)%

'\o255' : Char = '\173'; %(slash_o255)%

'\o256' : Char = '\174'; %(slash_o256)%

'\o257' : Char = '\175'; %(slash_o257)%

'\o260' : Char = '\176'; %(slash_o260)%

'\o261' : Char = '\177'; %(slash_o261)%

'\o262' : Char = '\178'; %(slash_o262)%

'\o263' : Char = '\179'; %(slash_o263)%

'\o264' : Char = '\180'; %(slash_o264)%

'\o265' : Char = '\181'; %(slash_o265)%

'\o266' : Char = '\182'; %(slash_o266)%

'\o267' : Char = '\183'; %(slash_o267)%

'\o270' : Char = '\184'; %(slash_o270)%

'\o271' : Char = '\185'; %(slash_o271)%

'\o272' : Char = '\186'; %(slash_o272)%

'\o273' : Char = '\187'; %(slash_o273)%

'\o274' : Char = '\188'; %(slash_o274)%

'\o275' : Char = '\189'; %(slash_o275)%

'\o276' : Char = '\190'; %(slash_o276)%

'\o277' : Char = '\191'; %(slash_o277)%

'\o300' : Char = '\192'; %(slash_o300)%

'\o301' : Char = '\193'; %(slash_o301)%

'\o302' : Char = '\194'; %(slash_o302)%

'\o303' : Char = '\195'; %(slash_o303)%

'\o304' : Char = '\196'; %(slash_o304)%

'\o305' : Char = '\197'; %(slash_o305)%

'\o306' : Char = '\198'; %(slash_o306)%

'\o307' : Char = '\199'; %(slash_o307)%

'\o310' : Char = '\200'; %(slash_o310)%

'\o311' : Char = '\201'; %(slash_o311)%

'\o312' : Char = '\202'; %(slash_o312)%

'\o313' : Char = '\203'; %(slash_o313)%

'\o314' : Char = '\204'; %(slash_o314)%

'\o315' : Char = '\205'; %(slash_o315)%

'\o316' : Char = '\206'; %(slash_o316)%

'\o317' : Char = '\207'; %(slash_o317)%

'\o320' : Char = '\208'; %(slash_o320)%

'\o321' : Char = '\209'; %(slash_o321)%

'\o322' : Char = '\210'; %(slash_o322)%

'\o323' : Char = '\211'; %(slash_o323)%

'\o324' : Char = '\212'; %(slash_o324)%

'\o325' : Char = '\213'; %(slash_o325)%

'\o326' : Char = '\214'; %(slash_o326)%

'\o327' : Char = '\215'; %(slash_o327)%

'\o330' : Char = '\216'; %(slash_o330)%

'\o331' : Char = '\217'; %(slash_o331)%

'\o332' : Char = '\218'; %(slash_o332)%

'\o333' : Char = '\219'; %(slash_o333)%

'\o334' : Char = '\220'; %(slash_o334)%

'\o335' : Char = '\221'; %(slash_o335)%

'\o336' : Char = '\222'; %(slash_o336)%

'\o337' : Char = '\223'; %(slash_o337)%

'\o340' : Char = '\224'; %(slash_o340)%

'\o341' : Char = '\225'; %(slash_o341)%

'\o342' : Char = '\226'; %(slash_o342)%

'\o343' : Char = '\227'; %(slash_o343)%

'\o344' : Char = '\228'; %(slash_o344)%

'\o345' : Char = '\229'; %(slash_o345)%

'\o346' : Char = '\230'; %(slash_o346)%

'\o347' : Char = '\231'; %(slash_o347)%

'\o350' : Char = '\232'; %(slash_o350)%

'\o351' : Char = '\233'; %(slash_o351)%

'\o352' : Char = '\234'; %(slash_o352)%

'\o353' : Char = '\235'; %(slash_o353)%

'\o354' : Char = '\236'; %(slash_o354)%

'\o355' : Char = '\237'; %(slash_o355)%

'\o356' : Char = '\238'; %(slash_o356)%

'\o357' : Char = '\239'; %(slash_o357)%

'\o360' : Char = '\240'; %(slash_o360)%

'\o361' : Char = '\241'; %(slash_o361)%

'\o362' : Char = '\242'; %(slash_o362)%

'\o363' : Char = '\243'; %(slash_o363)%

'\o364' : Char = '\244'; %(slash_o364)%

'\o365' : Char = '\245'; %(slash_o365)%

'\o366' : Char = '\246'; %(slash_o366)%

'\o367' : Char = '\247'; %(slash_o367)%

'\o370' : Char = '\248'; %(slash_o370)%

'\o371' : Char = '\249'; %(slash_o371)%

'\o372' : Char = '\250'; %(slash_o372)%

'\o373' : Char = '\251'; %(slash_o373)%

'\o374' : Char = '\252'; %(slash_o374)%

'\o375' : Char = '\253'; %(slash_o375)%

'\o376' : Char = '\254'; %(slash_o376)%

'\o377' : Char = '\255'; %(slash_o377)%

%% alternative definition of characters as '\xhh',

%% where h in {0,1,..., F} :

ops

'\x00' : Char = '\000'; %(slash_x00)%

'\x01' : Char = '\001'; %(slash_x01)%

'\x02' : Char = '\002'; %(slash_x02)%

'\x03' : Char = '\003'; %(slash_x03)%

'\x04' : Char = '\004'; %(slash_x04)%

'\x05' : Char = '\005'; %(slash_x05)%

'\x06' : Char = '\006'; %(slash_x06)%

'\x07' : Char = '\007'; %(slash_x07)%

'\x08' : Char = '\008'; %(slash_x08)%

'\x09' : Char = '\009'; %(slash_x09)%

'\x0A' : Char = '\010'; %(slash_x0A)%

'\x0B' : Char = '\011'; %(slash_x0B)%

'\x0C' : Char = '\012'; %(slash_x0C)%

'\x0D' : Char = '\013'; %(slash_x0D)%

'\x0E' : Char = '\014'; %(slash_x0E)%

'\x0F' : Char = '\015'; %(slash_x0F)%

'\x10' : Char = '\016'; %(slash_x10)%

'\x11' : Char = '\017'; %(slash_x11)%

'\x12' : Char = '\018'; %(slash_x12)%

'\x13' : Char = '\019'; %(slash_x13)%

'\x14' : Char = '\020'; %(slash_x14)%

'\x15' : Char = '\021'; %(slash_x15)%

'\x16' : Char = '\022'; %(slash_x16)%

'\x17' : Char = '\023'; %(slash_x17)%

'\x18' : Char = '\024'; %(slash_x18)%

'\x19' : Char = '\025'; %(slash_x19)%

'\x1A' : Char = '\026'; %(slash_x1A)%

'\x1B' : Char = '\027'; %(slash_x1B)%

'\x1C' : Char = '\028'; %(slash_x1C)%

'\x1D' : Char = '\029'; %(slash_x1D)%

'\x1E' : Char = '\030'; %(slash_x1E)%

'\x1F' : Char = '\031'; %(slash_x1F)%

'\x20' : Char = '\032'; %(slash_x20)%

'\x21' : Char = '\033'; %(slash_x21)%

'\x22' : Char = '\034'; %(slash_x22)%

'\x23' : Char = '\035'; %(slash_x23)%

'\x24' : Char = '\036'; %(slash_x24)%

'\x25' : Char = '\037'; %(slash_x25)%

'\x26' : Char = '\038'; %(slash_x26)%

'\x27' : Char = '\039'; %(slash_x27)%

'\x28' : Char = '\040'; %(slash_x28)%

'\x29' : Char = '\041'; %(slash_x29)%

'\x2A' : Char = '\042'; %(slash_x2A)%

'\x2B' : Char = '\043'; %(slash_x2B)%

'\x2C' : Char = '\044'; %(slash_x2C)%

'\x2D' : Char = '\045'; %(slash_x2D)%

'\x2E' : Char = '\046'; %(slash_x2E)%

'\x2F' : Char = '\047'; %(slash_x2F)%

'\x30' : Char = '\048'; %(slash_x30)%

'\x31' : Char = '\049'; %(slash_x31)%

'\x32' : Char = '\050'; %(slash_x32)%

'\x33' : Char = '\051'; %(slash_x33)%

'\x34' : Char = '\052'; %(slash_x34)%

'\x35' : Char = '\053'; %(slash_x35)%

'\x36' : Char = '\054'; %(slash_x36)%

'\x37' : Char = '\055'; %(slash_x37)%

'\x38' : Char = '\056'; %(slash_x38)%

'\x39' : Char = '\057'; %(slash_x39)%

'\x3A' : Char = '\058'; %(slash_x3A)%

'\x3B' : Char = '\059'; %(slash_x3B)%

'\x3C' : Char = '\060'; %(slash_x3C)%

'\x3D' : Char = '\061'; %(slash_x3D)%

'\x3E' : Char = '\062'; %(slash_x3E)%

'\x3F' : Char = '\063'; %(slash_x3F)%

'\x40' : Char = '\064'; %(slash_x40)%

'\x41' : Char = '\065'; %(slash_x41)%

'\x42' : Char = '\066'; %(slash_x42)%

'\x43' : Char = '\067'; %(slash_x43)%

'\x44' : Char = '\068'; %(slash_x44)%

'\x45' : Char = '\069'; %(slash_x45)%

'\x46' : Char = '\070'; %(slash_x46)%

'\x47' : Char = '\071'; %(slash_x47)%

'\x48' : Char = '\072'; %(slash_x48)%

'\x49' : Char = '\073'; %(slash_x49)%

'\x4A' : Char = '\074'; %(slash_x4A)%

'\x4B' : Char = '\075'; %(slash_x4B)%

'\x4C' : Char = '\076'; %(slash_x4C)%

'\x4D' : Char = '\077'; %(slash_x4D)%

'\x4E' : Char = '\078'; %(slash_x4E)%

'\x4F' : Char = '\079'; %(slash_x4F)%

'\x50' : Char = '\080'; %(slash_x50)%

'\x51' : Char = '\081'; %(slash_x51)%

'\x52' : Char = '\082'; %(slash_x52)%

'\x53' : Char = '\083'; %(slash_x53)%

'\x54' : Char = '\084'; %(slash_x54)%

'\x55' : Char = '\085'; %(slash_x55)%

'\x56' : Char = '\086'; %(slash_x56)%

'\x57' : Char = '\087'; %(slash_x57)%

'\x58' : Char = '\088'; %(slash_x58)%

'\x59' : Char = '\089'; %(slash_x59)%

'\x5A' : Char = '\090'; %(slash_x5A)%

'\x5B' : Char = '\091'; %(slash_x5B)%

'\x5C' : Char = '\092'; %(slash_x5C)%

'\x5D' : Char = '\093'; %(slash_x5D)%

'\x5E' : Char = '\094'; %(slash_x5E)%

'\x5F' : Char = '\095'; %(slash_x5F)%

'\x60' : Char = '\096'; %(slash_x60)%

'\x61' : Char = '\097'; %(slash_x61)%

'\x62' : Char = '\098'; %(slash_x62)%

'\x63' : Char = '\099'; %(slash_x63)%

'\x64' : Char = '\100'; %(slash_x64)%

'\x65' : Char = '\101'; %(slash_x65)%

'\x66' : Char = '\102'; %(slash_x66)%

'\x67' : Char = '\103'; %(slash_x67)%

'\x68' : Char = '\104'; %(slash_x68)%

'\x69' : Char = '\105'; %(slash_x69)%

'\x6A' : Char = '\106'; %(slash_x6A)%

'\x6B' : Char = '\107'; %(slash_x6B)%

'\x6C' : Char = '\108'; %(slash_x6C)%

'\x6D' : Char = '\109'; %(slash_x6D)%

'\x6E' : Char = '\110'; %(slash_x6E)%

'\x6F' : Char = '\111'; %(slash_x6F)%

'\x70' : Char = '\112'; %(slash_x70)%

'\x71' : Char = '\113'; %(slash_x71)%

'\x72' : Char = '\114'; %(slash_x72)%

'\x73' : Char = '\115'; %(slash_x73)%

'\x74' : Char = '\116'; %(slash_x74)%

'\x75' : Char = '\117'; %(slash_x75)%

'\x76' : Char = '\118'; %(slash_x76)%

'\x77' : Char = '\119'; %(slash_x77)%

'\x78' : Char = '\120'; %(slash_x78)%

'\x79' : Char = '\121'; %(slash_x79)%

'\x7A' : Char = '\122'; %(slash_x7A)%

'\x7B' : Char = '\123'; %(slash_x7B)%

'\x7C' : Char = '\124'; %(slash_x7C)%

'\x7D' : Char = '\125'; %(slash_x7D)%

'\x7E' : Char = '\126'; %(slash_x7E)%

'\x7F' : Char = '\127'; %(slash_x7F)%

'\x80' : Char = '\128'; %(slash_x80)%

'\x81' : Char = '\129'; %(slash_x81)%

'\x82' : Char = '\130'; %(slash_x82)%

'\x83' : Char = '\131'; %(slash_x83)%

'\x84' : Char = '\132'; %(slash_x84)%

'\x85' : Char = '\133'; %(slash_x85)%

'\x86' : Char = '\134'; %(slash_x86)%

'\x87' : Char = '\135'; %(slash_x87)%

'\x88' : Char = '\136'; %(slash_x88)%

'\x89' : Char = '\137'; %(slash_x89)%

'\x8A' : Char = '\138'; %(slash_x8A)%

'\x8B' : Char = '\139'; %(slash_x8B)%

'\x8C' : Char = '\140'; %(slash_x8C)%

'\x8D' : Char = '\141'; %(slash_x8D)%

'\x8E' : Char = '\142'; %(slash_x8E)%

'\x8F' : Char = '\143'; %(slash_x8F)%

'\x90' : Char = '\144'; %(slash_x90)%

'\x91' : Char = '\145'; %(slash_x91)%

'\x92' : Char = '\146'; %(slash_x92)%

'\x93' : Char = '\147'; %(slash_x93)%

'\x94' : Char = '\148'; %(slash_x94)%

'\x95' : Char = '\149'; %(slash_x95)%

'\x96' : Char = '\150'; %(slash_x96)%

'\x97' : Char = '\151'; %(slash_x97)%

'\x98' : Char = '\152'; %(slash_x98)%

'\x99' : Char = '\153'; %(slash_x99)%

'\x9A' : Char = '\154'; %(slash_x9A)%

'\x9B' : Char = '\155'; %(slash_x9B)%

'\x9C' : Char = '\156'; %(slash_x9C)%

'\x9D' : Char = '\157'; %(slash_x9D)%

'\x9E' : Char = '\158'; %(slash_x9E)%

'\x9F' : Char = '\159'; %(slash_x9F)%

'\xA0' : Char = '\160'; %(slash_xA0)%

'\xA1' : Char = '\161'; %(slash_xA1)%

'\xA2' : Char = '\162'; %(slash_xA2)%

'\xA3' : Char = '\163'; %(slash_xA3)%

'\xA4' : Char = '\164'; %(slash_xA4)%

'\xA5' : Char = '\165'; %(slash_xA5)%

'\xA6' : Char = '\166'; %(slash_xA6)%

'\xA7' : Char = '\167'; %(slash_xA7)%

'\xA8' : Char = '\168'; %(slash_xA8)%

'\xA9' : Char = '\169'; %(slash_xA9)%

'\xAA' : Char = '\170'; %(slash_xAA)%

'\xAB' : Char = '\171'; %(slash_xAB)%

'\xAC' : Char = '\172'; %(slash_xAC)%

'\xAD' : Char = '\173'; %(slash_xAD)%

'\xAE' : Char = '\174'; %(slash_xAE)%

'\xAF' : Char = '\175'; %(slash_xAF)%

'\xB0' : Char = '\176'; %(slash_xB0)%

'\xB1' : Char = '\177'; %(slash_xB1)%

'\xB2' : Char = '\178'; %(slash_xB2)%

'\xB3' : Char = '\179'; %(slash_xB3)%

'\xB4' : Char = '\180'; %(slash_xB4)%

'\xB5' : Char = '\181'; %(slash_xB5)%

'\xB6' : Char = '\182'; %(slash_xB6)%

'\xB7' : Char = '\183'; %(slash_xB7)%

'\xB8' : Char = '\184'; %(slash_xB8)%

'\xB9' : Char = '\185'; %(slash_xB9)%

'\xBA' : Char = '\186'; %(slash_xBA)%

'\xBB' : Char = '\187'; %(slash_xBB)%

'\xBC' : Char = '\188'; %(slash_xBC)%

'\xBD' : Char = '\189'; %(slash_xBD)%

'\xBE' : Char = '\190'; %(slash_xBE)%

'\xBF' : Char = '\191'; %(slash_xBF)%

'\xC0' : Char = '\192'; %(slash_xC0)%

'\xC1' : Char = '\193'; %(slash_xC1)%

'\xC2' : Char = '\194'; %(slash_xC2)%

'\xC3' : Char = '\195'; %(slash_xC3)%

'\xC4' : Char = '\196'; %(slash_xC4)%

'\xC5' : Char = '\197'; %(slash_xC5)%

'\xC6' : Char = '\198'; %(slash_xC6)%

'\xC7' : Char = '\199'; %(slash_xC7)%

'\xC8' : Char = '\200'; %(slash_xC8)%

'\xC9' : Char = '\201'; %(slash_xC9)%

'\xCA' : Char = '\202'; %(slash_xCA)%

'\xCB' : Char = '\203'; %(slash_xCB)%

'\xCC' : Char = '\204'; %(slash_xCC)%

'\xCD' : Char = '\205'; %(slash_xCD)%

'\xCE' : Char = '\206'; %(slash_xCE)%

'\xCF' : Char = '\207'; %(slash_xCF)%

'\xD0' : Char = '\208'; %(slash_xD0)%

'\xD1' : Char = '\209'; %(slash_xD1)%

'\xD2' : Char = '\210'; %(slash_xD2)%

'\xD3' : Char = '\211'; %(slash_xD3)%

'\xD4' : Char = '\212'; %(slash_xD4)%

'\xD5' : Char = '\213'; %(slash_xD5)%

'\xD6' : Char = '\214'; %(slash_xD6)%

'\xD7' : Char = '\215'; %(slash_xD7)%

'\xD8' : Char = '\216'; %(slash_xD8)%

'\xD9' : Char = '\217'; %(slash_xD9)%

'\xDA' : Char = '\218'; %(slash_xDA)%

'\xDB' : Char = '\219'; %(slash_xDB)%

'\xDC' : Char = '\220'; %(slash_xDC)%

'\xDD' : Char = '\221'; %(slash_xDD)%

'\xDE' : Char = '\222'; %(slash_xDE)%

'\xDF' : Char = '\223'; %(slash_xDF)%

'\xE0' : Char = '\224'; %(slash_xE0)%

'\xE1' : Char = '\225'; %(slash_xE1)%

'\xE2' : Char = '\226'; %(slash_xE2)%

'\xE3' : Char = '\227'; %(slash_xE3)%

'\xE4' : Char = '\228'; %(slash_xE4)%

'\xE5' : Char = '\229'; %(slash_xE5)%

'\xE6' : Char = '\230'; %(slash_xE6)%

'\xE7' : Char = '\231'; %(slash_xE7)%

'\xE8' : Char = '\232'; %(slash_xE8)%

'\xE9' : Char = '\233'; %(slash_xE9)%

'\xEA' : Char = '\234'; %(slash_xEA)%

'\xEB' : Char = '\235'; %(slash_xEB)%

'\xEC' : Char = '\236'; %(slash_xEC)%

'\xED' : Char = '\237'; %(slash_xED)%

'\xEE' : Char = '\238'; %(slash_xEE)%

'\xEF' : Char = '\239'; %(slash_xEF)%

'\xF0' : Char = '\240'; %(slash_xF0)%

'\xF1' : Char = '\241'; %(slash_xF1)%

'\xF2' : Char = '\242'; %(slash_xF2)%

'\xF3' : Char = '\243'; %(slash_xF3)%

'\xF4' : Char = '\244'; %(slash_xF4)%

'\xF5' : Char = '\245'; %(slash_xF5)%

'\xF6' : Char = '\246'; %(slash_xF6)%

'\xF7' : Char = '\247'; %(slash_xF7)%

'\xF8' : Char = '\248'; %(slash_xF8)%

'\xF9' : Char = '\249'; %(slash_xF9)%

'\xFA' : Char = '\250'; %(slash_xFA)%

'\xFB' : Char = '\251'; %(slash_xFB)%

'\xFC' : Char = '\252'; %(slash_xFC)%

'\xFD' : Char = '\253'; %(slash_xFD)%

'\xFE' : Char = '\254'; %(slash_xFE)%

'\xFF' : Char = '\255'; %(slash_xFF)%

%% special characters:

ops NUL:Char = '\000'; %(NUL_def)%

SOH:Char = '\001'; %(SOH_def)%

SYX:Char = '\002'; %(SYX_def)%

ETX:Char = '\003'; %(ETX_def)%

EOT:Char = '\004'; %(EOT_def)%

ENQ:Char = '\005'; %(ENQ_def)%

ACK:Char = '\006'; %(ACK_def)%

BEL:Char = '\007'; %(BEL_def)%

BS:Char = '\008'; %(BS_def)%

HT:Char = '\009'; %(HT_def)%

LF:Char = '\010'; %(LF_def)%

VT:Char = '\011'; %(VT_def)%

FF:Char = '\012'; %(FF_def)%

CR:Char = '\013'; %(CR_def)%

SO:Char = '\014'; %(SO_def)%

SI:Char = '\015'; %(SI_def)%

DLE:Char = '\016'; %(DLE_def)%

DC1:Char = '\017'; %(DC1_def)%

DC2:Char = '\018'; %(DC2_def)%

DC3:Char = '\019'; %(DC3_def)%

DC4:Char = '\020'; %(DC4_def)%

NAK:Char = '\021'; %(NAK_def)%

SYN:Char = '\022'; %(SYN_def)%

ETB:Char = '\023'; %(ETB_def)%

CAN:Char = '\024'; %(CAN_def)%

EM:Char = '\025'; %(EM_def)%

SUB:Char = '\026'; %(SUB_def)%

ESC:Char = '\027'; %(ESC_def)%

FS:Char = '\028'; %(FS_def)%

GS:Char = '\029'; %(GS_def)%

RS:Char = '\030'; %(RS_def)%

US:Char = '\031'; %(US_def)%

SP:Char = '\032'; %(SP_def)%

DEL:Char = '\127'; %(DEL_def)%

%% alternative names for special charcters:

ops NL:Char = LF; %(NL_def)%

NP:Char = FF; %(NP_def)%

%% character constants:

ops '\n' : Char = NL; %(slash_n)%

'\t' : Char = HT; %(slash_t)%

'\v' : Char = VT; %(slash_v)%

'\b' : Char = BS; %(slash_b)%

'\r' : Char = CR; %(slash_r)%

'\f' : Char = FF; %(slash_f)%

'\a' : Char = BEL; %(slash_a)%

'\?' : Char = '?'; %(slash_quest)%

sort a;

ops __||__ : a * a -> a, assoc

op b : a

. b || b || b = b