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}

ops 1 : Pos; %(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

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

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

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 / p) * (q / j) if not j = 0

%(Rat_divide_rule)%

pred __<__ : a * a

ops __a : b;

c : b

sorts s, t < s

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

. a = a

. a = a

. a = a

. a = a

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

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

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

generated

{pred __<__ : a * a

ops a : b;

c : b

sorts s, t < s

type s ::= sorts s2, s1

| c

| c(a)

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

| c(a)? %(bla1)%}

%(sort)%

sorts %(after-sort)%

s; %(bla2)%

t

%(op)%

ops 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)%

%(formula)%

sort s

sorts s, abcdefghijlklmnopqrstuvwxyz, ABCDEFGHIJKLMONOPQRSTUVWXYZ,

x0123456789,

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

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

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

ops 1, 2, 3, 4 : s;

- : s -> s;

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

. 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

sort 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

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

sorts s, t

pred a : ()

pred b : s

preds c : s * s;

c : s * s * s

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}

sort 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)

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 : ())

. (pred q : s)(x)

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

. def {}

. def { x }

. true

forall x: s

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

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

op b : a

. (b || b) || b = b

*** Hint 17.9, redeclared as total 'min'

*** Hint 17.14, redeclared as total 'max'

*** Error 90.19, no typing for: suc(0): Pos

*** Hint 98.10, redeclared op 'min'

*** Hint 98.15, redeclared op 'max'

*** Hint 121.18, redeclared sort 'Int'

*** Hint 121.12, redeclared sort 'Nat'

*** Hint 209.17, redeclared sort 'Rat'

*** Hint 209.11, redeclared sort 'Int'

*** Error 261.9-261.21, ambiguous mixfix term

__*__(i, __-__(q, __*__(j, p)))

__-__(__*__(i, q), __*__(j, p))

__*__(__*__(i, __-__(q, j)), p)

*** Error 266.16, unknown sort 'a'

*** Error 266.20, unknown sort 'a'

*** Error 268.9, unknown sort 'b'

*** Error 268.6, wrong number of places '__a'

*** Error 268.15, unknown sort 'b'

*** Hint 269.6, redeclared sort 's'

*** Warning 269.6, void reflexive subsort 's'

*** Error 270.3, no operation with 0 arguments found for 'a'

*** Warning 271.11, known variable shadowed 'a'

*** Warning 272.6, known variable shadowed 'a'

*** Warning 272.11, known variable shadowed 'a'

*** Warning 272.13, known variable shadowed 'b'

*** Warning 275.8, known variable shadowed 'a'

*** Warning 275.13, known variable shadowed 'a'

*** Warning 275.15, known variable shadowed 'b'

*** Hint 285.6, redeclared sort 's'

*** Error 285.17, unknown sort 's2'

*** Error 285.20, unknown sort 's1'

*** Error 285.31, unknown sort 'a'

*** Warning 285.34, also known as variable 'a'

*** Warning 285.36, also known as variable 'b'

*** Hint 285.41, redeclared op 'a'

*** Error 285.34, duplicates at '(285,41)' for 'a : s -> t'

*** Error 285.52, unknown sort 'a'

*** Error 285.25, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 285.50, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Hint 286.11, redeclared sort 's'

*** Error 286.22, unknown sort 's2'

*** Hint 286.22, redeclared subsort 's2 < s'

*** Error 286.25, unknown sort 's1'

*** Hint 286.25, redeclared subsort 's1 < s'

*** Hint 286.30, redeclared op 'c'

*** Error 286.36, unknown sort 'a'

*** Hint 286.39, redeclared op 'a'

*** Hint 286.41, redeclared op 'b'

*** Hint 286.46, redeclared op 'd'

*** Error 286.55, unknown sort 'a'

*** Hint 286.53, redeclared op 'c'

*** Error 286.30, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 286.53, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Hint 287.16, redeclared sort 's'

