free type Nat ::= 0 |

suc (pre :? Nat)

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

odd, even : Nat

op min, max : Nat * Nat ->? Nat

op __+__, __*__ : 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 : Nat; n : Nat; r : Nat; 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

type 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

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

forall x : Nat; m : Nat; n : Nat; r : Nat; s : Nat; 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

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

forall a : Nat; b : Nat; c : Nat; d : Nat

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

%% then

type Nat < Int

forall a : Nat

. a = a - 0 %(Int_Nat_embedding)%

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

odd, even : Int

op 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 : Int; n : Int; r : Int; s : Int; a : Nat; b : Nat;

c : Nat; 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))

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

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

%% then %implies

%(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

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

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

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

type Int < Rat

forall i : Int

. i / 1 = i %(embeddingIntToRat)%

%% then

pred __<=__, __<__, __>=__, __>__ : Rat * Rat

op 0, 1 : Rat;

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

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

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

__^__ : Rat * Int -> Rat;

min, max : Rat * Rat -> Rat

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

y : Rat; 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

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

. (i / p) - (j / q) = (i * q - j * p) / (p * q) %(Rat_max_def)%

%% then %implies

%(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

type s, t < s

. a = a

var a : t; a : s; b : s

var a : t; a : s; b : s

. a = a

. a = a forall a : t; a : s; b : s . a = a

. a = a

. a = a

. a = a

. a = a

. a = a

type s ::= type s2, s1 |

c |

c (a; a : t; b : t; a : t; d : t) |

c (a)?

free type s ::= type s2, s1 |

c |

c (a; a : t; b : t; d : t) |

c (a)?

generated {type s ::= type s2, s1 |

c |

c (a; a : t; b : t; d : t) |

c (a)?}

generated {pred __<__ : a * a;

op a : b;

c : b;

type s, t < s;

type s ::= type s2, s1 |

c |

c (a) |

c (a; a : t; b : t; d : t) |

c (a)? %(bla1)%}

%(sort)%

type

%(after-sort)%

s; %(bla2)%

t

%(op)%

op a : b; %(bla4)%

c : d %(bla5)%

%(bla6)%

var a : t; a : s; b : s

%(bla8-ignored)%

%(type)%

type t ::=

%(c)%

c %(c)% |

e %(e)% |

d %(9)%

%(axiom)%

. a = a %(a1)%

. a = a %(a2)%

%(formula)%

. a = a %(f1)%

. a = a %(f1)%

type s

type s, abcdefghijlklmnopqrstuvwxyz, ABCDEFGHIJKLMONOPQRSTUVWXYZ,

x0123456789,

����������������������������������������������������������, abc,

a_b_c, ab2, ab_2_3_a, a', a'b''2

op __+-*/\&=<>!?:.$@#^~�����������������|__ : s * s -> s

%% NO-BRACKET-SIGNs

op 'a', '\"', '\\', '\n', '\000', '\255', '\x00', '\xFF', '\o000',

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

'�', '!', '�', '$', '&', '/', '(', ')', '=', '?', '\\' : s

%%characters

op 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!% )%

type s

op __and'__ : s

type a

type a, b, c

type a < b

type a, b, c, d < e

type a = b = c = d = e

type a = {x : b . true}

type s, t

op a : s

op b : s -> s

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

c : s * s * s -> s

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 : s; y : s; z : t) : s = a

op a :? s = a

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

type s, t

pred a : Unit

pred b : s

pred c : s * s;

c : s * s * s

pred c(x : s; y : s; z : t) :? Unit = false

type Data1 ::= a |

b |

c

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

Cons22 (Data2; Data1) |

type 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)?

type Data1, Data2, Data3

type 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 {type nat;

op 0 : nat;

succ : nat -> nat}

type s < t

op f, g : s ->? s;

g : s -> t;

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

{} : s;

{__} : s -> s

pred p : Unit;

q : s

var x : s; y : s; z : s; r1 : t; 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)

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)

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

. ((pred p : Unit))

. ((pred q : s)) (x)

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

. def {}

. def {x}

. true

. exists! x : s . e

forall x : s

. e

free type Boolean ::= True |

False

op Not__ : Boolean -> Boolean;

__And__, __Or__ : Boolean * Boolean -> Boolean

forall x : Boolean; y : Boolean; 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)%

type Char

op 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:

op '\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:

op ' ' : 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)%

pred isLetter(c : Char) :? Unit

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

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

%(isLetter_def)%

isDigit(c : Char) :? Unit

= ord ('0') <= ord (c) /\ ord (c) <= ord ('9'); %(isDigit_def)%

isPrintable(c : Char) :? Unit

= ((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} :

op '\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} :

op '\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:

op 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:

op NL : Char = LF; %(NL_def)%

NP : Char = FF %(NP_def)%

%% character constants:

op '\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)%

type a

op __||__ : a * a -> a, assoc

op b : a

. b || b || b = b