BasicSpec.casl.output revision 0a907ffb1de8958ba48d229e5f5039141d4499cc
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringfree type Nat ::= 0 | suc (pre :? Nat)
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay Sieverspreds __<=__, __<__, __>=__, __>__ : Nat * Nat;
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay Sievers odd, even : Nat
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringops min, max : Nat * Nat ->? Nat
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringops __+__, __*__ : Nat * Nat -> Nat;
05677bb78079c3fa0283101aac2c07581f4873f1Lennart Poettering __^__ : Nat * Nat -> Nat;
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart Poettering min, max : Nat * Nat -> Nat;
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers +__ : Nat -> Nat;
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers abs : Nat -> Nat;
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers __! : Nat -> Nat;
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers __-?__ : Nat * Nat ->? Nat;
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering __/?__ : Nat * Nat ->? Nat;
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering __div__, __mod__, __quot__, __rem__ : Nat * Nat ->? Nat; %()%
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sievers %% Operations to represent natural numbers with digits:
4ce849853c46b1e857df3c6c9e7752159a58ddf1Lennart Poettering 1, 2, 3, 4, 5, 6, 7, 8, 9 : Nat;
4ce849853c46b1e857df3c6c9e7752159a58ddf1Lennart Poettering __@@__ : Nat * Nat -> Nat
c3090674833c8bd34fbdb0e743f1c47d85dd14fbLennart Poetteringforall m, n, r, s : Nat
c3090674833c8bd34fbdb0e743f1c47d85dd14fbLennart Poettering. 0 <= n %(Nat_leq_def1)%
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering. not (suc (n) <= 0) %(Nat_leq_def2)%
205b7fa46594b38901636b167b02a8725d915b79Lennart Poettering. suc (m) <= suc (n) <=> m <= n %(Nat_leq_def3)%
8e417f59b668b1e5cbf6c1ff305595a6ffe56fbaLennart Poettering. m >= n <=> n <= m %(Nat_geq_def)%
8e417f59b668b1e5cbf6c1ff305595a6ffe56fbaLennart Poettering. m < n <=> (m <= n /\ not (m = n)) %(Nat_less_def)%
8e417f59b668b1e5cbf6c1ff305595a6ffe56fbaLennart Poettering. m > n <=> m < n %(Nat_greater_def)%
8e417f59b668b1e5cbf6c1ff305595a6ffe56fbaLennart Poettering. 0 + m = m %(Nat_add_0)%
728075eea89dc20067d900bb086d3515e37caab0Lennart Poettering. suc (n) + m = suc (n + m) %(Nat_add_suc)%
728075eea89dc20067d900bb086d3515e37caab0Lennart Poettering. 0 * m = 0 %(Nat_mult_0)%
c817bbb1cbc47e2436731914710195d65fa0dd83Lennart Poettering. suc (n) * m = (n * m) + m %(Nat_mult_suc)%
c817bbb1cbc47e2436731914710195d65fa0dd83Lennart Poettering. m ^ 0 = 1 %(Nat_power_0)%
c817bbb1cbc47e2436731914710195d65fa0dd83Lennart Poettering. m ^ suc (n) = m * m ^ n %(Nat_power_suc)%
c817bbb1cbc47e2436731914710195d65fa0dd83Lennart Poettering. min (m, n) = m when m <= n else n %(Nat_min_def)%
ec6d2611e4c48409613870ea3924f5e36ab1997aLennart Poettering. max (m, n) = n when m <= n else m %(Nat_max_def)%
ec6d2611e4c48409613870ea3924f5e36ab1997aLennart Poettering. + m = m %(plus_def)%
ec6d2611e4c48409613870ea3924f5e36ab1997aLennart Poettering. abs (n) = n %(Nat_abs)%
6eebcda6a260cae878e7329b457c80b53bdc4b49Lennart Poettering. odd (m) <=> not even (m) %(Nat_odd_def)%
6eebcda6a260cae878e7329b457c80b53bdc4b49Lennart Poettering. even (0) %(Nat_even_0)%
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering. even (suc (m)) <=> odd (m) %(Nat_even_suc)%
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering. 0 ! = 1 %(Nat_factorial_0)%
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering. suc (n) ! = suc (n) * n ! %(Nat_factorial_suc)%
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering. m -? n = r <=> m = r + n %(Nat_sub_def)%
788f75a0e766738c052086e856b7c1b1b676de6bLennart Poettering. not def (m /? 0) %(Nat_divide_0)%
788f75a0e766738c052086e856b7c1b1b676de6bLennart Poettering. (m /? n = r <=> m = r * n) if n > 0 %(Nat_divide_Pos)%
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering. m div n = r <=> (exists s : Nat . m = n * r + s /\ s < n)
205b7fa46594b38901636b167b02a8725d915b79Lennart Poettering. m mod n = s <=> (exists r : Nat . m = n * r + s /\ s < n)
772374a8c4808529fb0d0060cb81c6685b35f6dbKay Sievers. m quot n = m div n %(Nat_quot)%
9b41366baeb02b0e732f22f8b5d42a25ae569e20Lennart Poettering. m rem n = m mod n %(Nat_rem)%
95b4be171988fc2ea33377b1b4450e5d410add7bLennart Poettering. 1 = suc (0) %(Nat_1_def)%
95b4be171988fc2ea33377b1b4450e5d410add7bLennart Poettering. 2 = suc (1) %(Nat_2_def)%
15abdb9a6f34628b04b887e0b9649fa582d6cd37Lennart Poettering. 3 = suc (2) %(Nat_3_def)%
2d0b0528ace89d378051c280bf3be367b2a7d2deLennart Poettering. 4 = suc (3) %(Nat_4_def)%
499519c6499e92d1953fd79b99a805b9278d5ea1Lennart Poettering. 5 = suc (4) %(Nat_5_def)%
499519c6499e92d1953fd79b99a805b9278d5ea1Lennart Poettering. 6 = suc (5) %(Nat_6_def)%
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering. 7 = suc (6) %(Nat_7_def)%
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering. 8 = suc (7) %(Nat_8_def)%
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering. 9 = suc (8) %(Nat_9_def)%
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering. m @@ n = (m * suc (9)) + n; %(Nat_decimal_def)%
5965984d6b9f7751d6281028142ecf3ca475f156Lennart Poetteringtype Pos = {p : Nat . p > 0}
5965984d6b9f7751d6281028142ecf3ca475f156Lennart Poetteringops 1 : Pos = suc (0); %(Nat_1_as_Pos_def)%
e41814846c19a48f4490169d82e359e005c4db45Lennart Poettering __*__ : Pos * Pos -> Pos;
e41814846c19a48f4490169d82e359e005c4db45Lennart Poettering __+__ : Pos * Nat -> Pos;
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering __+__ : Nat * Pos -> Pos;
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering suc : Nat -> Pos
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering%% then %implies
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poetteringops min, max : Nat * Nat -> Nat, comm, assoc
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poetteringforall x, m, n, r, s, t : Nat; p : Pos
15abdb9a6f34628b04b887e0b9649fa582d6cd37Lennart Poettering. def (m -? n) <=> m >= n %(Nat_sub_dom)%
8ed206517c2be381324ac5832bf34cc14024270eLennart Poettering. def (m /? n) <=> m mod n = 0 %(Nat_divide_dom)%
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poettering. def (m div n) <=> not (n = 0) %(Nat_div_dom)%
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poettering. def (m mod n) <=> not (n = 0) %(Nat_mod_dom)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering. def (m quot n) <=> not (n = 0) %(Nat_quot_dom)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering. def (m rem n) <=> not (n = 0) %(Nat_rem_dom)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering. (r + s) * t = (r * t) + (s * t) %(Nat_distr)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering. max (m, 0) = m %(Nat_max_unit)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering. min (m, 0) = 0; %(Nat_min_0)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poetteringgenerated type Int ::= __-__ (Nat; Nat)
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poetteringforall a, b, c, d : Nat
7361c3b4e1e28a7eb4354a3da354b22e79782141Lennart Poettering. a - b = c - d <=> a + d = c + b; %(Int_equality)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poetteringforall a : Nat . a = a - 0; %(Int_Nat_embedding)%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poetteringpreds __<=__, __<__, __>=__, __>__ : Int * Int;
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers odd, even : Int
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sieversops 0, 1 : Int;
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers __+__, __-__, __*__ : Int * Int -> Int;
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers __^__ : Int * Nat -> Int;
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers +__, -__, sign : Int -> Int;
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers min, max : Int * Int -> Int;
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers abs : Int -> Nat;
f6113d42d015ad9f3a9e702a09eb8006511a4424Kay Sievers __/?__, __div__, __quot__, __rem__ : Int * Int ->? Int;
f6113d42d015ad9f3a9e702a09eb8006511a4424Kay Sievers __mod__ : Int * Int ->? Nat
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sieversforall m, n, r, s : Int; a, b, c, d : Nat
7a43e910ce00eef22fd42925ae4c85cbea1b1320Kay Sievers. (a - b) + (c - d) = (a + c) - (b + d) %(Int_add_def)%
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers. (a - b) * (c - d) = (a * c + b * d) - (b * c + a * d)
c55b1b59b837dfd924b704d457ed77c55f8bfeabLennart Poettering %(Int_mult_def)%
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering. m - n = m + (- n) %(Int_sub_def)%
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering. + m = m %(Int_pos_def)%
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering. - (a - b) = b - a %(Int_neg_def)%
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering. sign (m) = 0 when m = 0 else (1 when m > 0 else - 1)
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers %(Int_sign_def)%
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers. m <= n <=> n - m in Nat %(Int_leq_def)%
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers. m >= n <=> n <= m %(Int_geq_def)%
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers. m < n <=> (m <= n /\ not (m = n)) %(Int_less_def)%
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers. m > n <=> m < n %(Int_greater_def)%
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poettering. min (m, n) = m when m <= n else n %(Int_min_def)%
9ec82de1725ddaab333149171b790d62c47ae133Lennart Poettering. max (m, n) = n when m <= n else m %(Int_max_def)%
9ec82de1725ddaab333149171b790d62c47ae133Lennart Poettering. abs (m) = - m if m < 0 %(Int_abs_def)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. (- 1) ^ a = 1 when even (a) else - 1 %(Int_neg1_power_def)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. m ^ a = sign (m) ^ a * abs (m) ^ a %(Int_power_def)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. even (m) <=> even (abs (m)) %(Int_even_def)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. odd (m) <=> not (even (m)) %(Int_odd_def)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. m /? n = sign (m) * sign (n) * (abs (m) /? abs (n))
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering %(Int_divide)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. m mod n < abs (n) if not n = 0 %(Int_mod_range)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. m = (m div n) * n + (m mod n) if not n = 0 %(Int_mod__div_def)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. not def m mod 0 %(Int_mod_zero)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. not def m div 0 %(Int_div_zero)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering. m quot n = sign (m) * sign (n) * (abs (m) quot abs (n))
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering %(Int_quot_def)%
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering. m rem n = sign (m) * sign (n) * (abs (m) rem abs (n))
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering forall m, n, r : Int; a, b : Nat . def (a -? b) => a -? b = a - b
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering %(Int_rem_def)%
f2d433e178df7df01a836e95775261e1d85ec60dZbigniew Jędrzejewski-Szmek%(Int_Nat_sub_compat)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. m = sign (m) * abs (m) %(Int_abs_decomp)%
f2d433e178df7df01a836e95775261e1d85ec60dZbigniew Jędrzejewski-Szmek. odd (m) <=> odd (abs (m)) %(Int_odd_alt)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. m /? n = r <=> not n = 0 /\ n * r = n %(Int_divide_dom1)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. def (m /? n) <=> m mod n = 0 %(Int_divide_dom2)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. def (m mod n) <=> not n = 0 %(Int_mod_dom)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. m mod n = m mod abs (n) %(Int_mod_abs)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. def (m div n) <=> not n = 0 %(Int_div_dom)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. def (m quot n) <=> not n = 0 %(Int_quot_dom)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. def (m rem n) <=> not n = 0 %(Int_rem_dom)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. m = (m quot n) * n + (m rem n) if not n = 0; %(Int_quot_rem)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poetteringgenerated type Rat ::= __/__ (Int; Pos)
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poetteringforall i, j : Int; p, q : Pos
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering. i / p = j / q <=> i * q = j * p; %(Rat_equality)%
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poetteringforall i : Int . i / 1 = i; %(embeddingIntToRat)%
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poetteringpreds __<=__, __<__, __>=__, __>__ : Rat * Rat
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poetteringops 0, 1 : Rat;
603cd8fe07cb03e8b11722d1a732e569e5a46347Lennart Poettering __+__, __-__, __*__ : Rat * Rat -> Rat;
06bf461193b4e7f9936abf7582e8b82e39e187c8Lennart Poettering __/__ : Rat * Rat ->? Rat;
06bf461193b4e7f9936abf7582e8b82e39e187c8Lennart Poettering +__, -__, abs : Rat -> Rat;
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering __^__ : Rat * Int -> Rat;
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering min, max : Rat * Rat -> Rat
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poetteringforall p, q : Pos; n : Nat; i, j : Int; x, y, z : Rat
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering. (i / p <= j / q <=> i * q <= j * p) %(Rat_leq_def)%
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering. x >= y <=> y <= x %(Rat_geq_def)%
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering. x < y <=> (x <= y /\ not (x = y)) %(Rat_less_def)%
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering. x > y <=> y < x %(Rat_greater_def)%
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering. (i / p) + (j / q) = (i * q + j * p) / (p * q) %(Rat_add_def)%
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering. x - y = x + (- y) %(Rat_sub_def)%
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering. (i / p) * (j / q) = (i * j) / (p * q) %(Rat_mult_def)%
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart Poettering. not def x / 0 %(Rat_divide_def1)%
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart Poettering. (x / y = z <=> z = x * y) if not y = 0 %(Rat_divide_def2)%
9a526a06bd22ccaf6641d11323fb04a0512a0e49Lennart Poettering. + x = x %(Rat_plus_def)%
9a526a06bd22ccaf6641d11323fb04a0512a0e49Lennart Poettering. - (i / p) = (- i) / p %(Rat_minus_def)%
a8985ba3c2ad428bf572c636f9d64c4ce52bfbe7Lennart Poettering. abs (i / p) = abs (i) / p %(Rat_abs_def)%
a8985ba3c2ad428bf572c636f9d64c4ce52bfbe7Lennart Poettering. x ^ 0 = 1 %(Rat_power_0)%
9b27910bb0c23e5225fc1177176e4f9bf9bf787bLennart Poettering. x ^ suc (n) = x * x ^ n %(Rat_power_suc)%
9b27910bb0c23e5225fc1177176e4f9bf9bf787bLennart Poettering. x ^ (- p) = 1 / (x ^ p) %(Rat_power_neg)%
b03bfa212dd23397871e36ea32c35cdd8fe43506Lennart Poettering. min (x, y) = x when x <= y else y %(Rat_min_def)%
b03bfa212dd23397871e36ea32c35cdd8fe43506Lennart Poettering. max (x, y) = y
935fb723ba7370abaf793914fb5a722f7f5e41e1Lennart Poettering when x <= y else
b03bfa212dd23397871e36ea32c35cdd8fe43506Lennart Poettering forall i, j : Int; p, q : Pos
b03bfa212dd23397871e36ea32c35cdd8fe43506Lennart Poettering . (i / p) - (j / q) = (i * q - j * p) / (p * q) %(Rat_max_def)%
935fb723ba7370abaf793914fb5a722f7f5e41e1Lennart Poettering%% then %implies
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poettering%(Rat_sub_rule)%
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers. (i / p) / (j / q) = (i / p) * (q / j) if not j = 0;
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers %(Rat_divide_rule)%
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieverspred __<__ : a * a
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieverstypes s, t < s
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sieversvars a : t; a, b : s
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sieversvars a : t; a, b : s
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering. a = a forall a : t; a, b : s . a = a
1b89884ba31cbe98f159ce2c7d6fac5f6a57698fLennart Poettering ::= type s2, s1 | c | c (a; a : t; b : t; a : t; d : t) | c (a)?
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poetterings ::= type s2, s1 | c | c (a; a : t; b : t; d : t) | c (a)?
15abdb9a6f34628b04b887e0b9649fa582d6cd37Lennart Poetteringgenerated type s
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering ::= type s2, s1 | c | c (a; a : t; b : t; d : t) | c (a)?
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering{pred __<__ : a * a
a07fdfa376add41d9101d39db25fb2ecb17d5fcaLennart Poettering ::= type s2, s1 |
a07fdfa376add41d9101d39db25fb2ecb17d5fcaLennart Poettering c (a; a : t; b : t; d : t) |
f801968466fed39d50d410b30ac828c26722cc95Lennart Poettering c (a)? %(bla1)%
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poettering %(after-sort)%
98a77df5fe8591034c48e5d56d903ee268de37f9Lennart Poetteringops a : b; %(bla4)%
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poettering c : d %(bla5)%
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poetteringvars a : t; a, b : s
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poettering%(bla8-ignored)%
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poettering. a = a; %(a2)%
b5b46d599524341ddd7407e5dff1021af8ff5089Lennart Poettering. a = a; %(f1)%
5e8b28838e493b59628322b69580097ef7dd9384Lennart Poetteringtypes s, abcdefghijlklmnopqrstuvwxyz, ABCDEFGHIJKLMONOPQRSTUVWXYZ,
d87be9b0af81a6e07d4fb3028e45c4409100dc26Lennart Poettering ����������������������������������������������������������, abc,
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering a_b_c, ab2, ab_2_3_a, a', a'b''2
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringop __+-*/\&=<>!?:.$@#^~�����������������|__ : s * s -> s
cb7ed9dfca647198bce95f503552710eae22da37Lennart Poettering %% NO-BRACKET-SIGNs
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringops 'a', '\"', '\\', '\n', '\000', '\255', '\x00', '\xFF',
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering '\o000', '\o377', '^', '1', '2', '3', '4', '5', '6', '7', '8', '9',
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering '0', '�', '!', '�', '$', '&', '/', '(', ')', '=', '?', '\\' : s
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringops 1, 2, 3, 4 : s;
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering __@@__, __exp__, __frac__ : s * s -> s
7560fffcd2531786b9c1ca657667a43e90331326Lennart Poettering. def 12.34E+34
7560fffcd2531786b9c1ca657667a43e90331326Lennart Poettering. def 12.34E-34
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering. true %(The true formula)%
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering along several lines!
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering and with special stuff: -*/\&=<>BCDEFGHIJKLM!% )%
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poetteringop __and'__ : s
0790b9fed42eefc4e22dbbe2337cba9713b7848cLennart Poetteringtypes a, b, c, d < e
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poetteringtypes a = b = c = d = e
df1c8f6ac8a45913104b5eeb44f4574689fedd50Lennart Poetteringtype a = {x : b . true}
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart Poetteringops c : s * s -> s, assoc, comm, idem, unit a;
fd4d89b2c0b31da01d134301e30916931ae3c7d9Lennart Poettering c : s * s * s -> s
8230e26dc954a40d8c9dbc8ddd9376117021f9d2Lennart Poetteringop c : s * s ->? s, assoc, comm, idem, unit a;
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poetteringop c : s * s * s ->? s
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poetteringop c(x : s; y : s; z : t) : s = a;
4d9909c93e9c58789c71b34555a1908307c6849eLennart Poetteringop c(x : s; y : s; z : t) :? s = a;
88a6c5894c9d3f85d63b87b040c130366b4006ceKay Sieverspreds c : s * s;
6a7353684b65f0107cbdfa0a16ab7717ba257b61Lennart Poetteringpred c(x : s; y : s; z : t) <=> false;
6a7353684b65f0107cbdfa0a16ab7717ba257b61Lennart Poetteringtype Data1 ::= a | b | c
6b78f9b4354010f8af2fe48c783ffd52b2db8f57Lennart Poettering ::= Cons21 (Data1; Data2) | Cons22 (Data2; Data1) | type Data1
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart Poettering ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart Poettering Cons32 (sel2 :? Data2; sel1 :? Data1)
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering Cons42 (sel2 :? Data2; sel1 : ? Data1)?
b7def684941808600c344f0be7a2b9fcdda97e0fLennart Poetteringtypes Data1, Data2, Data3
b7def684941808600c344f0be7a2b9fcdda97e0fLennart Poetteringtypes Tree ::= Leaf Data1 | Forest;
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering Forest ::= Nil | Cons (Tree; Forest)
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poetteringfree type List ::= Nil | Cons (Data1; List)
c649f72baed31c54c8384c3ca1d203fab6e98d08David Straussgenerated type Set ::= Mt | Add (Data1; Set)
c649f72baed31c54c8384c3ca1d203fab6e98d08David Straussgenerated type Set ::= Mt | Add (Data1; Set)
be0aa78406c73a6625308dc0672b5ff27ec6f9a8Lennart Poettering succ : nat -> nat
9946996cda11a18b44d82344676e5a0e96339408Lennart Poetteringops f, g : s ->? s;
9946996cda11a18b44d82344676e5a0e96339408Lennart Poettering __+__, __-__, __*__, __/__ : s * s -> s;
b4efdf97203ddf781c17f77be84cc61516a077d2Lennart Poetteringvars x, y, z : s; r1, r2 : t
eeb875144e5a80d0521461a139f13fc8014d77d8Lennart Poettering. not p /\ not q (x) /\ q (x)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering. not p \/ not q (x) \/ q (x)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering. not p /\ not q (x) /\ q (x) => not p \/ not q (x) \/ q (x) => not
edca2e2348b314e2d892fe6f8ae276fdc223f014Thomas Hindoe Paaboel Andersen p /\ not q (x) /\ q (x)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering. not p /\ not q (x) /\ q (x)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering not p \/ not q (x) \/ q (x)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers not p /\ not q (x) /\ q (x)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers forall x : s
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers . not p /\ not q (x) /\ q (x) <=>
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers exists x : s
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers . not p \/ not q (x) \/ q (x) <=>
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers exists! x : s . not p /\ not q (x) /\ q (x)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers. f (x) =e= g (x)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers. f (x) = g (x)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers. def g (x) : t
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers. def g (x) as s
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers. def ((op f : s ->? s)) (x)
166503dada92d7ca3570a653e07a51ed826b7c8aLennart Poettering. def ((op g : s -> t)) (x)
59cea26a349cfa8db906b520dac72563dd773ff2Lennart Poettering. ((pred p : ()))
35eb6b124ebdf82bd77aad6e44962a9a039c4d33Lennart Poettering. ((pred q : s)) (x)
9473414219330b9febc1d0712bbf49ad74cf962fLennart Poettering. def x * y * z + z * y * x
7b63bde1ed0d4f30c799c9b4737fa926465929f9Lennart Poettering. exists! x : s . e;
7b63bde1ed0d4f30c799c9b4737fa926465929f9Lennart Poetteringforall x : s . e;
5b40d33761376354116a8cddb9b9fbdb6c4727d6Lennart Poetteringfree type Boolean ::= True | False
5b40d33761376354116a8cddb9b9fbdb6c4727d6Lennart Poetteringops Not__ : Boolean -> Boolean;
f7f21d33db5dfe88dc8175c61dada44013347729Lennart Poettering __And__, __Or__ : Boolean * Boolean -> Boolean
f7f21d33db5dfe88dc8175c61dada44013347729Lennart Poetteringforall x, y, z : Boolean
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering. Not (False) = True %(Not_False)%
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering. Not (True) = False %(Not_True)%
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering. False And False = False %(And_def1)%
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering. False And True = False %(And_def2)%
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering. True And False = False %(And_def3)%
a26336da875a6657d404d1e44b86ae067c34b110Kay Sievers. True And True = True %(And_def4)%
a26336da875a6657d404d1e44b86ae067c34b110Kay Sievers. x Or y = Not (Not (x) And Not (y)); %(Or_def)%
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringops chr : Nat ->? Char;
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering ord : Char -> Nat
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart Poetteringforall n : Nat; c : Char
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart Poettering. def chr (n) <=> n <= 255 %(chr_dom)%
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering. chr (ord (c)) = c %(chr_def)%
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering. ord (chr (n)) = n if n <= 255; %(ord_def)%
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering%% definition of individual characters:
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poetteringops '\000' : Char = chr (0); %(slash_000)%
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering '\001' : Char = chr (1); %(slash_001)%
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poettering '\002' : Char = chr (2); %(slash_002)%
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poettering '\003' : Char = chr (3); %(slash_003)%
7e2668c6fd5720ae4d2d55eb8a062739687516afLennart Poettering '\004' : Char = chr (4); %(slash_004)%
7e2668c6fd5720ae4d2d55eb8a062739687516afLennart Poettering '\005' : Char = chr (5); %(slash_005)%
e85647f73e235c2a6ea412cb8d841e092c373501Lennart Poettering '\006' : Char = chr (6); %(slash_006)%
e85647f73e235c2a6ea412cb8d841e092c373501Lennart Poettering '\007' : Char = chr (7); %(slash_007)%
e01a15b71e18bf2008aec7e75041ffa42eb80b80Kay Sievers '\008' : Char = chr (8); %(slash_008)%
a888b352eb53b07daa24fa859ceeb254336b293dLennart Poettering '\009' : Char = chr (9); %(slash_009)%
3b2d5b02ae231f1d3eb0d96eb980155d7797304eLennart Poettering '\010' : Char = chr (10); %(slash_010)%
3b2d5b02ae231f1d3eb0d96eb980155d7797304eLennart Poettering '\011' : Char = chr (11); %(slash_011)%
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering '\012' : Char = chr (12); %(slash_012)%
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering '\013' : Char = chr (13); %(slash_013)%
3d9a412243035beeaaf3465a62065444a5adf21cLennart Poettering '\014' : Char = chr (14); %(slash_014)%
3d9a412243035beeaaf3465a62065444a5adf21cLennart Poettering '\015' : Char = chr (15); %(slash_015)%
98ef27df896f36f0407eaa7ed9e295203b9c271bLennart Poettering '\016' : Char = chr (16); %(slash_016)%
a0a3844815b0f346dba03f41245c620f432e462fLennart Poettering '\017' : Char = chr (17); %(slash_017)%
4ee717820208a4c8e92383d0dbefa401827fab38Kay Sievers '\018' : Char = chr (18); %(slash_018)%
4ee717820208a4c8e92383d0dbefa401827fab38Kay Sievers '\019' : Char = chr (19); %(slash_019)%
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sievers '\020' : Char = chr (20); %(slash_020)%
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sievers '\021' : Char = chr (21); %(slash_021)%
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sievers '\022' : Char = chr (22); %(slash_022)%
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers '\023' : Char = chr (23); %(slash_023)%
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers '\024' : Char = chr (24); %(slash_024)%
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers '\025' : Char = chr (25); %(slash_025)%
b8217b7bd5fd171916a095b150fad4c3a37f5a41Kay Sievers '\026' : Char = chr (26); %(slash_026)%
08f23fd29c9df9c8b4e874933eb39711f069754bLennart Poettering '\027' : Char = chr (27); %(slash_027)%
08f23fd29c9df9c8b4e874933eb39711f069754bLennart Poettering '\028' : Char = chr (28); %(slash_028)%
18b754d345ecb0b15e369978aaffa72e9814b86aKay Sievers '\029' : Char = chr (29); %(slash_029)%
068665b6fd9839f27bcace7e8f56c0baa6935272Lennart Poettering '\030' : Char = chr (30); %(slash_030)%
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering '\031' : Char = chr (31); %(slash_031)%
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering '\032' : Char = chr (32); %(slash_032)%
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart Poettering '\033' : Char = chr (33); %(slash_033)%
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart Poettering '\034' : Char = chr (34); %(slash_034)%
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart Poettering '\035' : Char = chr (35); %(slash_035)%
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart Poettering '\036' : Char = chr (36); %(slash_036)%
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poettering '\037' : Char = chr (37); %(slash_037)%
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poettering '\038' : Char = chr (38); %(slash_038)%
18da49531e4c6b31bd2439b4d738dc1bb9660af1Lennart Poettering '\039' : Char = chr (39); %(slash_039)%
18da49531e4c6b31bd2439b4d738dc1bb9660af1Lennart Poettering '\040' : Char = chr (40); %(slash_040)%
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poettering '\041' : Char = chr (41); %(slash_041)%
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poettering '\042' : Char = chr (42); %(slash_042)%
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poettering '\043' : Char = chr (43); %(slash_043)%
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poettering '\044' : Char = chr (44); %(slash_044)%
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poettering '\045' : Char = chr (45); %(slash_045)%
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poettering '\046' : Char = chr (46); %(slash_046)%
edca2e2348b314e2d892fe6f8ae276fdc223f014Thomas Hindoe Paaboel Andersen '\047' : Char = chr (47); %(slash_047)%
101f077676e9fbe1a66c8b2dc4864a8d7a94c372Lennart Poettering '\048' : Char = chr (48); %(slash_048)%
f7f964eb3625e4cca7f16377fa12aa7a760243e7Lennart Poettering '\049' : Char = chr (49); %(slash_049)%
f7f964eb3625e4cca7f16377fa12aa7a760243e7Lennart Poettering '\050' : Char = chr (50); %(slash_050)%
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering '\051' : Char = chr (51); %(slash_051)%
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering '\052' : Char = chr (52); %(slash_052)%
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering '\053' : Char = chr (53); %(slash_053)%
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering '\054' : Char = chr (54); %(slash_054)%
53ed2eeb2e709a6c0d152d7bdf2d9a4b9f997a16Lennart Poettering '\055' : Char = chr (55); %(slash_055)%
53ed2eeb2e709a6c0d152d7bdf2d9a4b9f997a16Lennart Poettering '\056' : Char = chr (56); %(slash_056)%
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart Poettering '\057' : Char = chr (57); %(slash_057)%
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart Poettering '\058' : Char = chr (58); %(slash_058)%
a6e87e90ede66815989ba2db92a07102a69906feLennart Poettering '\059' : Char = chr (59); %(slash_059)%
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering '\060' : Char = chr (60); %(slash_060)%
c4aa65e7147dc742886edf25593e10466b02fc3aLennart Poettering '\061' : Char = chr (61); %(slash_061)%
7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart Poettering '\062' : Char = chr (62); %(slash_062)%
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering '\063' : Char = chr (63); %(slash_063)%
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering '\064' : Char = chr (64); %(slash_064)%
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering '\065' : Char = chr (65); %(slash_065)%
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering '\066' : Char = chr (66); %(slash_066)%
05aa9edde0f9f4077b8120389c93cb0134eda9c5Lennart Poettering '\067' : Char = chr (67); %(slash_067)%
05aa9edde0f9f4077b8120389c93cb0134eda9c5Lennart Poettering '\068' : Char = chr (68); %(slash_068)%
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering '\069' : Char = chr (69); %(slash_069)%
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering '\070' : Char = chr (70); %(slash_070)%
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering '\071' : Char = chr (71); %(slash_071)%
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering '\072' : Char = chr (72); %(slash_072)%
5ba081b0fb02380cee4c2ff5bc7e05f869eb8415Lennart Poettering '\073' : Char = chr (73); %(slash_073)%
5ba081b0fb02380cee4c2ff5bc7e05f869eb8415Lennart Poettering '\074' : Char = chr (74); %(slash_074)%
b3fa47e0819b08ea32e69e19e6d88ce2daca069dLennart Poettering '\075' : Char = chr (75); %(slash_075)%
b3fa47e0819b08ea32e69e19e6d88ce2daca069dLennart Poettering '\076' : Char = chr (76); %(slash_076)%
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poettering '\077' : Char = chr (77); %(slash_077)%
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poettering '\078' : Char = chr (78); %(slash_078)%
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poettering '\079' : Char = chr (79); %(slash_079)%
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poettering '\080' : Char = chr (80); %(slash_080)%
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poettering '\081' : Char = chr (81); %(slash_081)%
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poettering '\082' : Char = chr (82); %(slash_082)%
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart Poettering '\083' : Char = chr (83); %(slash_083)%
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart Poettering '\084' : Char = chr (84); %(slash_084)%
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers '\085' : Char = chr (85); %(slash_085)%
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers '\086' : Char = chr (86); %(slash_086)%
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers '\087' : Char = chr (87); %(slash_087)%
a2f5666d06fe8233025738047115bb9e3959df3eLennart Poettering '\088' : Char = chr (88); %(slash_088)%
a2f5666d06fe8233025738047115bb9e3959df3eLennart Poettering '\089' : Char = chr (89); %(slash_089)%
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poettering '\090' : Char = chr (90); %(slash_090)%
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poettering '\091' : Char = chr (91); %(slash_091)%
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart Poettering '\092' : Char = chr (92); %(slash_092)%
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart Poettering '\093' : Char = chr (93); %(slash_093)%
de6c78f8795743894431a099d26ec562a8acf3dfLennart Poettering '\094' : Char = chr (94); %(slash_094)%
7d441ddb5ca090b5a97f58ac4b4d97b3e84fa81eLennart Poettering '\095' : Char = chr (95); %(slash_095)%
14e639ae7a1dbf156273ce697d30fbc6c6594209Lennart Poettering '\096' : Char = chr (96); %(slash_096)%
14e639ae7a1dbf156273ce697d30fbc6c6594209Lennart Poettering '\097' : Char = chr (97); %(slash_097)%
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering '\098' : Char = chr (98); %(slash_098)%
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering '\099' : Char = chr (99); %(slash_099)%
d3c7d7dd77b2b72315164b672462825cef6c0f9aKay Sievers '\100' : Char = chr (100); %(slash_100)%
72b9ed828bd22f3ddd74b6853c183eebf006d6d8Lennart Poettering '\101' : Char = chr (101); %(slash_101)%
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering '\102' : Char = chr (102); %(slash_102)%
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering '\103' : Char = chr (103); %(slash_103)%
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering '\104' : Char = chr (104); %(slash_104)%
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering '\105' : Char = chr (105); %(slash_105)%
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering '\106' : Char = chr (106); %(slash_106)%
97f73ffb04947acf0a5854e3a7bdbb7a0105f6faLennart Poettering '\107' : Char = chr (107); %(slash_107)%
97f73ffb04947acf0a5854e3a7bdbb7a0105f6faLennart Poettering '\108' : Char = chr (108); %(slash_108)%
85f248b26653f5322c26735661d63d4e8460c30eLennart Poettering '\109' : Char = chr (109); %(slash_109)%
85f248b26653f5322c26735661d63d4e8460c30eLennart Poettering '\110' : Char = chr (110); %(slash_110)%
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering '\111' : Char = chr (111); %(slash_111)%
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering '\112' : Char = chr (112); %(slash_112)%
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering '\113' : Char = chr (113); %(slash_113)%
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poettering '\114' : Char = chr (114); %(slash_114)%
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poettering '\115' : Char = chr (115); %(slash_115)%
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering '\116' : Char = chr (116); %(slash_116)%
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering '\117' : Char = chr (117); %(slash_117)%
7c697168102cb64c5cb65a542959684014da99c7Lennart Poettering '\118' : Char = chr (118); %(slash_118)%
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart Poettering '\119' : Char = chr (119); %(slash_119)%
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering '\120' : Char = chr (120); %(slash_120)%
8d0e38a2b966799af884e78a54fd6a2dffa44788Lennart Poettering '\121' : Char = chr (121); %(slash_121)%
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering '\122' : Char = chr (122); %(slash_122)%
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering '\123' : Char = chr (123); %(slash_123)%
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering '\124' : Char = chr (124); %(slash_124)%
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering '\125' : Char = chr (125); %(slash_125)%
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering '\126' : Char = chr (126); %(slash_126)%
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering '\127' : Char = chr (127); %(slash_127)%
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering '\128' : Char = chr (128); %(slash_128)%
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering '\129' : Char = chr (129); %(slash_129)%
916abb21d0a6653e0187b91591e492026886b0a4Lennart Poettering '\130' : Char = chr (130); %(slash_130)%
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering '\131' : Char = chr (131); %(slash_131)%
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering '\132' : Char = chr (132); %(slash_132)%
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering '\133' : Char = chr (133); %(slash_133)%
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering '\134' : Char = chr (134); %(slash_134)%
9534ce54858c67363b841cdbdc315140437bfdb4Lennart Poettering '\135' : Char = chr (135); %(slash_135)%
9534ce54858c67363b841cdbdc315140437bfdb4Lennart Poettering '\136' : Char = chr (136); %(slash_136)%
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering '\137' : Char = chr (137); %(slash_137)%
796b06c21b62d13c9021e2fbd9c58a5c6edb2764Kay Sievers '\138' : Char = chr (138); %(slash_138)%
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering '\139' : Char = chr (139); %(slash_139)%
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering '\140' : Char = chr (140); %(slash_140)%
7a2a0b907b5cc60f5d9a871997d7d6e7f62bf4d8Lennart Poettering '\141' : Char = chr (141); %(slash_141)%
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart Poettering '\142' : Char = chr (142); %(slash_142)%
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart Poettering '\143' : Char = chr (143); %(slash_143)%
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart Poettering '\144' : Char = chr (144); %(slash_144)%
8bbabc447b1d913bd21faf97c7b17d20d315d2b4Lennart Poettering '\145' : Char = chr (145); %(slash_145)%
f530371f1f85a070d7d0fb5112146a43533ae00bLennart Poettering '\146' : Char = chr (146); %(slash_146)%
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering '\147' : Char = chr (147); %(slash_147)%
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering '\148' : Char = chr (148); %(slash_148)%
a73d88fa024b5668ed7dde681e99547d41e6a864Lennart Poettering '\149' : Char = chr (149); %(slash_149)%
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poettering '\150' : Char = chr (150); %(slash_150)%
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart Poettering '\151' : Char = chr (151); %(slash_151)%
44143309dd0b37d61d7d842ca58f01a65646ec71Kay Sievers '\152' : Char = chr (152); %(slash_152)%
3d57c6ab801f4437f12948e29589e3d00c3ad9dbLennart Poettering '\153' : Char = chr (153); %(slash_153)%
935fb723ba7370abaf793914fb5a722f7f5e41e1Lennart Poettering '\154' : Char = chr (154); %(slash_154)%
b9a2a36b519ccd79c4198e7dda4e657d597a14adLennart Poettering '\155' : Char = chr (155); %(slash_155)%
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poettering '\156' : Char = chr (156); %(slash_156)%
9408a2d295a312a5472345090e28e0502570494bLennart Poettering '\157' : Char = chr (157); %(slash_157)%
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering '\158' : Char = chr (158); %(slash_158)%
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sievers '\159' : Char = chr (159); %(slash_159)%
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart Poettering '\160' : Char = chr (160); %(slash_160)%
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart Poettering '\161' : Char = chr (161); %(slash_161)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering '\162' : Char = chr (162); %(slash_162)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering '\163' : Char = chr (163); %(slash_163)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering '\164' : Char = chr (164); %(slash_164)%
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poettering '\165' : Char = chr (165); %(slash_165)%
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering '\166' : Char = chr (166); %(slash_166)%
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering '\167' : Char = chr (167); %(slash_167)%