*** Error 287.27, unknown sort 's2'

*** Hint 287.27, redeclared subsort 's2 < s'

*** Error 287.30, unknown sort 's1'

*** Hint 287.30, redeclared subsort 's1 < s'

*** Hint 287.35, redeclared op 'c'

*** Error 287.41, unknown sort 'a'

*** Hint 287.39, redeclared op 'c'

*** Hint 287.44, redeclared op 'a'

*** Hint 287.46, redeclared op 'b'

*** Hint 287.51, redeclared op 'd'

*** Error 287.60, unknown sort 'a'

*** Hint 287.58, redeclared op 'c'

*** Error 287.35, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 287.58, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Error 290.16, unknown sort 'a'

*** Error 290.20, unknown sort 'a'

*** Hint 290.9, redeclared pred '__<__'

*** Error 292.7, unknown sort 'b'

*** Warning 292.4, also known as variable 'a'

*** Error 292.13, unknown sort 'b'

*** Hint 292.10, redeclared op 'c'

*** Hint 293.13, redeclared sort 's'

*** Hint 293.6, redeclared sort 's'

*** Hint 293.9, redeclared sort 't'

*** Warning 293.6, void reflexive subsort 's'

*** Hint 293.9, redeclared subsort 't < s'

*** Hint 294.6, redeclared sort 's'

*** Error 294.17, unknown sort 's2'

*** Hint 294.17, redeclared subsort 's2 < s'

*** Error 294.20, unknown sort 's1'

*** Hint 294.20, redeclared subsort 's1 < s'

*** Hint 294.25, redeclared op 'c'

*** Error 294.31, unknown sort 'a'

*** Hint 294.29, redeclared as total 'c'

*** Error 294.38, unknown sort 'a'

*** Hint 294.36, redeclared op 'c'

*** Hint 294.41, redeclared op 'a'

*** Hint 294.43, redeclared op 'b'

*** Hint 294.48, redeclared op 'd'

*** Error 294.57, unknown sort 'a'

*** Warning 294.55, partially redeclared 'c'

*** Error 294.29, duplicates at '(294,55)' for 'c : a -> s'

*** Error 294.25, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 294.29, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a -> s'

*** Error 294.55, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Hint 300.6, redeclared sort 's'

*** Hint 301.6, redeclared sort 't'

*** Error 304.6, unknown sort 'b'

*** Hint 304.4, redeclared op 'a'

*** Error 305.6, unknown sort 'd'

*** Warning 308.6, known variable shadowed 'a'

*** Warning 308.6, also known as operation 'a'

*** Warning 309.9, known variable shadowed 'a'

*** Warning 309.9, also known as operation 'a'

*** Warning 309.11, known variable shadowed 'b'

*** Warning 309.11, also known as operation 'b'

*** Hint 312.6, redeclared sort 't'

*** Error 316.3, ambiguous term

. (op a : b) = (op a : b)

. (var a : s) = (var a : s)

*** Error 317.3, ambiguous term

. (op a : b) = (op a : b)

. (var a : s) = (var a : s)

*** Error 320.5, ambiguous term

. (op a : b) = (op a : b)

. (var a : s) = (var a : s)

*** Error 321.5, ambiguous term

. (op a : b) = (op a : b)

. (var a : s) = (var a : s)

*** Hint 323.6, redeclared sort 's'

*** Hint 325.9, redeclared sort 's'

*** Hint 336.47, redeclared op ''\\''

*** Error, ambiguous term

(op __@@__ : Nat * Nat -> Nat)((op 1 : Pos), (op 2 : Nat))

(op __@@__ : s * s -> s)((op 1 : s), (op 2 : s))

*** Error 342.20, no operation with 2 arguments found for '__E__'

*** Error 342.32, no operation with 2 arguments found for '__E__'

*** Error 342.45, no operation with 2 arguments found for '__:::__'

*** Error 343.14, no operation with 2 arguments found for '__E__'

