4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%[% [ ] % %[
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%[ ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%[ ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder free type Nat ::= 0 | suc(pre:? Nat)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder preds __ <= __, __ < __,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ >= __, __ > __: Nat * Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder odd, even: Nat
4c4a3329080becd4b81d56396586b740487924cbChristian Maeder ops min, max: Nat * Nat ->? Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops __ + __, __ * __: Nat * Nat -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ ^ __: Nat * Nat -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder min, max: Nat * Nat -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder +__: Nat -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder abs: Nat -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __! : Nat -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ -?__: Nat * Nat ->? Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ /? __: Nat * Nat ->? Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ div __, __ mod __ , __ quot __, __ rem __ :Nat * Nat ->? Nat; %()%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% Operations to represent natural numbers with digits:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 1,2,3,4,5,6,7,8,9: Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ @@ __ : Nat * Nat -> Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall m,n,r,s: Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 0 <= n %(Nat_leq_def1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not (suc(n) <= 0) %(Nat_leq_def2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . suc(m) <= suc(n) <=> m <= n %(Nat_leq_def3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m >= n <=> n <= m %(Nat_geq_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m < n <=> (m <= n /\ not (m=n)) %(Nat_less_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m > n <=> m < n %(Nat_greater_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 0 + m = m %(Nat_add_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . suc(n) + m = suc(n + m) %(Nat_add_suc)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 0 * m = 0 %(Nat_mult_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . suc(n) * m = (n * m) + m %(Nat_mult_suc)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m ^ 0 = 1 %(Nat_power_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m ^ suc(n) = m * m ^ n %(Nat_power_suc)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . min(m,n) = m when m <= n else n %(Nat_min_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . max(m,n) = n when m <= n else m %(Nat_max_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . + m = m %(plus_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . abs(n) = n %(Nat_abs)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . odd(m) <=> not even(m) %(Nat_odd_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . even(0) %(Nat_even_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . even(suc(m)) <=> odd(m) %(Nat_even_suc)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 0! = 1 %(Nat_factorial_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . suc(n)! =suc(n)*n! %(Nat_factorial_suc)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m -? n = r <=> m = r + n %(Nat_sub_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not def(m /? 0) %(Nat_divide_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . ( m /? n = r <=> m = r * n ) if n>0 %(Nat_divide_Pos)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m div n = r <=>
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (exists s: Nat . m = n*r + s /\ s < n) %(Nat_div)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m mod n = s <=>
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (exists r: Nat . m = n*r + s /\ s < n) %(Nat_mod)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m quot n = m div n %(Nat_quot)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m rem n = m mod n %(Nat_rem)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 1 = suc (0) %(Nat_1_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 2 = suc (1) %(Nat_2_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 3 = suc (2) %(Nat_3_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 4 = suc (3) %(Nat_4_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 5 = suc (4) %(Nat_5_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 6 = suc (5) %(Nat_6_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 7 = suc (6) %(Nat_7_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 8 = suc (7) %(Nat_8_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . 9 = suc (8) %(Nat_9_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m @@ n = (m * suc(9)) + n %(Nat_decimal_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% then %def
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort Pos = { p: Nat . p > 0 }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op 1: Pos = suc(0); %(Nat_1_as_Pos_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __*__: Pos * Pos -> Pos;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __+__: Pos * Nat -> Pos;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __+__: Nat * Pos -> Pos;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder suc: Nat -> Pos
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% then %implies
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops min, max: Nat * Nat -> Nat, comm, assoc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall x,m,n,r,s,t: Nat; p: Pos
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def(m-?n) <=> m >= n %(Nat_sub_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def(m /? n) <=> m mod n = 0 %(Nat_divide_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def ( m div n ) <=> not (n=0) %(Nat_div_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def ( m mod n ) <=> not (n=0) %(Nat_mod_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def ( m quot n ) <=> not (n=0) %(Nat_quot_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def ( m rem n ) <=> not (n=0) %(Nat_rem_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (r + s) * t = (r * t) + (s * t) %(Nat_distr)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . max(m,0)=m %(Nat_max_unit)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . min(m,0)=0 %(Nat_min_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% end
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%[spec Int =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederthen %def
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated type Int ::= __ - __(Nat;Nat)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall a,b,c,d: Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . a - b = c - d <=> a + d = c + b %(Int_equality)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% then
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort Nat < Int
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall a: Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . a = a - 0 %(Int_Nat_embedding)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder preds __ <= __, __ < __,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ >= __, __ > __: Int * Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder odd, even: Int
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops 0,1: Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ + __, __ - __,__ * __: Int * Int -> Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ ^ __: Int * Nat -> Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder + __, - __, sign: Int -> Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder min, max: Int * Int -> Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder abs: Int -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ /? __,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ div __, __ quot __, __ rem __ : Int * Int ->? Int;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ mod __: Int * Int ->? Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall m,n,r,s: Int; a,b,c,d: Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (a - b) + (c - d) = (a + c) - (b + d) %(Int_add_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (a - b) * (c - d) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (a * c + b * d) - (b * c + a * d) %(Int_mult_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m - n = m + ( - n ) %(Int_sub_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . + m = m %(Int_pos_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . - (a - b) = b - a %(Int_neg_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . sign(m) = 0 when m = 0
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder else (1 when m > 0 else -1) %(Int_sign_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m <= n <=> n - m in Nat %(Int_leq_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m >= n <=> n <= m %(Int_geq_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m < n <=> (m <= n /\ not (m=n)) %(Int_less_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m > n <=> m < n %(Int_greater_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . min(m,n) = m when m <= n else n %(Int_min_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . max(m,n) = n when m <= n else m %(Int_max_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . abs(m) = - m if m < 0 %(Int_abs_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (- 1) ^ a = 1 when even(a) else - 1 %(Int_neg1_power_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m ^ a = sign(m)^a * abs(m)^a %(Int_power_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . even(m) <=> even(abs(m)) %(Int_even_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . odd(m) <=> not(even(m)) %(Int_odd_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m /? n =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign(m) * sign(n) * (abs(m) /? abs(n)) %(Int_divide)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m mod n < abs(n) if not n = 0 %(Int_mod_range)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m = (m div n) * n + (m mod n) if not n = 0
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %(Int_mod__div_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not def m mod 0 %(Int_mod_zero)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not def m div 0 %(Int_div_zero)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m quot n =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign(m) * sign(n) * (abs(m) quot abs(n)) %(Int_quot_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m rem n =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sign(m) * sign(n) * (abs(m) rem abs(n)) %(Int_rem_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% then %implies
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %[ this is not legal, since -__:Nat->Int is not in the signature!
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated type Int::= Nat | -__ (Nat) ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall m,n,r: Int; a,b: Nat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def(a -? b) => a -? b = a - b %(Int_Nat_sub_compat)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m = sign(m) * abs(m) %(Int_abs_decomp)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . odd(m) <=> odd(abs(m)) %(Int_odd_alt)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m /? n = r <=> not n = 0 /\ n * r = n %(Int_divide_dom1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (m /? n) <=> m mod n = 0 %(Int_divide_dom2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (m mod n) <=> not n = 0 %(Int_mod_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m mod n = m mod abs(n) %(Int_mod_abs)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (m div n) <=> not n = 0 %(Int_div_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (m quot n) <=> not n = 0 %(Int_quot_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (m rem n) <=> not n = 0 %(Int_rem_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . m = (m quot n) * n + (m rem n) if not n = 0 %(Int_quot_rem)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% end
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%[spec Rat =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Int
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederthen %def
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated type Rat ::= __ / __ (Int;Pos)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall i,j: Int; p,q: Pos
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . i / p = j / q <=> i*q = j*p %(Rat_equality)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort Int < Rat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall i:Int
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . i / 1 = i %(embeddingIntToRat)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% then
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder preds __ <= __, __ < __,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ >= __, __ > __: Rat * Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops 0,1: Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ + __,__ - __, __ * __ : Rat * Rat -> Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ / __ : Rat * Rat ->? Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder +__, -__, abs: Rat -> Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __ ^ __: Rat * Int -> Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder min,max: Rat * Rat -> Rat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall p,q:Pos; n:Nat; i,j: Int; x,y,z: Rat
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (i / p <= j / q <=> i * q <= j * p ) %(Rat_leq_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x >= y <=> y <= x %(Rat_geq_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x < y <=> (x <= y /\ not (x=y)) %(Rat_less_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x > y <=> y < x %(Rat_greater_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (i / p) + (j / q) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (i * q + j * p) / (p * q) %(Rat_add_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x-y = x + (-y) %(Rat_sub_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (i / p) * (j / q) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (i * j) / (p * q) %(Rat_mult_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not def x/0 %(Rat_divide_def1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (x/y=z <=> z=x*y)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder if not y = 0 %(Rat_divide_def2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . + x = x %(Rat_plus_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . - (i/p) = (-i)/p %(Rat_minus_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . abs(i / p)= abs(i) / p %(Rat_abs_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x ^ 0 = 1 %(Rat_power_0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x ^ suc(n) = x * x ^ n %(Rat_power_suc)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x ^ (-p) = 1 / (x ^ p) %(Rat_power_neg)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . min(x,y) = x when x <= y else y %(Rat_min_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . max(x,y) = y when x <= y else x %(Rat_max_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% then %implies
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall i,j: Int; p,q:Pos
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (i / p) - (j / q) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (i * q - j * p) / (p * q) %(Rat_sub_rule)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (i / p) / (j / q) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (i / p) * (q / j) if not j=0 %(Rat_divide_rule)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederpred __ < __ : a * a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederop __a: b; c: b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersort s, t < s ;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedervars a:t; a,b:s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedervars a:t; a,b:s ;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederforall a:t; a,b:s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederaxioms a = a ;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera = a ;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederaxiom a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder; a = a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4c4a3329080becd4b81d56396586b740487924cbChristian Maedertype s ::= sort s2,s1 | c | c(a; a,b:t; a,d:t) | c(a)?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederfree type s ::= sort s2,s1 | c | c(a; a,b:t; d:t) | c(a)?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedergenerated type s ::= sort s2,s1 | c | c(a; a,b:t; d:t) | c(a)?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedergenerated {
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederpred __ < __ : a * a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederop a: b; c: b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersort s, t < s ;
4c4a3329080becd4b81d56396586b740487924cbChristian Maedertype s ::= sort s2,s1 | c | c(a) | c(a; a,b:t; d:t) | c(a)?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(bla1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(sort)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersort %(after-sort)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder s; %(bla2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder t
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(op)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederop a:b; %(bla4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder c:d %(bla5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(bla6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedervars a:t;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder a,b:s ; %(bla8-ignored)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(type)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype t ::= %(c)% c %(c)% | e %(e)% | d %(9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(axiom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederaxioms
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera = a; %(a1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera = a; %(a2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%(formula)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a %(f1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder. a = a ; %(f1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersort s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts s,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder abcdefghijlklmnopqrstuvwxyz,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ABCDEFGHIJKLMONOPQRSTUVWXYZ,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder x0123456789,
5a448e9be8c4482a978b174b744237757335140fChristian Maeder ÀÁÂÃÄÅÆÇÈÉÊËÌÍÎÏÑÒÓÔÕÖØÙÚÛÜÝßàáâãäåæçèéêëìíîïñòóôõöøùúûüýÿ,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder abc, a_b_c, ab2, ab_2_3_a, a', a'b''2 %[WORDS]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %[.abc, .a_b_c, .ab2, .ab_2_3_a, .a', .a'b''2, DOT-WORDS]%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder op __+-*/\&=<>!?:.$@#^~¡¿×÷£©±¶§¹²³·¢¬°|__ : s*s->s %% NO-BRACKET-SIGNs
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops 'a','"','\\','\n','\000','\255',
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x00','\xFF','\o000','\o377',
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '^','1','2','3','4','5','6','7','8','9','0',
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ß','!','§','$','&','/','(',')','=','?','\\' : s; %%characters
5a448e9be8c4482a978b174b744237757335140fChristian Maeder %[. def "^1234567890ß!§$&/()=?"; ]%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder %[ strings ´°%\\\" does not work yet!]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops 1,2,3,4 : s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder - : s->s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __@@__,__exp__,__frac__ : s*s->s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def 12 . def 12E34 . def 12E-34 . def 12.34 %%numbers
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def 12.34E34 . def 12.34E+34 . def 12.34E-34 %%fractions
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . true %(The true formula)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . true %(and this
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder also goes
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder along several lines!
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder and with special stuff: -*/\&=<>BCDEFGHIJKLM!% )%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op __and'__:s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts a,b,c;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort a<b;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts a,b,c,d < e;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts a=b=c=d=e;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort a = {x:b . true}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts s,t;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op a:s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op b:s->s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops c:s*s->s, assoc, comm, idem, unit a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder c:s*s*s->s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op a: ?s; %[ Should be: op a:?s ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op b:s->?s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op c:s*s->?s, assoc, comm, idem, unit a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op c:s*s*s->?s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op a:s=a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op c(x,y:s;z:t):s = a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op a:?s=a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op c(x,y:s;z:t):?s = a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %[op a: ?s=a;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder op c(x,y:s;z:t): ?s = a; ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts s,t;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pred a:();
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pred b:s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder preds c:s*s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder c:s*s*s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %[pred a:()<=> true;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pred c(x,y:s;z:t)<=>false;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pred a: () <=> true; ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pred c(x,y:s;z:t) <=> false;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder type Data1 ::= a | b | c;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederData1)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder?Data1)?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts Data1, Data2, Data3
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder types Tree ::= Leaf (Data1) | Forest;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Forest ::= Nil | Cons (Tree;Forest)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder free type List ::= Nil | Cons(Data1; List)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated type Set ::= Mt | Add(Data1; Set)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated {type Set ::= Mt | Add(Data1; Set)}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder generated {sort nat; ops 0:nat; succ:nat->nat; }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sorts s<t
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops f,g:s->?s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder g:s->t;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __+__,__-__,__*__,__/__ : s*s->s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {}:s;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder {__} : s->s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder preds p:(); q:s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder vars x,y,z:s; r1,r2:t
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . false
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder var x:s . true
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not p /\ not q(x) /\ q(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not p \/ not q(x) \/ q(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not p /\ not q(x) /\ q(x) => not p \/ not q(x) \/ q(x) => not p /\ not q(x) /\ q(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . not p /\ not q(x) /\ q(x) if not p \/ not q(x) \/ q(x) if not p /\ not q(x) /\ q(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %[. not p /\ not q(x) /\ q(x) <=> not p \/ not q(x) \/ q(x) <=> not p /\ not q(x) /\ q(x)]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall x:s . not p /\ not q(x) /\ q(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder <=> exists x:s . not p \/ not q(x) \/ q(x) <=> exists! x:s . not p /\ not q(x) /\ q(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def f(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . f(x) =e= g(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . f(x) = g(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . r1 in s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def g(x):t
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def g(x) as s
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (op f:s->?s)(x) %[ (var x:s) ]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def (op g:s->t)(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (pred p:())
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . (pred q:s)(x)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def x*y*z+z*y*x
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def {}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def {x}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederaxioms true ;exists! x:s.e;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederforall x:s.e
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%[spec Boolean =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder]%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder free type Boolean ::= True | False
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops Not__ : Boolean -> Boolean;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder __And__, __Or__ : Boolean * Boolean -> Boolean
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall x,y,z:Boolean
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . Not(False) = True %(Not_False)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . Not(True) = False %(Not_True)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . False And False = False %(And_def1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . False And True = False %(And_def2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . True And False = False %(And_def3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . True And True = True %(And_def4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . x Or y = Not(Not(x) And Not(y)) %(Or_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sort Char
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops chr : Nat ->? Char;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ord : Char -> Nat;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder forall n:Nat; c:Char
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . def chr(n) <=> n <= 255 %(chr_dom)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . chr(ord(c))=c %(chr_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . ord(chr(n))=n if n <= 255 %(ord_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% definition of individual characters:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops '\000' : Char = chr(0); %(slash_000)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\001' : Char = chr(1); %(slash_001)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\002' : Char = chr(2); %(slash_002)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\003' : Char = chr(3); %(slash_003)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\004' : Char = chr(4); %(slash_004)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\005' : Char = chr(5); %(slash_005)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\006' : Char = chr(6); %(slash_006)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\007' : Char = chr(7); %(slash_007)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\008' : Char = chr(8); %(slash_008)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\009' : Char = chr(9); %(slash_009)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\010' : Char = chr(10); %(slash_010)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\011' : Char = chr(11); %(slash_011)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\012' : Char = chr(12); %(slash_012)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\013' : Char = chr(13); %(slash_013)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\014' : Char = chr(14); %(slash_014)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\015' : Char = chr(15); %(slash_015)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\016' : Char = chr(16); %(slash_016)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\017' : Char = chr(17); %(slash_017)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\018' : Char = chr(18); %(slash_018)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\019' : Char = chr(19); %(slash_019)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\020' : Char = chr(20); %(slash_020)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\021' : Char = chr(21); %(slash_021)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\022' : Char = chr(22); %(slash_022)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\023' : Char = chr(23); %(slash_023)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\024' : Char = chr(24); %(slash_024)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\025' : Char = chr(25); %(slash_025)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\026' : Char = chr(26); %(slash_026)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\027' : Char = chr(27); %(slash_027)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\028' : Char = chr(28); %(slash_028)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\029' : Char = chr(29); %(slash_029)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\030' : Char = chr(30); %(slash_030)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\031' : Char = chr(31); %(slash_031)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\032' : Char = chr(32); %(slash_032)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\033' : Char = chr(33); %(slash_033)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\034' : Char = chr(34); %(slash_034)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\035' : Char = chr(35); %(slash_035)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\036' : Char = chr(36); %(slash_036)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\037' : Char = chr(37); %(slash_037)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\038' : Char = chr(38); %(slash_038)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\039' : Char = chr(39); %(slash_039)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\040' : Char = chr(40); %(slash_040)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\041' : Char = chr(41); %(slash_041)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\042' : Char = chr(42); %(slash_042)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\043' : Char = chr(43); %(slash_043)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\044' : Char = chr(44); %(slash_044)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\045' : Char = chr(45); %(slash_045)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\046' : Char = chr(46); %(slash_046)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\047' : Char = chr(47); %(slash_047)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\048' : Char = chr(48); %(slash_048)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\049' : Char = chr(49); %(slash_049)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\050' : Char = chr(50); %(slash_050)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\051' : Char = chr(51); %(slash_051)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\052' : Char = chr(52); %(slash_052)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\053' : Char = chr(53); %(slash_053)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\054' : Char = chr(54); %(slash_054)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\055' : Char = chr(55); %(slash_055)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\056' : Char = chr(56); %(slash_056)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\057' : Char = chr(57); %(slash_057)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\058' : Char = chr(58); %(slash_058)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\059' : Char = chr(59); %(slash_059)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\060' : Char = chr(60); %(slash_060)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\061' : Char = chr(61); %(slash_061)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\062' : Char = chr(62); %(slash_062)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\063' : Char = chr(63); %(slash_063)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\064' : Char = chr(64); %(slash_064)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\065' : Char = chr(65); %(slash_065)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\066' : Char = chr(66); %(slash_066)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\067' : Char = chr(67); %(slash_067)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\068' : Char = chr(68); %(slash_068)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\069' : Char = chr(69); %(slash_069)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\070' : Char = chr(70); %(slash_070)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\071' : Char = chr(71); %(slash_071)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\072' : Char = chr(72); %(slash_072)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\073' : Char = chr(73); %(slash_073)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\074' : Char = chr(74); %(slash_074)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\075' : Char = chr(75); %(slash_075)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\076' : Char = chr(76); %(slash_076)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\077' : Char = chr(77); %(slash_077)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\078' : Char = chr(78); %(slash_078)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\079' : Char = chr(79); %(slash_079)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\080' : Char = chr(80); %(slash_080)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\081' : Char = chr(81); %(slash_081)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\082' : Char = chr(82); %(slash_082)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\083' : Char = chr(83); %(slash_083)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\084' : Char = chr(84); %(slash_084)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\085' : Char = chr(85); %(slash_085)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\086' : Char = chr(86); %(slash_086)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\087' : Char = chr(87); %(slash_087)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\088' : Char = chr(88); %(slash_088)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\089' : Char = chr(89); %(slash_089)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\090' : Char = chr(90); %(slash_090)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\091' : Char = chr(91); %(slash_091)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\092' : Char = chr(92); %(slash_092)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\093' : Char = chr(93); %(slash_093)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\094' : Char = chr(94); %(slash_094)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\095' : Char = chr(95); %(slash_095)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\096' : Char = chr(96); %(slash_096)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\097' : Char = chr(97); %(slash_097)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\098' : Char = chr(98); %(slash_098)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\099' : Char = chr(99); %(slash_099)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\100' : Char = chr(100); %(slash_100)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\101' : Char = chr(101); %(slash_101)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\102' : Char = chr(102); %(slash_102)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\103' : Char = chr(103); %(slash_103)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\104' : Char = chr(104); %(slash_104)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\105' : Char = chr(105); %(slash_105)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\106' : Char = chr(106); %(slash_106)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\107' : Char = chr(107); %(slash_107)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\108' : Char = chr(108); %(slash_108)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\109' : Char = chr(109); %(slash_109)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\110' : Char = chr(110); %(slash_110)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\111' : Char = chr(111); %(slash_111)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\112' : Char = chr(112); %(slash_112)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\113' : Char = chr(113); %(slash_113)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\114' : Char = chr(114); %(slash_114)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\115' : Char = chr(115); %(slash_115)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\116' : Char = chr(116); %(slash_116)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\117' : Char = chr(117); %(slash_117)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\118' : Char = chr(118); %(slash_118)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\119' : Char = chr(119); %(slash_119)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\120' : Char = chr(120); %(slash_120)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\121' : Char = chr(121); %(slash_121)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\122' : Char = chr(122); %(slash_122)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\123' : Char = chr(123); %(slash_123)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\124' : Char = chr(124); %(slash_124)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\125' : Char = chr(125); %(slash_125)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\126' : Char = chr(126); %(slash_126)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\127' : Char = chr(127); %(slash_127)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\128' : Char = chr(128); %(slash_128)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\129' : Char = chr(129); %(slash_129)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\130' : Char = chr(130); %(slash_130)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\131' : Char = chr(131); %(slash_131)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\132' : Char = chr(132); %(slash_132)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\133' : Char = chr(133); %(slash_133)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\134' : Char = chr(134); %(slash_134)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\135' : Char = chr(135); %(slash_135)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\136' : Char = chr(136); %(slash_136)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\137' : Char = chr(137); %(slash_137)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\138' : Char = chr(138); %(slash_138)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\139' : Char = chr(139); %(slash_139)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\140' : Char = chr(140); %(slash_140)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\141' : Char = chr(141); %(slash_141)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\142' : Char = chr(142); %(slash_142)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\143' : Char = chr(143); %(slash_143)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\144' : Char = chr(144); %(slash_144)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\145' : Char = chr(145); %(slash_145)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\146' : Char = chr(146); %(slash_146)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\147' : Char = chr(147); %(slash_147)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\148' : Char = chr(148); %(slash_148)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\149' : Char = chr(149); %(slash_149)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\150' : Char = chr(150); %(slash_150)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\151' : Char = chr(151); %(slash_151)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\152' : Char = chr(152); %(slash_152)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\153' : Char = chr(153); %(slash_153)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\154' : Char = chr(154); %(slash_154)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\155' : Char = chr(155); %(slash_155)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\156' : Char = chr(156); %(slash_156)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\157' : Char = chr(157); %(slash_157)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\158' : Char = chr(158); %(slash_158)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\159' : Char = chr(159); %(slash_159)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\160' : Char = chr(160); %(slash_160)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\161' : Char = chr(161); %(slash_161)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\162' : Char = chr(162); %(slash_162)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\163' : Char = chr(163); %(slash_163)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\164' : Char = chr(164); %(slash_164)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\165' : Char = chr(165); %(slash_165)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\166' : Char = chr(166); %(slash_166)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\167' : Char = chr(167); %(slash_167)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\168' : Char = chr(168); %(slash_168)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\169' : Char = chr(169); %(slash_169)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\170' : Char = chr(170); %(slash_170)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\171' : Char = chr(171); %(slash_171)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\172' : Char = chr(172); %(slash_172)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\173' : Char = chr(173); %(slash_173)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\174' : Char = chr(174); %(slash_174)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\175' : Char = chr(175); %(slash_175)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\176' : Char = chr(176); %(slash_176)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\177' : Char = chr(177); %(slash_177)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\178' : Char = chr(178); %(slash_178)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\179' : Char = chr(179); %(slash_179)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\180' : Char = chr(180); %(slash_180)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\181' : Char = chr(181); %(slash_181)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\182' : Char = chr(182); %(slash_182)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\183' : Char = chr(183); %(slash_183)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\184' : Char = chr(184); %(slash_184)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\185' : Char = chr(185); %(slash_185)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\186' : Char = chr(186); %(slash_186)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\187' : Char = chr(187); %(slash_187)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\188' : Char = chr(188); %(slash_188)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\189' : Char = chr(189); %(slash_189)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\190' : Char = chr(190); %(slash_190)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\191' : Char = chr(191); %(slash_191)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\192' : Char = chr(192); %(slash_192)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\193' : Char = chr(193); %(slash_193)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\194' : Char = chr(194); %(slash_194)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\195' : Char = chr(195); %(slash_195)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\196' : Char = chr(196); %(slash_196)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\197' : Char = chr(197); %(slash_197)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\198' : Char = chr(198); %(slash_198)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\199' : Char = chr(199); %(slash_199)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\200' : Char = chr(200); %(slash_200)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\201' : Char = chr(201); %(slash_201)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\202' : Char = chr(202); %(slash_202)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\203' : Char = chr(203); %(slash_203)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\204' : Char = chr(204); %(slash_204)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\205' : Char = chr(205); %(slash_205)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\206' : Char = chr(206); %(slash_206)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\207' : Char = chr(207); %(slash_207)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\208' : Char = chr(208); %(slash_208)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\209' : Char = chr(209); %(slash_209)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\210' : Char = chr(210); %(slash_210)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\211' : Char = chr(211); %(slash_211)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\212' : Char = chr(212); %(slash_212)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\213' : Char = chr(213); %(slash_213)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\214' : Char = chr(214); %(slash_214)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\215' : Char = chr(215); %(slash_215)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\216' : Char = chr(216); %(slash_216)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\217' : Char = chr(217); %(slash_217)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\218' : Char = chr(218); %(slash_218)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\219' : Char = chr(219); %(slash_219)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\220' : Char = chr(220); %(slash_220)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\221' : Char = chr(221); %(slash_221)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\222' : Char = chr(222); %(slash_222)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\223' : Char = chr(223); %(slash_223)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\224' : Char = chr(224); %(slash_224)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\225' : Char = chr(225); %(slash_225)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\226' : Char = chr(226); %(slash_226)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\227' : Char = chr(227); %(slash_227)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\228' : Char = chr(228); %(slash_228)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\229' : Char = chr(229); %(slash_229)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\230' : Char = chr(230); %(slash_230)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\231' : Char = chr(231); %(slash_231)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\232' : Char = chr(232); %(slash_232)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\233' : Char = chr(233); %(slash_233)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\234' : Char = chr(234); %(slash_234)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\235' : Char = chr(235); %(slash_235)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\236' : Char = chr(236); %(slash_236)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\237' : Char = chr(237); %(slash_237)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\238' : Char = chr(238); %(slash_238)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\239' : Char = chr(239); %(slash_239)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\240' : Char = chr(240); %(slash_240)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\241' : Char = chr(241); %(slash_241)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\242' : Char = chr(242); %(slash_242)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\243' : Char = chr(243); %(slash_243)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\244' : Char = chr(244); %(slash_244)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\245' : Char = chr(245); %(slash_245)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\246' : Char = chr(246); %(slash_246)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\247' : Char = chr(247); %(slash_247)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\248' : Char = chr(248); %(slash_248)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\249' : Char = chr(249); %(slash_249)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\250' : Char = chr(250); %(slash_250)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\251' : Char = chr(251); %(slash_251)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\252' : Char = chr(252); %(slash_252)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\253' : Char = chr(253); %(slash_253)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\254' : Char = chr(254); %(slash_254)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\255' : Char = chr(255); %(slash_255)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% definition of the printable characters:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops ' ' : Char = '\032'; %(printable_32)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '!' : Char = '\033'; %(printable_33)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\"' : Char = '\034'; %(printable_34)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '#' : Char = '\035'; %(printable_35)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '$' : Char = '\036'; %(printable_36)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '%' : Char = '\037'; %(printable_37)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '&' : Char = '\038'; %(printable_38)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\'' : Char = '\039'; %(printable_39)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '(' : Char = '\040'; %(printable_40)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ')' : Char = '\041'; %(printable_41)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '*' : Char = '\042'; %(printable_42)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '+' : Char = '\043'; %(printable_43)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ',' : Char = '\044'; %(printable_44)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '-' : Char = '\045'; %(printable_45)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '.' : Char = '\046'; %(printable_46)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '/' : Char = '\047'; %(printable_47)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '0' : Char = '\048'; %(printable_48)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '1' : Char = '\049'; %(printable_49)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '2' : Char = '\050'; %(printable_50)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '3' : Char = '\051'; %(printable_51)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '4' : Char = '\052'; %(printable_52)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '5' : Char = '\053'; %(printable_53)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '6' : Char = '\054'; %(printable_54)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '7' : Char = '\055'; %(printable_55)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '8' : Char = '\056'; %(printable_56)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '9' : Char = '\057'; %(printable_57)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ':' : Char = '\058'; %(printable_58)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ';' : Char = '\059'; %(printable_59)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '<' : Char = '\060'; %(printable_60)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '=' : Char = '\061'; %(printable_61)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '>' : Char = '\062'; %(printable_62)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '?' : Char = '\063'; %(printable_63)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '@' : Char = '\064'; %(printable_64)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'A' : Char = '\065'; %(printable_65)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'B' : Char = '\066'; %(printable_66)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'C' : Char = '\067'; %(printable_67)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'D' : Char = '\068'; %(printable_68)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'E' : Char = '\069'; %(printable_69)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'F' : Char = '\070'; %(printable_70)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'G' : Char = '\071'; %(printable_71)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'H' : Char = '\072'; %(printable_72)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'I' : Char = '\073'; %(printable_73)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'J' : Char = '\074'; %(printable_74)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'K' : Char = '\075'; %(printable_75)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'L' : Char = '\076'; %(printable_76)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'M' : Char = '\077'; %(printable_77)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'N' : Char = '\078'; %(printable_78)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'O' : Char = '\079'; %(printable_79)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'P' : Char = '\080'; %(printable_80)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'Q' : Char = '\081'; %(printable_81)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'R' : Char = '\082'; %(printable_82)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'S' : Char = '\083'; %(printable_83)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'T' : Char = '\084'; %(printable_84)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'U' : Char = '\085'; %(printable_85)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'V' : Char = '\086'; %(printable_86)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'W' : Char = '\087'; %(printable_87)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'X' : Char = '\088'; %(printable_88)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'Y' : Char = '\089'; %(printable_89)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'Z' : Char = '\090'; %(printable_90)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '[' : Char = '\091'; %(printable_91)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\\' : Char = '\092'; %(printable_92)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ']' : Char = '\093'; %(printable_93)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '^' : Char = '\094'; %(printable_94)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '_' : Char = '\095'; %(printable_95)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '`' : Char = '\096'; %(printable_96)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'a' : Char = '\097'; %(printable_97)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'b' : Char = '\098'; %(printable_98)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'c' : Char = '\099'; %(printable_99)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'd' : Char = '\100' ; %(printable_100)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'e' : Char = '\101' ; %(printable_101)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'f' : Char = '\102' ; %(printable_102)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'g' : Char = '\103' ; %(printable_103)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'h' : Char = '\104' ; %(printable_104)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'i' : Char = '\105' ; %(printable_105)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'j' : Char = '\106' ; %(printable_106)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'k' : Char = '\107' ; %(printable_107)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'l' : Char = '\108' ; %(printable_108)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'm' : Char = '\109' ; %(printable_109)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'n' : Char = '\110' ; %(printable_110)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'o' : Char = '\111' ; %(printable_111)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'p' : Char = '\112' ; %(printable_112)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'q' : Char = '\113' ; %(printable_113)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'r' : Char = '\114' ; %(printable_114)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 's' : Char = '\115' ; %(printable_115)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 't' : Char = '\116' ; %(printable_116)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'u' : Char = '\117' ; %(printable_117)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'v' : Char = '\118' ; %(printable_118)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'w' : Char = '\119' ; %(printable_119)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'x' : Char = '\120' ; %(printable_120)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'y' : Char = '\121' ; %(printable_121)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 'z' : Char = '\122' ; %(printable_122)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '{' : Char = '\123' ; %(printable_123)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '|' : Char = '\124' ; %(printable_124)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '}' : Char = '\125' ; %(printable_125)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '~' : Char = '\126' ; %(printable_126)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ' ' : Char = '\160' ; %(printable_160)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¡' : Char = '\161' ; %(printable_161)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¢' : Char = '\162' ; %(printable_162)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '£' : Char = '\163' ; %(printable_163)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¤' : Char = '\164' ; %(printable_164)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¥' : Char = '\165' ; %(printable_165)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¦' : Char = '\166' ; %(printable_166)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '§' : Char = '\167' ; %(printable_167)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¨' : Char = '\168' ; %(printable_168)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '©' : Char = '\169' ; %(printable_169)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ª' : Char = '\170' ; %(printable_170)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '«' : Char = '\171' ; %(printable_171)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¬' : Char = '\172' ; %(printable_172)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '­' : Char = '\173' ; %(printable_173)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '®' : Char = '\174' ; %(printable_174)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¯' : Char = '\175' ; %(printable_175)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '°' : Char = '\176' ; %(printable_176)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '±' : Char = '\177' ; %(printable_177)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '²' : Char = '\178' ; %(printable_178)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '³' : Char = '\179' ; %(printable_179)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '´' : Char = '\180' ; %(printable_180)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'µ' : Char = '\181' ; %(printable_181)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¶' : Char = '\182' ; %(printable_182)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '·' : Char = '\183' ; %(printable_183)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¸' : Char = '\184' ; %(printable_184)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¹' : Char = '\185' ; %(printable_185)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'º' : Char = '\186' ; %(printable_186)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '»' : Char = '\187' ; %(printable_187)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¼' : Char = '\188' ; %(printable_188)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '½' : Char = '\189' ; %(printable_189)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¾' : Char = '\190' ; %(printable_190)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '¿' : Char = '\191' ; %(printable_191)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'À' : Char = '\192' ; %(printable_192)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Á' : Char = '\193' ; %(printable_193)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Â' : Char = '\194' ; %(printable_194)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ã' : Char = '\195' ; %(printable_195)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ä' : Char = '\196' ; %(printable_196)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Å' : Char = '\197' ; %(printable_197)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Æ' : Char = '\198' ; %(printable_198)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ç' : Char = '\199' ; %(printable_199)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'È' : Char = '\200' ; %(printable_200)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'É' : Char = '\201' ; %(printable_201)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ê' : Char = '\202' ; %(printable_202)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ë' : Char = '\203' ; %(printable_203)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ì' : Char = '\204' ; %(printable_204)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Í' : Char = '\205' ; %(printable_205)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Î' : Char = '\206' ; %(printable_206)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ï' : Char = '\207' ; %(printable_207)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ð' : Char = '\208' ; %(printable_208)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ñ' : Char = '\209' ; %(printable_209)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ò' : Char = '\210' ; %(printable_210)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ó' : Char = '\211' ; %(printable_211)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ô' : Char = '\212' ; %(printable_212)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Õ' : Char = '\213' ; %(printable_213)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ö' : Char = '\214' ; %(printable_214)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '×' : Char = '\215' ; %(printable_215)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ø' : Char = '\216' ; %(printable_216)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ù' : Char = '\217' ; %(printable_217)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ú' : Char = '\218' ; %(printable_218)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Û' : Char = '\219' ; %(printable_219)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ü' : Char = '\220' ; %(printable_220)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Ý' : Char = '\221' ; %(printable_221)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'Þ' : Char = '\222' ; %(printable_222)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ß' : Char = '\223' ; %(printable_223)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'à' : Char = '\224' ; %(printable_224)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'á' : Char = '\225' ; %(printable_225)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'â' : Char = '\226' ; %(printable_226)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ã' : Char = '\227' ; %(printable_227)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ä' : Char = '\228' ; %(printable_228)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'å' : Char = '\229' ; %(printable_229)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'æ' : Char = '\230' ; %(printable_230)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ç' : Char = '\231' ; %(printable_231)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'è' : Char = '\232' ; %(printable_232)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'é' : Char = '\233' ; %(printable_233)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ê' : Char = '\234' ; %(printable_234)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ë' : Char = '\235' ; %(printable_235)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ì' : Char = '\236' ; %(printable_236)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'í' : Char = '\237' ; %(printable_237)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'î' : Char = '\238' ; %(printable_238)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ï' : Char = '\239' ; %(printable_239)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ð' : Char = '\240' ; %(printable_240)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ñ' : Char = '\241' ; %(printable_241)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ò' : Char = '\242' ; %(printable_242)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ó' : Char = '\243' ; %(printable_243)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ô' : Char = '\244' ; %(printable_244)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'õ' : Char = '\245' ; %(printable_245)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ö' : Char = '\246' ; %(printable_246)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder '÷' : Char = '\247' ; %(printable_247)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ø' : Char = '\248' ; %(printable_248)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ù' : Char = '\249' ; %(printable_249)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ú' : Char = '\250' ; %(printable_250)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'û' : Char = '\251' ; %(printable_251)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ü' : Char = '\252' ; %(printable_252)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ý' : Char = '\253' ; %(printable_253)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'þ' : Char = '\254' ; %(printable_254)%
5a448e9be8c4482a978b174b744237757335140fChristian Maeder 'ÿ' : Char = '\255' ; %(printable_255)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder preds isLetter(c:Char) <=> (
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (ord('A') <= ord(c) /\ ord(c) <= ord('Z')) \/
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (ord('a') <= ord(c) /\ ord(c) <= ord('z')) ); %(isLetter_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder isDigit(c:Char) <=> ord('0') <= ord(c) /\ ord(c) <= ord('9'); %(isDigit_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder isPrintable(c:Char) <=> (
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (ord(' ') <= ord(c) /\ ord(c) <= ord('~') ) \/
5a448e9be8c4482a978b174b744237757335140fChristian Maeder (ord(' ') <= ord(c) /\ ord(c) <= ord('ÿ')) ) %(isPrintable_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% alternative definition of characters as '\o ppp',
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% where p in {0,1,...,7} :
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops '\o000' : Char = '\000'; %(slash_o000)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o001' : Char = '\001'; %(slash_o001)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o002' : Char = '\002'; %(slash_o002)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o003' : Char = '\003'; %(slash_o003)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o004' : Char = '\004'; %(slash_o004)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o005' : Char = '\005'; %(slash_o005)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o006' : Char = '\006'; %(slash_o006)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o007' : Char = '\007'; %(slash_o007)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o010' : Char = '\008'; %(slash_o010)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o011' : Char = '\009'; %(slash_o011)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o012' : Char = '\010'; %(slash_o012)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o013' : Char = '\011'; %(slash_o013)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o014' : Char = '\012'; %(slash_o014)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o015' : Char = '\013'; %(slash_o015)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o016' : Char = '\014'; %(slash_o016)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o017' : Char = '\015'; %(slash_o017)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o020' : Char = '\016'; %(slash_o020)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o021' : Char = '\017'; %(slash_o021)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o022' : Char = '\018'; %(slash_o022)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o023' : Char = '\019'; %(slash_o023)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o024' : Char = '\020'; %(slash_o024)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o025' : Char = '\021'; %(slash_o025)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o026' : Char = '\022'; %(slash_o026)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o027' : Char = '\023'; %(slash_o027)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o030' : Char = '\024'; %(slash_o030)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o031' : Char = '\025'; %(slash_o031)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o032' : Char = '\026'; %(slash_o032)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o033' : Char = '\027'; %(slash_o033)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o034' : Char = '\028'; %(slash_o034)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o035' : Char = '\029'; %(slash_o035)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o036' : Char = '\030'; %(slash_o036)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o037' : Char = '\031'; %(slash_o037)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o040' : Char = '\032'; %(slash_o040)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o041' : Char = '\033'; %(slash_o041)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o042' : Char = '\034'; %(slash_o042)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o043' : Char = '\035'; %(slash_o043)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o044' : Char = '\036'; %(slash_o044)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o045' : Char = '\037'; %(slash_o045)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o046' : Char = '\038'; %(slash_o046)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o047' : Char = '\039'; %(slash_o047)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o050' : Char = '\040'; %(slash_o050)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o051' : Char = '\041'; %(slash_o051)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o052' : Char = '\042'; %(slash_o052)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o053' : Char = '\043'; %(slash_o053)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o054' : Char = '\044'; %(slash_o054)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o055' : Char = '\045'; %(slash_o055)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o056' : Char = '\046'; %(slash_o056)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o057' : Char = '\047'; %(slash_o057)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o060' : Char = '\048'; %(slash_o060)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o061' : Char = '\049'; %(slash_o061)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o062' : Char = '\050'; %(slash_o062)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o063' : Char = '\051'; %(slash_o063)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o064' : Char = '\052'; %(slash_o064)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o065' : Char = '\053'; %(slash_o065)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o066' : Char = '\054'; %(slash_o066)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o067' : Char = '\055'; %(slash_o067)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o070' : Char = '\056'; %(slash_o070)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o071' : Char = '\057'; %(slash_o071)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o072' : Char = '\058'; %(slash_o072)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o073' : Char = '\059'; %(slash_o073)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o074' : Char = '\060'; %(slash_o074)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o075' : Char = '\061'; %(slash_o075)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o076' : Char = '\062'; %(slash_o076)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o077' : Char = '\063'; %(slash_o077)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o100' : Char = '\064'; %(slash_o100)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o101' : Char = '\065'; %(slash_o101)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o102' : Char = '\066'; %(slash_o102)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o103' : Char = '\067'; %(slash_o103)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o104' : Char = '\068'; %(slash_o104)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o105' : Char = '\069'; %(slash_o105)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o106' : Char = '\070'; %(slash_o106)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o107' : Char = '\071'; %(slash_o107)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o110' : Char = '\072'; %(slash_o110)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o111' : Char = '\073'; %(slash_o111)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o112' : Char = '\074'; %(slash_o112)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o113' : Char = '\075'; %(slash_o113)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o114' : Char = '\076'; %(slash_o114)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o115' : Char = '\077'; %(slash_o115)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o116' : Char = '\078'; %(slash_o116)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o117' : Char = '\079'; %(slash_o117)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o120' : Char = '\080'; %(slash_o120)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o121' : Char = '\081'; %(slash_o121)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o122' : Char = '\082'; %(slash_o122)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o123' : Char = '\083'; %(slash_o123)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o124' : Char = '\084'; %(slash_o124)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o125' : Char = '\085'; %(slash_o125)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o126' : Char = '\086'; %(slash_o126)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o127' : Char = '\087'; %(slash_o127)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o130' : Char = '\088'; %(slash_o130)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o131' : Char = '\089'; %(slash_o131)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o132' : Char = '\090'; %(slash_o132)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o133' : Char = '\091'; %(slash_o133)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o134' : Char = '\092'; %(slash_o134)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o135' : Char = '\093'; %(slash_o135)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o136' : Char = '\094'; %(slash_o136)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o137' : Char = '\095'; %(slash_o137)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o140' : Char = '\096'; %(slash_o140)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o141' : Char = '\097'; %(slash_o141)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o142' : Char = '\098'; %(slash_o142)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o143' : Char = '\099'; %(slash_o143)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o144' : Char = '\100'; %(slash_o144)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o145' : Char = '\101'; %(slash_o145)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o146' : Char = '\102'; %(slash_o146)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o147' : Char = '\103'; %(slash_o147)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o150' : Char = '\104'; %(slash_o150)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o151' : Char = '\105'; %(slash_o151)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o152' : Char = '\106'; %(slash_o152)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o153' : Char = '\107'; %(slash_o153)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o154' : Char = '\108'; %(slash_o154)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o155' : Char = '\109'; %(slash_o155)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o156' : Char = '\110'; %(slash_o156)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o157' : Char = '\111'; %(slash_o157)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o160' : Char = '\112'; %(slash_o160)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o161' : Char = '\113'; %(slash_o161)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o162' : Char = '\114'; %(slash_o162)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o163' : Char = '\115'; %(slash_o163)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o164' : Char = '\116'; %(slash_o164)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o165' : Char = '\117'; %(slash_o165)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o166' : Char = '\118'; %(slash_o166)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o167' : Char = '\119'; %(slash_o167)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o170' : Char = '\120'; %(slash_o170)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o171' : Char = '\121'; %(slash_o171)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o172' : Char = '\122'; %(slash_o172)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o173' : Char = '\123'; %(slash_o173)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o174' : Char = '\124'; %(slash_o174)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o175' : Char = '\125'; %(slash_o175)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o176' : Char = '\126'; %(slash_o176)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o177' : Char = '\127'; %(slash_o177)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o200' : Char = '\128'; %(slash_o200)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o201' : Char = '\129'; %(slash_o201)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o202' : Char = '\130'; %(slash_o202)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o203' : Char = '\131'; %(slash_o203)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o204' : Char = '\132'; %(slash_o204)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o205' : Char = '\133'; %(slash_o205)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o206' : Char = '\134'; %(slash_o206)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o207' : Char = '\135'; %(slash_o207)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o210' : Char = '\136'; %(slash_o210)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o211' : Char = '\137'; %(slash_o211)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o212' : Char = '\138'; %(slash_o212)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o213' : Char = '\139'; %(slash_o213)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o214' : Char = '\140'; %(slash_o214)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o215' : Char = '\141'; %(slash_o215)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o216' : Char = '\142'; %(slash_o216)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o217' : Char = '\143'; %(slash_o217)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o220' : Char = '\144'; %(slash_o220)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o221' : Char = '\145'; %(slash_o221)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o222' : Char = '\146'; %(slash_o222)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o223' : Char = '\147'; %(slash_o223)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o224' : Char = '\148'; %(slash_o224)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o225' : Char = '\149'; %(slash_o225)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o226' : Char = '\150'; %(slash_o226)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o227' : Char = '\151'; %(slash_o227)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o230' : Char = '\152'; %(slash_o230)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o231' : Char = '\153'; %(slash_o231)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o232' : Char = '\154'; %(slash_o232)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o233' : Char = '\155'; %(slash_o233)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o234' : Char = '\156'; %(slash_o234)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o235' : Char = '\157'; %(slash_o235)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o236' : Char = '\158'; %(slash_o236)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o237' : Char = '\159'; %(slash_o237)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o240' : Char = '\160'; %(slash_o240)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o241' : Char = '\161'; %(slash_o241)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o242' : Char = '\162'; %(slash_o242)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o243' : Char = '\163'; %(slash_o243)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o244' : Char = '\164'; %(slash_o244)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o245' : Char = '\165'; %(slash_o245)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o246' : Char = '\166'; %(slash_o246)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o247' : Char = '\167'; %(slash_o247)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o250' : Char = '\168'; %(slash_o250)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o251' : Char = '\169'; %(slash_o251)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o252' : Char = '\170'; %(slash_o252)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o253' : Char = '\171'; %(slash_o253)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o254' : Char = '\172'; %(slash_o254)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o255' : Char = '\173'; %(slash_o255)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o256' : Char = '\174'; %(slash_o256)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o257' : Char = '\175'; %(slash_o257)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o260' : Char = '\176'; %(slash_o260)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o261' : Char = '\177'; %(slash_o261)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o262' : Char = '\178'; %(slash_o262)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o263' : Char = '\179'; %(slash_o263)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o264' : Char = '\180'; %(slash_o264)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o265' : Char = '\181'; %(slash_o265)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o266' : Char = '\182'; %(slash_o266)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o267' : Char = '\183'; %(slash_o267)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o270' : Char = '\184'; %(slash_o270)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o271' : Char = '\185'; %(slash_o271)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o272' : Char = '\186'; %(slash_o272)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o273' : Char = '\187'; %(slash_o273)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o274' : Char = '\188'; %(slash_o274)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o275' : Char = '\189'; %(slash_o275)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o276' : Char = '\190'; %(slash_o276)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o277' : Char = '\191'; %(slash_o277)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o300' : Char = '\192'; %(slash_o300)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o301' : Char = '\193'; %(slash_o301)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o302' : Char = '\194'; %(slash_o302)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o303' : Char = '\195'; %(slash_o303)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o304' : Char = '\196'; %(slash_o304)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o305' : Char = '\197'; %(slash_o305)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o306' : Char = '\198'; %(slash_o306)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o307' : Char = '\199'; %(slash_o307)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o310' : Char = '\200'; %(slash_o310)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o311' : Char = '\201'; %(slash_o311)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o312' : Char = '\202'; %(slash_o312)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o313' : Char = '\203'; %(slash_o313)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o314' : Char = '\204'; %(slash_o314)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o315' : Char = '\205'; %(slash_o315)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o316' : Char = '\206'; %(slash_o316)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o317' : Char = '\207'; %(slash_o317)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o320' : Char = '\208'; %(slash_o320)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o321' : Char = '\209'; %(slash_o321)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o322' : Char = '\210'; %(slash_o322)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o323' : Char = '\211'; %(slash_o323)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o324' : Char = '\212'; %(slash_o324)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o325' : Char = '\213'; %(slash_o325)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o326' : Char = '\214'; %(slash_o326)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o327' : Char = '\215'; %(slash_o327)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o330' : Char = '\216'; %(slash_o330)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o331' : Char = '\217'; %(slash_o331)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o332' : Char = '\218'; %(slash_o332)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o333' : Char = '\219'; %(slash_o333)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o334' : Char = '\220'; %(slash_o334)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o335' : Char = '\221'; %(slash_o335)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o336' : Char = '\222'; %(slash_o336)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o337' : Char = '\223'; %(slash_o337)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o340' : Char = '\224'; %(slash_o340)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o341' : Char = '\225'; %(slash_o341)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o342' : Char = '\226'; %(slash_o342)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o343' : Char = '\227'; %(slash_o343)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o344' : Char = '\228'; %(slash_o344)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o345' : Char = '\229'; %(slash_o345)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o346' : Char = '\230'; %(slash_o346)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o347' : Char = '\231'; %(slash_o347)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o350' : Char = '\232'; %(slash_o350)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o351' : Char = '\233'; %(slash_o351)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o352' : Char = '\234'; %(slash_o352)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o353' : Char = '\235'; %(slash_o353)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o354' : Char = '\236'; %(slash_o354)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o355' : Char = '\237'; %(slash_o355)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o356' : Char = '\238'; %(slash_o356)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o357' : Char = '\239'; %(slash_o357)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o360' : Char = '\240'; %(slash_o360)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o361' : Char = '\241'; %(slash_o361)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o362' : Char = '\242'; %(slash_o362)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o363' : Char = '\243'; %(slash_o363)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o364' : Char = '\244'; %(slash_o364)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o365' : Char = '\245'; %(slash_o365)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o366' : Char = '\246'; %(slash_o366)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o367' : Char = '\247'; %(slash_o367)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o370' : Char = '\248'; %(slash_o370)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o371' : Char = '\249'; %(slash_o371)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o372' : Char = '\250'; %(slash_o372)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o373' : Char = '\251'; %(slash_o373)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o374' : Char = '\252'; %(slash_o374)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o375' : Char = '\253'; %(slash_o375)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o376' : Char = '\254'; %(slash_o376)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\o377' : Char = '\255'; %(slash_o377)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% alternative definition of characters as '\xhh',
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% where h in {0,1,..., F} :
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x00' : Char = '\000'; %(slash_x00)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x01' : Char = '\001'; %(slash_x01)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x02' : Char = '\002'; %(slash_x02)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x03' : Char = '\003'; %(slash_x03)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x04' : Char = '\004'; %(slash_x04)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x05' : Char = '\005'; %(slash_x05)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x06' : Char = '\006'; %(slash_x06)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x07' : Char = '\007'; %(slash_x07)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x08' : Char = '\008'; %(slash_x08)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x09' : Char = '\009'; %(slash_x09)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x0A' : Char = '\010'; %(slash_x0A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x0B' : Char = '\011'; %(slash_x0B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x0C' : Char = '\012'; %(slash_x0C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x0D' : Char = '\013'; %(slash_x0D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x0E' : Char = '\014'; %(slash_x0E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x0F' : Char = '\015'; %(slash_x0F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x10' : Char = '\016'; %(slash_x10)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x11' : Char = '\017'; %(slash_x11)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x12' : Char = '\018'; %(slash_x12)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x13' : Char = '\019'; %(slash_x13)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x14' : Char = '\020'; %(slash_x14)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x15' : Char = '\021'; %(slash_x15)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x16' : Char = '\022'; %(slash_x16)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x17' : Char = '\023'; %(slash_x17)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x18' : Char = '\024'; %(slash_x18)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x19' : Char = '\025'; %(slash_x19)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x1A' : Char = '\026'; %(slash_x1A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x1B' : Char = '\027'; %(slash_x1B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x1C' : Char = '\028'; %(slash_x1C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x1D' : Char = '\029'; %(slash_x1D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x1E' : Char = '\030'; %(slash_x1E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x1F' : Char = '\031'; %(slash_x1F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x20' : Char = '\032'; %(slash_x20)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x21' : Char = '\033'; %(slash_x21)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x22' : Char = '\034'; %(slash_x22)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x23' : Char = '\035'; %(slash_x23)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x24' : Char = '\036'; %(slash_x24)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x25' : Char = '\037'; %(slash_x25)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x26' : Char = '\038'; %(slash_x26)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x27' : Char = '\039'; %(slash_x27)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x28' : Char = '\040'; %(slash_x28)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x29' : Char = '\041'; %(slash_x29)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x2A' : Char = '\042'; %(slash_x2A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x2B' : Char = '\043'; %(slash_x2B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x2C' : Char = '\044'; %(slash_x2C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x2D' : Char = '\045'; %(slash_x2D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x2E' : Char = '\046'; %(slash_x2E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x2F' : Char = '\047'; %(slash_x2F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x30' : Char = '\048'; %(slash_x30)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x31' : Char = '\049'; %(slash_x31)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x32' : Char = '\050'; %(slash_x32)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x33' : Char = '\051'; %(slash_x33)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x34' : Char = '\052'; %(slash_x34)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x35' : Char = '\053'; %(slash_x35)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x36' : Char = '\054'; %(slash_x36)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x37' : Char = '\055'; %(slash_x37)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x38' : Char = '\056'; %(slash_x38)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x39' : Char = '\057'; %(slash_x39)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x3A' : Char = '\058'; %(slash_x3A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x3B' : Char = '\059'; %(slash_x3B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x3C' : Char = '\060'; %(slash_x3C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x3D' : Char = '\061'; %(slash_x3D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x3E' : Char = '\062'; %(slash_x3E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x3F' : Char = '\063'; %(slash_x3F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x40' : Char = '\064'; %(slash_x40)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x41' : Char = '\065'; %(slash_x41)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x42' : Char = '\066'; %(slash_x42)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x43' : Char = '\067'; %(slash_x43)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x44' : Char = '\068'; %(slash_x44)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x45' : Char = '\069'; %(slash_x45)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x46' : Char = '\070'; %(slash_x46)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x47' : Char = '\071'; %(slash_x47)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x48' : Char = '\072'; %(slash_x48)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x49' : Char = '\073'; %(slash_x49)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x4A' : Char = '\074'; %(slash_x4A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x4B' : Char = '\075'; %(slash_x4B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x4C' : Char = '\076'; %(slash_x4C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x4D' : Char = '\077'; %(slash_x4D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x4E' : Char = '\078'; %(slash_x4E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x4F' : Char = '\079'; %(slash_x4F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x50' : Char = '\080'; %(slash_x50)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x51' : Char = '\081'; %(slash_x51)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x52' : Char = '\082'; %(slash_x52)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x53' : Char = '\083'; %(slash_x53)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x54' : Char = '\084'; %(slash_x54)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x55' : Char = '\085'; %(slash_x55)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x56' : Char = '\086'; %(slash_x56)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x57' : Char = '\087'; %(slash_x57)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x58' : Char = '\088'; %(slash_x58)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x59' : Char = '\089'; %(slash_x59)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x5A' : Char = '\090'; %(slash_x5A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x5B' : Char = '\091'; %(slash_x5B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x5C' : Char = '\092'; %(slash_x5C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x5D' : Char = '\093'; %(slash_x5D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x5E' : Char = '\094'; %(slash_x5E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x5F' : Char = '\095'; %(slash_x5F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x60' : Char = '\096'; %(slash_x60)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x61' : Char = '\097'; %(slash_x61)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x62' : Char = '\098'; %(slash_x62)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x63' : Char = '\099'; %(slash_x63)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x64' : Char = '\100'; %(slash_x64)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x65' : Char = '\101'; %(slash_x65)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x66' : Char = '\102'; %(slash_x66)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x67' : Char = '\103'; %(slash_x67)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x68' : Char = '\104'; %(slash_x68)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x69' : Char = '\105'; %(slash_x69)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x6A' : Char = '\106'; %(slash_x6A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x6B' : Char = '\107'; %(slash_x6B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x6C' : Char = '\108'; %(slash_x6C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x6D' : Char = '\109'; %(slash_x6D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x6E' : Char = '\110'; %(slash_x6E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x6F' : Char = '\111'; %(slash_x6F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x70' : Char = '\112'; %(slash_x70)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x71' : Char = '\113'; %(slash_x71)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x72' : Char = '\114'; %(slash_x72)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x73' : Char = '\115'; %(slash_x73)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x74' : Char = '\116'; %(slash_x74)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x75' : Char = '\117'; %(slash_x75)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x76' : Char = '\118'; %(slash_x76)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x77' : Char = '\119'; %(slash_x77)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x78' : Char = '\120'; %(slash_x78)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x79' : Char = '\121'; %(slash_x79)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x7A' : Char = '\122'; %(slash_x7A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x7B' : Char = '\123'; %(slash_x7B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x7C' : Char = '\124'; %(slash_x7C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x7D' : Char = '\125'; %(slash_x7D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x7E' : Char = '\126'; %(slash_x7E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x7F' : Char = '\127'; %(slash_x7F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x80' : Char = '\128'; %(slash_x80)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x81' : Char = '\129'; %(slash_x81)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x82' : Char = '\130'; %(slash_x82)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x83' : Char = '\131'; %(slash_x83)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x84' : Char = '\132'; %(slash_x84)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x85' : Char = '\133'; %(slash_x85)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x86' : Char = '\134'; %(slash_x86)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x87' : Char = '\135'; %(slash_x87)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x88' : Char = '\136'; %(slash_x88)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x89' : Char = '\137'; %(slash_x89)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x8A' : Char = '\138'; %(slash_x8A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x8B' : Char = '\139'; %(slash_x8B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x8C' : Char = '\140'; %(slash_x8C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x8D' : Char = '\141'; %(slash_x8D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x8E' : Char = '\142'; %(slash_x8E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x8F' : Char = '\143'; %(slash_x8F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x90' : Char = '\144'; %(slash_x90)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x91' : Char = '\145'; %(slash_x91)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x92' : Char = '\146'; %(slash_x92)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x93' : Char = '\147'; %(slash_x93)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x94' : Char = '\148'; %(slash_x94)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x95' : Char = '\149'; %(slash_x95)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x96' : Char = '\150'; %(slash_x96)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x97' : Char = '\151'; %(slash_x97)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x98' : Char = '\152'; %(slash_x98)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x99' : Char = '\153'; %(slash_x99)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x9A' : Char = '\154'; %(slash_x9A)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x9B' : Char = '\155'; %(slash_x9B)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x9C' : Char = '\156'; %(slash_x9C)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x9D' : Char = '\157'; %(slash_x9D)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x9E' : Char = '\158'; %(slash_x9E)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\x9F' : Char = '\159'; %(slash_x9F)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA0' : Char = '\160'; %(slash_xA0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA1' : Char = '\161'; %(slash_xA1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA2' : Char = '\162'; %(slash_xA2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA3' : Char = '\163'; %(slash_xA3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA4' : Char = '\164'; %(slash_xA4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA5' : Char = '\165'; %(slash_xA5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA6' : Char = '\166'; %(slash_xA6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA7' : Char = '\167'; %(slash_xA7)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA8' : Char = '\168'; %(slash_xA8)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xA9' : Char = '\169'; %(slash_xA9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xAA' : Char = '\170'; %(slash_xAA)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xAB' : Char = '\171'; %(slash_xAB)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xAC' : Char = '\172'; %(slash_xAC)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xAD' : Char = '\173'; %(slash_xAD)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xAE' : Char = '\174'; %(slash_xAE)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xAF' : Char = '\175'; %(slash_xAF)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB0' : Char = '\176'; %(slash_xB0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB1' : Char = '\177'; %(slash_xB1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB2' : Char = '\178'; %(slash_xB2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB3' : Char = '\179'; %(slash_xB3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB4' : Char = '\180'; %(slash_xB4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB5' : Char = '\181'; %(slash_xB5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB6' : Char = '\182'; %(slash_xB6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB7' : Char = '\183'; %(slash_xB7)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB8' : Char = '\184'; %(slash_xB8)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xB9' : Char = '\185'; %(slash_xB9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xBA' : Char = '\186'; %(slash_xBA)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xBB' : Char = '\187'; %(slash_xBB)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xBC' : Char = '\188'; %(slash_xBC)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xBD' : Char = '\189'; %(slash_xBD)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xBE' : Char = '\190'; %(slash_xBE)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xBF' : Char = '\191'; %(slash_xBF)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC0' : Char = '\192'; %(slash_xC0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC1' : Char = '\193'; %(slash_xC1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC2' : Char = '\194'; %(slash_xC2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC3' : Char = '\195'; %(slash_xC3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC4' : Char = '\196'; %(slash_xC4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC5' : Char = '\197'; %(slash_xC5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC6' : Char = '\198'; %(slash_xC6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC7' : Char = '\199'; %(slash_xC7)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC8' : Char = '\200'; %(slash_xC8)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xC9' : Char = '\201'; %(slash_xC9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xCA' : Char = '\202'; %(slash_xCA)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xCB' : Char = '\203'; %(slash_xCB)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xCC' : Char = '\204'; %(slash_xCC)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xCD' : Char = '\205'; %(slash_xCD)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xCE' : Char = '\206'; %(slash_xCE)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xCF' : Char = '\207'; %(slash_xCF)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD0' : Char = '\208'; %(slash_xD0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD1' : Char = '\209'; %(slash_xD1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD2' : Char = '\210'; %(slash_xD2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD3' : Char = '\211'; %(slash_xD3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD4' : Char = '\212'; %(slash_xD4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD5' : Char = '\213'; %(slash_xD5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD6' : Char = '\214'; %(slash_xD6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD7' : Char = '\215'; %(slash_xD7)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD8' : Char = '\216'; %(slash_xD8)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xD9' : Char = '\217'; %(slash_xD9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xDA' : Char = '\218'; %(slash_xDA)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xDB' : Char = '\219'; %(slash_xDB)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xDC' : Char = '\220'; %(slash_xDC)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xDD' : Char = '\221'; %(slash_xDD)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xDE' : Char = '\222'; %(slash_xDE)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xDF' : Char = '\223'; %(slash_xDF)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE0' : Char = '\224'; %(slash_xE0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE1' : Char = '\225'; %(slash_xE1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE2' : Char = '\226'; %(slash_xE2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE3' : Char = '\227'; %(slash_xE3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE4' : Char = '\228'; %(slash_xE4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE5' : Char = '\229'; %(slash_xE5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE6' : Char = '\230'; %(slash_xE6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE7' : Char = '\231'; %(slash_xE7)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE8' : Char = '\232'; %(slash_xE8)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xE9' : Char = '\233'; %(slash_xE9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xEA' : Char = '\234'; %(slash_xEA)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xEB' : Char = '\235'; %(slash_xEB)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xEC' : Char = '\236'; %(slash_xEC)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xED' : Char = '\237'; %(slash_xED)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xEE' : Char = '\238'; %(slash_xEE)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xEF' : Char = '\239'; %(slash_xEF)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF0' : Char = '\240'; %(slash_xF0)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF1' : Char = '\241'; %(slash_xF1)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF2' : Char = '\242'; %(slash_xF2)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF3' : Char = '\243'; %(slash_xF3)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF4' : Char = '\244'; %(slash_xF4)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF5' : Char = '\245'; %(slash_xF5)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF6' : Char = '\246'; %(slash_xF6)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF7' : Char = '\247'; %(slash_xF7)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF8' : Char = '\248'; %(slash_xF8)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xF9' : Char = '\249'; %(slash_xF9)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xFA' : Char = '\250'; %(slash_xFA)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xFB' : Char = '\251'; %(slash_xFB)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xFC' : Char = '\252'; %(slash_xFC)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xFD' : Char = '\253'; %(slash_xFD)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xFE' : Char = '\254'; %(slash_xFE)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\xFF' : Char = '\255'; %(slash_xFF)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% special characters:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops NUL:Char = '\000'; %(NUL_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SOH:Char = '\001'; %(SOH_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SYX:Char = '\002'; %(SYX_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ETX:Char = '\003'; %(ETX_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder EOT:Char = '\004'; %(EOT_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ENQ:Char = '\005'; %(ENQ_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ACK:Char = '\006'; %(ACK_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder BEL:Char = '\007'; %(BEL_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder BS:Char = '\008'; %(BS_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder HT:Char = '\009'; %(HT_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder LF:Char = '\010'; %(LF_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder VT:Char = '\011'; %(VT_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder FF:Char = '\012'; %(FF_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder CR:Char = '\013'; %(CR_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SO:Char = '\014'; %(SO_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SI:Char = '\015'; %(SI_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder DLE:Char = '\016'; %(DLE_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder DC1:Char = '\017'; %(DC1_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder DC2:Char = '\018'; %(DC2_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder DC3:Char = '\019'; %(DC3_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder DC4:Char = '\020'; %(DC4_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder NAK:Char = '\021'; %(NAK_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SYN:Char = '\022'; %(SYN_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ETB:Char = '\023'; %(ETB_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder CAN:Char = '\024'; %(CAN_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder EM:Char = '\025'; %(EM_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SUB:Char = '\026'; %(SUB_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ESC:Char = '\027'; %(ESC_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder FS:Char = '\028'; %(FS_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder GS:Char = '\029'; %(GS_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder RS:Char = '\030'; %(RS_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder US:Char = '\031'; %(US_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder SP:Char = '\032'; %(SP_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder DEL:Char = '\127'; %(DEL_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% alternative names for special charcters:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops NL:Char = LF; %(NL_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder NP:Char = FF; %(NP_def)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% character constants:
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ops '\n' : Char = NL; %(slash_n)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\t' : Char = HT; %(slash_t)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\v' : Char = VT; %(slash_v)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\b' : Char = BS; %(slash_b)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\r' : Char = CR; %(slash_r)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\f' : Char = FF; %(slash_f)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\a' : Char = BEL; %(slash_a)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder '\?' : Char = '?'; %(slash_quest)%
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
9d75607bcf5f66d02e90db8b92ff89f89f48f16eChristian Maeder
9d75607bcf5f66d02e90db8b92ff89f89f48f16eChristian Maedersort a;
9d75607bcf5f66d02e90db8b92ff89f89f48f16eChristian Maederops __||__ : a * a -> a, assoc
9d75607bcf5f66d02e90db8b92ff89f89f48f16eChristian Maeder
9d75607bcf5f66d02e90db8b92ff89f89f48f16eChristian Maederop b : a
9d75607bcf5f66d02e90db8b92ff89f89f48f16eChristian Maeder. b || b || b = b