0 | 0 | kvanti |
1 | 0 | lemma uniqueMember |
2 | 0 | lemma uniqueMember(Type) |
3 | 0 | lemma sameSeries |
4 | 0 | lemma a4 |
5 | 0 | lemma sameMember |
6 | 0 | 1rule Qclosed(Addition) |
7 | 0 | 1rule Qclosed(Multiplication) |
8 | 0 | 1rule fromCartProd(1) |
9 | 0 | 1rule fromCartProd(2) |
10 | 1 | constantRationalSeries( {MissingArg} ) |
11 | 2 | cartProd( {MissingArg} , {MissingArg} ) |
12 | 1 | P( {MissingArg} ) |
13 | 2 | binaryUnion( {MissingArg} , {MissingArg} ) |
14 | 0 | setOfRationalSeries |
15 | 2 | isSubset( {MissingArg} , {MissingArg} ) |
16 | 2 | (p {MissingArg} , {MissingArg} ) |
17 | 1 | (s {MissingArg} ) |
18 | 0 | cdots |
19 | 0 | object-var |
20 | 0 | ex-var |
21 | 0 | ph-var |
22 | 0 | vaerdi |
23 | 0 | variabel |
24 | 1 | op {MissingArg} end op |
25 | 2 | op2 {MissingArg} comma {MissingArg} end op2 |
26 | 2 | define-equal {MissingArg} comma {MissingArg} end equal |
27 | 1 | contains-empty {MissingArg} end empty |
28 | 1 | Nat( {MissingArg} ) |
29 | 2 | 1deduction {MissingArg} conclude {MissingArg} end 1deduction |
30 | 2 | 1deduction zero {MissingArg} conclude {MissingArg} end 1deduction |
31 | 3 | 1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction |
32 | 3 | 1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction |
33 | 3 | 1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction |
34 | 4 | 1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction |
35 | 4 | 1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction |
36 | 4 | 1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction |
37 | 3 | 1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction |
38 | 4 | 1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction |
39 | 4 | 1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction |
40 | 1 | 1deduction seven {MissingArg} end 1deduction |
41 | 2 | 1deduction eight {MissingArg} bound {MissingArg} end 1deduction |
42 | 2 | 1deduction eight star {MissingArg} bound {MissingArg} end 1deduction |
43 | 0 | ex1 |
44 | 0 | ex2 |
45 | 0 | ex3 |
46 | 0 | ex10 |
47 | 0 | ex20 |
48 | 1 | existential var {MissingArg} end var |
49 | 1 | {MissingArg} is existential var |
50 | 4 | exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
51 | 4 | exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
52 | 4 | exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
53 | 4 | exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
54 | 0 | ph1 |
55 | 0 | ph2 |
56 | 0 | ph3 |
57 | 1 | placeholder-var {MissingArg} end var |
58 | 1 | {MissingArg} is placeholder-var |
59 | 4 | ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
60 | 4 | ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
61 | 4 | ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
62 | 4 | ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
63 | 4 | meta-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
64 | 4 | meta-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
65 | 4 | meta-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub |
66 | 0 | var big set |
67 | 0 | object big set |
68 | 0 | meta big set |
69 | 0 | zermelo empty set |
70 | 0 | system Q |
71 | 0 | 1rule mp |
72 | 0 | 1rule gen |
73 | 0 | 1rule repetition |
74 | 0 | 1rule ad absurdum |
75 | 0 | 1rule deduction |
76 | 0 | 1rule exist intro |
77 | 0 | axiom extensionality |
78 | 0 | axiom empty set |
79 | 0 | axiom pair definition |
80 | 0 | axiom union definition |
81 | 0 | axiom power definition |
82 | 0 | axiom separation definition |
83 | 0 | prop lemma add double neg |
84 | 0 | prop lemma remove double neg |
85 | 0 | prop lemma and commutativity |
86 | 0 | prop lemma auto imply |
87 | 0 | prop lemma contrapositive |
88 | 0 | prop lemma first conjunct |
89 | 0 | prop lemma second conjunct |
90 | 0 | prop lemma from contradiction |
91 | 0 | prop lemma from disjuncts |
92 | 0 | prop lemma iff commutativity |
93 | 0 | prop lemma iff first |
94 | 0 | prop lemma iff second |
95 | 0 | prop lemma imply transitivity |
96 | 0 | prop lemma join conjuncts |
97 | 0 | prop lemma mp2 |
98 | 0 | prop lemma mp3 |
99 | 0 | prop lemma mp4 |
100 | 0 | prop lemma mp5 |
101 | 0 | prop lemma mt |
102 | 0 | prop lemma negative mt |
103 | 0 | prop lemma technicality |
104 | 0 | prop lemma weakening |
105 | 0 | prop lemma weaken or first |
106 | 0 | prop lemma weaken or second |
107 | 0 | lemma formula2pair |
108 | 0 | lemma pair2formula |
109 | 0 | lemma formula2union |
110 | 0 | lemma union2formula |
111 | 0 | lemma formula2separation |
112 | 0 | lemma separation2formula |
113 | 0 | lemma formula2power |
114 | 0 | lemma subset in power set |
115 | 0 | lemma power set is subset0 |
116 | 0 | lemma power set is subset |
117 | 0 | lemma power set is subset0-switch |
118 | 0 | lemma power set is subset-switch |
119 | 0 | lemma set equality suff condition |
120 | 0 | lemma set equality suff condition(t)0 |
121 | 0 | lemma set equality suff condition(t) |
122 | 0 | lemma set equality skip quantifier |
123 | 0 | lemma set equality nec condition |
124 | 0 | lemma reflexivity0 |
125 | 0 | lemma reflexivity |
126 | 0 | lemma symmetry0 |
127 | 0 | lemma symmetry |
128 | 0 | lemma transitivity0 |
129 | 0 | lemma transitivity |
130 | 0 | lemma er is reflexive |
131 | 0 | lemma er is symmetric |
132 | 0 | lemma er is transitive |
133 | 0 | lemma empty set is subset |
134 | 0 | lemma member not empty0 |
135 | 0 | lemma member not empty |
136 | 0 | lemma unique empty set0 |
137 | 0 | lemma unique empty set |
138 | 0 | lemma ==Reflexivity |
139 | 0 | lemma ==Symmetry |
140 | 0 | lemma ==Transitivity0 |
141 | 0 | lemma ==Transitivity |
142 | 0 | lemma transfer ~is0 |
143 | 0 | lemma transfer ~is |
144 | 0 | lemma pair subset0 |
145 | 0 | lemma pair subset1 |
146 | 0 | lemma pair subset |
147 | 0 | lemma same pair |
148 | 0 | lemma same singleton |
149 | 0 | lemma union subset |
150 | 0 | lemma same union |
151 | 0 | lemma separation subset |
152 | 0 | lemma same separation |
153 | 0 | lemma same binary union |
154 | 0 | lemma intersection subset |
155 | 0 | lemma same intersection |
156 | 0 | lemma auto member |
157 | 0 | lemma eq-system not empty0 |
158 | 0 | lemma eq-system not empty |
159 | 0 | lemma eq subset0 |
160 | 0 | lemma eq subset |
161 | 0 | lemma equivalence nec condition0 |
162 | 0 | lemma equivalence nec condition |
163 | 0 | lemma none-equivalence nec condition0 |
164 | 0 | lemma none-equivalence nec condition1 |
165 | 0 | lemma none-equivalence nec condition |
166 | 0 | lemma equivalence class is subset |
167 | 0 | lemma equivalence classes are disjoint |
168 | 0 | lemma all disjoint |
169 | 0 | lemma all disjoint-imply |
170 | 0 | lemma bs subset union(bs/r) |
171 | 0 | lemma union(bs/r) subset bs |
172 | 0 | lemma union(bs/r) is bs |
173 | 0 | theorem eq-system is partition |
174 | 0 | var x1 |
175 | 0 | var x2 |
176 | 0 | var y1 |
177 | 0 | var y2 |
178 | 0 | var v1 |
179 | 0 | var v2 |
180 | 0 | var v3 |
181 | 0 | var v4 |
182 | 0 | var v2n |
183 | 0 | var m1 |
184 | 0 | var m2 |
185 | 0 | var n1 |
186 | 0 | var n2 |
187 | 0 | var n3 |
188 | 0 | var ep |
189 | 0 | var ep1 |
190 | 0 | var ep2 |
191 | 0 | var fep |
192 | 0 | var fx |
193 | 0 | var fy |
194 | 0 | var fz |
195 | 0 | var fu |
196 | 0 | var fv |
197 | 0 | var fw |
198 | 0 | var rx |
199 | 0 | var ry |
200 | 0 | var rz |
201 | 0 | var ru |
202 | 0 | var sx |
203 | 0 | var sx1 |
204 | 0 | var sy |
205 | 0 | var sy1 |
206 | 0 | var sz |
207 | 0 | var sz1 |
208 | 0 | var su |
209 | 0 | var su1 |
210 | 0 | var fxs |
211 | 0 | var fys |
212 | 0 | var crs1 |
213 | 0 | var f1 |
214 | 0 | var f2 |
215 | 0 | var f3 |
216 | 0 | var f4 |
217 | 0 | var op1 |
218 | 0 | var op2 |
219 | 0 | var r1 |
220 | 0 | var s1 |
221 | 0 | var s2 |
222 | 0 | meta x1 |
223 | 0 | meta x2 |
224 | 0 | meta y1 |
225 | 0 | meta y2 |
226 | 0 | meta v1 |
227 | 0 | meta v2 |
228 | 0 | meta v3 |
229 | 0 | meta v4 |
230 | 0 | meta v2n |
231 | 0 | meta m1 |
232 | 0 | meta m2 |
233 | 0 | meta n1 |
234 | 0 | meta n2 |
235 | 0 | meta n3 |
236 | 0 | meta ep |
237 | 0 | meta ep1 |
238 | 0 | meta ep2 |
239 | 0 | meta fx |
240 | 0 | meta fy |
241 | 0 | meta fz |
242 | 0 | meta fu |
243 | 0 | meta fv |
244 | 0 | meta fw |
245 | 0 | meta fep |
246 | 0 | meta rx |
247 | 0 | meta ry |
248 | 0 | meta rz |
249 | 0 | meta ru |
250 | 0 | meta sx |
251 | 0 | meta sx1 |
252 | 0 | meta sy |
253 | 0 | meta sy1 |
254 | 0 | meta sz |
255 | 0 | meta sz1 |
256 | 0 | meta su |
257 | 0 | meta su1 |
258 | 0 | meta fxs |
259 | 0 | meta fys |
260 | 0 | meta f1 |
261 | 0 | meta f2 |
262 | 0 | meta f3 |
263 | 0 | meta f4 |
264 | 0 | meta op1 |
265 | 0 | meta op2 |
266 | 0 | meta r1 |
267 | 0 | meta s1 |
268 | 0 | meta s2 |
269 | 0 | object ep |
270 | 0 | object crs1 |
271 | 0 | object f1 |
272 | 0 | object f2 |
273 | 0 | object f3 |
274 | 0 | object f4 |
275 | 0 | object n1 |
276 | 0 | object n2 |
277 | 0 | object op1 |
278 | 0 | object op2 |
279 | 0 | object r1 |
280 | 0 | object s1 |
281 | 0 | object s2 |
282 | 0 | ph4 |
283 | 0 | ph5 |
284 | 0 | ph6 |
285 | 0 | NAT |
286 | 0 | RATIONAL_SERIES |
287 | 0 | SERIES |
288 | 0 | setOfReals |
289 | 0 | setOfFxs |
290 | 0 | N |
291 | 0 | Q |
292 | 0 | X |
293 | 0 | xs |
294 | 0 | xsF |
295 | 0 | ysF |
296 | 0 | us |
297 | 0 | usF |
298 | 0 | 0 |
299 | 0 | 1 |
300 | 0 | (-1) |
301 | 0 | 2 |
302 | 0 | 3 |
303 | 0 | 1/2 |
304 | 0 | 1/3 |
305 | 0 | 2/3 |
306 | 0 | 0f |
307 | 0 | 1f |
308 | 0 | 00 |
309 | 0 | 01 |
310 | 0 | (--01) |
311 | 0 | 02 |
312 | 0 | 01//02 |
313 | 0 | lemma plusAssociativity(R) |
314 | 0 | lemma plusAssociativity(R)XX |
315 | 0 | lemma plus0(R) |
316 | 0 | lemma negative(R) |
317 | 0 | lemma times1(R) |
318 | 0 | lemma lessAddition(R) |
319 | 0 | lemma plusCommutativity(R) |
320 | 0 | lemma leqAntisymmetry(R) |
321 | 0 | lemma leqTransitivity(R) |
322 | 0 | lemma leqAddition(R) |
323 | 0 | lemma distribution(R) |
324 | 0 | axiom a4 |
325 | 0 | axiom induction |
326 | 0 | axiom equality |
327 | 0 | axiom eqLeq |
328 | 0 | axiom eqAddition |
329 | 0 | axiom eqMultiplication |
330 | 0 | axiom QisClosed(reciprocal) |
331 | 0 | lemma QisClosed(reciprocal) |
332 | 0 | axiom QisClosed(negative) |
333 | 0 | lemma QisClosed(negative) |
334 | 0 | axiom leqReflexivity |
335 | 0 | axiom leqAntisymmetry |
336 | 0 | axiom leqTransitivity |
337 | 0 | axiom leqTotality |
338 | 0 | axiom leqAddition |
339 | 0 | axiom leqMultiplication |
340 | 0 | axiom plusAssociativity |
341 | 0 | axiom plusCommutativity |
342 | 0 | axiom negative |
343 | 0 | axiom plus0 |
344 | 0 | axiom timesAssociativity |
345 | 0 | axiom timesCommutativity |
346 | 0 | axiom reciprocal |
347 | 0 | axiom times1 |
348 | 0 | axiom distribution |
349 | 0 | axiom 0not1 |
350 | 0 | lemma eqLeq(R) |
351 | 0 | lemma timesAssociativity(R) |
352 | 0 | lemma timesCommutativity(R) |
353 | 0 | 1rule adhoc sameR |
354 | 0 | lemma separation2formula(1) |
355 | 0 | lemma separation2formula(2) |
356 | 0 | axiom cauchy |
357 | 0 | axiom plusF |
358 | 0 | axiom reciprocalF |
359 | 0 | 1rule from== |
360 | 0 | 1rule to== |
361 | 0 | 1rule fromInR |
362 | 0 | lemma plusR(Sym) |
363 | 0 | axiom reciprocalR |
364 | 0 | 1rule lessMinus1(N) |
365 | 0 | axiom nonnegative(N) |
366 | 0 | axiom US0 |
367 | 0 | 1rule nextXS(upperBound) |
368 | 0 | 1rule nextXS(noUpperBound) |
369 | 0 | 1rule nextUS(upperBound) |
370 | 0 | 1rule nextUS(noUpperBound) |
371 | 0 | 1rule expZero |
372 | 0 | 1rule expPositive |
373 | 0 | 1rule expZero(R) |
374 | 0 | 1rule expPositive(R) |
375 | 0 | 1rule base(1/2)Sum zero |
376 | 0 | 1rule base(1/2)Sum positive |
377 | 0 | 1rule UStelescope zero |
378 | 0 | 1rule UStelescope positive |
379 | 0 | 1rule adhoc eqAddition(R) |
380 | 0 | 1rule fromLimit |
381 | 0 | 1rule toUpperBound |
382 | 0 | 1rule fromUpperBound |
383 | 0 | axiom USisUpperBound |
384 | 0 | axiom 0not1(R) |
385 | 0 | 1rule expUnbounded |
386 | 0 | 1rule fromLeq(Advanced)(N) |
387 | 0 | 1rule fromLeastUpperBound |
388 | 0 | 1rule toLeastUpperBound |
389 | 0 | axiom XSisNotUpperBound |
390 | 0 | axiom ysFGreater |
391 | 0 | axiom ysFLess |
392 | 0 | 1rule smallInverse |
393 | 0 | axiom natType |
394 | 0 | axiom rationalType |
395 | 0 | axiom seriesType |
396 | 0 | axiom max |
397 | 0 | axiom numerical |
398 | 0 | axiom numericalF |
399 | 0 | axiom memberOfSeries |
400 | 0 | prop lemma doubly conditioned join conjuncts |
401 | 0 | prop lemma imply negation |
402 | 0 | prop lemma tertium non datur |
403 | 0 | prop lemma from negated imply |
404 | 0 | prop lemma to negated imply |
405 | 0 | prop lemma from negated double imply |
406 | 0 | prop lemma from negated and |
407 | 0 | prop lemma from negated or |
408 | 0 | prop lemma to negated or |
409 | 0 | prop lemma from negations |
410 | 0 | prop lemma from three disjuncts |
411 | 0 | prop lemma from two times two disjuncts |
412 | 0 | prop lemma negate first disjunct |
413 | 0 | prop lemma negate second disjunct |
414 | 0 | prop lemma expand disjuncts |
415 | 0 | lemma set equality nec condition(1) |
416 | 0 | lemma set equality nec condition(2) |
417 | 0 | lemma lessLeq(R) |
418 | 0 | lemma memberOfSeries |
419 | 0 | lemma memberOfSeries(Type) |
420 | 2 | {MissingArg} ^ {MissingArg} |
421 | 1 | R( {MissingArg} ) |
422 | 1 | --R( {MissingArg} ) |
423 | 1 | 1/ {MissingArg} |
424 | 2 | eq-system of {MissingArg} modulo {MissingArg} |
425 | 2 | intersection {MissingArg} comma {MissingArg} end intersection |
426 | 2 | [ {MissingArg} ; {MissingArg} ] |
427 | 1 | union {MissingArg} end union |
428 | 2 | binary-union {MissingArg} comma {MissingArg} end union |
429 | 1 | power {MissingArg} end power |
430 | 1 | zermelo singleton {MissingArg} end singleton |
431 | 3 | stateExpand( {MissingArg} , {MissingArg} , {MissingArg} ) |
432 | 1 | extractSeries( {MissingArg} ) |
433 | 1 | setOfSeries( {MissingArg} ) |
434 | 1 | --Macro( {MissingArg} ) |
435 | 3 | expandList( {MissingArg} , {MissingArg} , {MissingArg} ) |
436 | 1 | **Macro( {MissingArg} ) |
437 | 1 | ++Macro( {MissingArg} ) |
438 | 1 |
< |
439 | 1 | ||Macro( {MissingArg} ) |
440 | 1 | 01//Macro( {MissingArg} ) |
441 | 2 | upperBound( {MissingArg} , {MissingArg} ) |
442 | 2 | leastUpperBound( {MissingArg} , {MissingArg} ) |
443 | 2 | base(1/2)Sum( {MissingArg} , {MissingArg} ) |
444 | 2 | UStelescope( {MissingArg} , {MissingArg} ) |
445 | 1 | ( {MissingArg} ) |
446 | 1 | |f {MissingArg} | |
447 | 1 | |r {MissingArg} | |
448 | 2 | limit( {MissingArg} , {MissingArg} ) |
449 | 1 | U( {MissingArg} ) |
450 | 3 | isOrderedPair( {MissingArg} , {MissingArg} , {MissingArg} ) |
451 | 3 | isRelation( {MissingArg} , {MissingArg} , {MissingArg} ) |
452 | 3 | isFunction( {MissingArg} , {MissingArg} , {MissingArg} ) |
453 | 2 | isSeries( {MissingArg} , {MissingArg} ) |
454 | 1 | isNatural( {MissingArg} ) |
455 | 2 | (o {MissingArg} , {MissingArg} ) |
456 | 1 | typeNat( {MissingArg} ) |
457 | 1 | typeNat0( {MissingArg} ) |
458 | 1 | typeRational( {MissingArg} ) |
459 | 1 | typeRational0( {MissingArg} ) |
460 | 2 | typeSeries( {MissingArg} , {MissingArg} ) |
461 | 2 | typeSeries0( {MissingArg} , {MissingArg} ) |
462 | 2 | zermelo pair {MissingArg} comma {MissingArg} end pair |
463 | 2 | zermelo ordered pair {MissingArg} comma {MissingArg} end pair |
464 | 1 | - {MissingArg} |
465 | 1 | -f {MissingArg} |
466 | 1 | -- {MissingArg} |
467 | 1 | 1f/ {MissingArg} |
468 | 1 | 01// {MissingArg} |
469 | 3 | {MissingArg} is related to {MissingArg} under {MissingArg} |
470 | 2 | {MissingArg} is reflexive relation in {MissingArg} |
471 | 2 | {MissingArg} is symmetric relation in {MissingArg} |
472 | 2 | {MissingArg} is transitive relation in {MissingArg} |
473 | 2 | {MissingArg} is equivalence relation in {MissingArg} |
474 | 3 | equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg} |
475 | 2 | {MissingArg} is partition of {MissingArg} |
476 | 2 | {MissingArg} * {MissingArg} |
477 | 2 | {MissingArg} *f {MissingArg} |
478 | 2 | {MissingArg} ** {MissingArg} |
479 | 2 | {MissingArg} + {MissingArg} |
480 | 2 | {MissingArg} - {MissingArg} |
481 | 2 | {MissingArg} +f {MissingArg} |
482 | 2 | {MissingArg} -f {MissingArg} |
483 | 2 | {MissingArg} ++ {MissingArg} |
484 | 2 | R( {MissingArg} ) -- R( {MissingArg} ) |
485 | 2 | {MissingArg} in0 {MissingArg} |
486 | 1 | | {MissingArg} | |
487 | 3 | if( {MissingArg} , {MissingArg} , {MissingArg} ) |
488 | 2 | max( {MissingArg} , {MissingArg} ) |
489 | 2 | maxR( {MissingArg} , {MissingArg} ) |
490 | 2 | {MissingArg} = {MissingArg} |
491 | 2 | {MissingArg} != {MissingArg} |
492 | 2 | {MissingArg} <= {MissingArg} |
493 | 2 | {MissingArg} < {MissingArg} |
494 | 2 |
{MissingArg} |
495 | 2 | {MissingArg} <=f {MissingArg} |
496 | 2 | {MissingArg} sameF {MissingArg} |
497 | 2 | {MissingArg} == {MissingArg} |
498 | 2 | {MissingArg} !!== {MissingArg} |
499 | 2 | {MissingArg} << {MissingArg} |
500 | 2 | {MissingArg} <<== {MissingArg} |
501 | 2 | {MissingArg} zermelo is {MissingArg} |
502 | 2 | {MissingArg} is subset of {MissingArg} |
503 | 1 | not0 {MissingArg} |
504 | 2 | {MissingArg} zermelo ~in {MissingArg} |
505 | 2 | {MissingArg} zermelo ~is {MissingArg} |
506 | 2 | {MissingArg} and0 {MissingArg} |
507 | 2 | {MissingArg} or0 {MissingArg} |
508 | 2 | exist0 {MissingArg} indeed {MissingArg} |
509 | 2 | {MissingArg} iff {MissingArg} |
510 | 2 | the set of ph in {MissingArg} such that {MissingArg} end set |
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,