*** Error 343.29, no operation with 2 arguments found for '__E__'

*** Error 343.45, no operation with 2 arguments found for '__E__'

*** Hint 350.11, redeclared sort 's'

*** Error 351.11, wrong number of places '__and'__'

*** Hint 353.12, redeclared sort 'a'

*** Hint 354.13, redeclared sort 'b'

*** Hint 354.11, redeclared sort 'a'

*** Hint 355.12, redeclared sort 'a'

*** Hint 355.14, redeclared sort 'b'

*** Hint 355.16, redeclared sort 'c'

*** Hint 356.12, redeclared sort 'a'

*** Hint 356.14, redeclared sort 'b'

*** Hint 356.16, redeclared sort 'c'

*** Hint 356.18, redeclared sort 'd'

*** Hint 356.20, redeclared sort 'e'

*** Warning 356.12, subsort 'a' made isomorphic by 'a = b'

*** Warning 356.18, subsort 'd' made isomorphic by 'd = e'

*** Hint 357.11, redeclared sort 'a'

*** Warning 357.11, sorts are isomorphic 'a < b'

*** Hint 358.12, redeclared sort 's'

*** Hint 358.14, redeclared sort 't'

*** Warning 359.9, also known as variable 'a'

*** Warning 360.9, also known as variable 'b'

*** Warning 363.9, partially redeclared 'a'

*** Warning 364.9, partially redeclared 'b'

*** Warning 365.9, partially redeclared 'c'

*** Warning 366.9, partially redeclared 'c'

*** Hint 367.9, redeclared op 'a'

*** Warning 369.9, partially redeclared 'a'

*** Warning 370.9, partially redeclared 'c'

*** Hint 373.12, redeclared sort 's'

*** Hint 373.14, redeclared sort 't'

*** Warning 374.11, also known as operation 'a'

*** Warning 374.11, also known as variable 'a'

*** Warning 375.11, also known as operation 'b'

*** Warning 375.11, also known as variable 'b'

*** Warning 376.12, also known as operation 'c'

*** Warning 377.12, also known as operation 'c'

*** Warning 381.11, also known as operation 'c'

*** Warning 382.21, also known as predicate 'a'

*** Warning 382.21, also known as variable 'a'

*** Warning 382.25, also known as predicate 'b'

*** Warning 382.25, also known as variable 'b'

*** Warning 382.29, also known as predicate 'c'

*** Hint 384.64, redeclared op 'sel2'

*** Hint 384.77, redeclared op 'sel1'

*** Hint 386.65, redeclared op 'sel2'

*** Hint 386.78, redeclared op 'sel1'

*** Hint 388.27, redeclared sort 'Data1'

*** Hint 388.34, redeclared sort 'Data2'

*** Hint 388.41, redeclared sort 'Data3'

*** Hint 393.22, redeclared sort 'Set'

*** Hint 393.30, redeclared op 'Mt'

*** Hint 393.35, redeclared op 'Add'

*** Hint 395.11, redeclared sort 't'

*** Hint 395.9, redeclared sort 's'

*** Warning 395.9, added subsort cycle by 's < t'

*** Warning 404.7, known variable shadowed 'x'

*** Warning 410.10, known variable shadowed 'x'

*** Error 426.26, no predicate with 0 arguments found for 'e'

*** Warning 427.8, known variable shadowed 'x'

*** Error 427.12, no predicate with 0 arguments found for 'e'

*** Warning 436.13, known variable shadowed 'x'

*** Warning 436.15, known variable shadowed 'y'

*** Warning 436.17, known variable shadowed 'z'

*** Warning 451.20, also known as operation 'c'

*** Warning 451.20, also known as predicate 'c'

*** Hint 811.11, redeclared op '' ''

*** Hint 1486.6, redeclared sort 'a'

*** Warning 1489.4, also known as predicate 'b'

*** Warning 1489.4, also known as variable 'b'