]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/freescale/word16.ma
some corrections ...
[helm.git] / matita / matita / contribs / assembly / freescale / word16.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                           Progetto FreeScale                           *)
17 (*                                                                        *)
18 (* Sviluppato da:                                                         *)
19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
20 (*                                                                        *)
21 (* Questo materiale fa parte della tesi:                                  *)
22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
23 (*                                                                        *)
24 (*                    data ultima modifica 15/11/2007                     *)
25 (* ********************************************************************** *)
26
27 include "freescale/byte8.ma".
28
29 (* ********************** *)
30 (* DEFINIZIONE DELLE WORD *)
31 (* ********************** *)
32
33 record word16 : Type ≝
34  {
35  w16h: byte8;
36  w16l: byte8
37  }.
38
39 (* \langle \rangle *)
40 notation "〈x:y〉" non associative with precedence 80
41  for @{ 'mk_word16 $x $y }.
42 interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
43
44 (* operatore = *)
45 definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
46
47 (* operatore < *)
48 definition lt_w16 ≝
49 λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with
50  [ true ⇒ true
51  | false ⇒ match gt_b8 (w16h w1) (w16h w2) with
52   [ true ⇒ false
53   | false ⇒ lt_b8 (w16l w1) (w16l w2) ]].
54
55 (* operatore ≤ *)
56 definition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2).
57
58 (* operatore > *)
59 definition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2).
60
61 (* operatore ≥ *)
62 definition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2).
63
64 (* operatore and *)
65 definition and_w16 ≝
66 λw1,w2:word16.mk_word16 (and_b8 (w16h w1) (w16h w2)) (and_b8 (w16l w1) (w16l w2)).
67
68 (* operatore or *)
69 definition or_w16 ≝
70 λw1,w2:word16.mk_word16 (or_b8 (w16h w1) (w16h w2)) (or_b8 (w16l w1) (w16l w2)).
71
72 (* operatore xor *)
73 definition xor_w16 ≝
74 λw1,w2:word16.mk_word16 (xor_b8 (w16h w1) (w16h w2)) (xor_b8 (w16l w1) (w16l w2)).
75
76 (* operatore rotazione destra con carry *)
77 definition rcr_w16 ≝
78 λw:word16.λc:bool.match rcr_b8 (w16h w) c with
79  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
80   [ pair wl' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]]. 
81
82 (* operatore shift destro *)
83 definition shr_w16 ≝
84 λw:word16.match rcr_b8 (w16h w) false with
85  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
86   [ pair wl' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
87
88 (* operatore rotazione destra *)
89 definition ror_w16 ≝
90 λw:word16.match rcr_b8 (w16h w) false with
91  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
92   [ pair wl' c'' ⇒ match c'' with
93    [ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
94    | false ⇒ mk_word16 wh' wl' ]]].
95
96 (* operatore rotazione destra n-volte *)
97 let rec ror_w16_n (w:word16) (n:nat) on n ≝
98  match n with
99   [ O ⇒ w
100   | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
101
102 (* operatore rotazione sinistra con carry *)
103 definition rcl_w16 ≝
104 λw:word16.λc:bool.match rcl_b8 (w16l w) c with
105  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
106   [ pair wh' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]]. 
107
108 (* operatore shift sinistro *)
109 definition shl_w16 ≝
110 λw:word16.match rcl_b8 (w16l w) false with
111  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
112   [ pair wh' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
113
114 (* operatore rotazione sinistra *)
115 definition rol_w16 ≝
116 λw:word16.match rcl_b8 (w16l w) false with
117  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
118   [ pair wh' c'' ⇒ match c'' with
119    [ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
120    | false ⇒ mk_word16 wh' wl' ]]].
121
122 (* operatore rotazione sinistra n-volte *)
123 let rec rol_w16_n (w:word16) (n:nat) on n ≝
124  match n with
125   [ O ⇒ w
126   | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
127
128 (* operatore not/complemento a 1 *)
129 definition not_w16 ≝
130 λw:word16.mk_word16 (not_b8 (w16h w)) (not_b8 (w16l w)).
131
132 (* operatore somma con carry *)
133 definition plus_w16 ≝
134 λw1,w2:word16.λc:bool.
135  match plus_b8 (w16l w1) (w16l w2) c with
136   [ pair l c' ⇒ match plus_b8 (w16h w1) (w16h w2) c' with
137    [ pair h c'' ⇒ pair ?? (mk_word16 h l) c'' ]].
138
139 (* operatore somma senza carry *)
140 definition plus_w16nc ≝
141 λw1,w2:word16.fst ?? (plus_w16 w1 w2 false).
142
143 (* operatore carry della somma *)
144 definition plus_w16c ≝
145 λw1,w2:word16.snd ?? (plus_w16 w1 w2 false).
146
147 (* operatore Most Significant Bit *)
148 definition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
149
150 (* word → naturali *)
151 definition nat_of_word16 ≝ λw:word16. 256 * (w16h w) + (nat_of_byte8 (w16l w)).
152
153 coercion nat_of_word16.
154
155 (* naturali → word *)
156 definition word16_of_nat ≝
157  λn.mk_word16 (byte8_of_nat (n / 256)) (byte8_of_nat n).
158
159 (* operatore predecessore *)
160 definition pred_w16 ≝
161 λw:word16.match eq_b8 (w16l w) (mk_byte8 x0 x0) with
162  [ true ⇒ mk_word16 (pred_b8 (w16h w)) (pred_b8 (w16l w))
163  | false ⇒ mk_word16 (w16h w) (pred_b8 (w16l w)) ].
164
165 (* operatore successore *)
166 definition succ_w16 ≝
167 λw:word16.match eq_b8 (w16l w) (mk_byte8 xF xF) with
168  [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w))
169  | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ].
170
171 (* operatore neg/complemento a 2 *)
172 definition compl_w16 ≝
173 λw:word16.match MSB_w16 w with
174  [ true ⇒ succ_w16 (not_w16 w)
175  | false ⇒ not_w16 (pred_w16 w) ].
176
177 (* 
178    operatore moltiplicazione senza segno: b*b=[0x0000,0xFE01]
179    ... in pratica (〈a,b〉*〈c,d〉) = (a*c)<<8+(a*d)<<4+(b*c)<<4+(b*d)
180 *)
181 definition mul_b8 ≝
182 λb1,b2:byte8.match b1 with
183 [ mk_byte8 b1h b1l ⇒ match b2 with
184 [ mk_byte8 b2h b2l ⇒ match mul_ex b1l b2l with
185 [ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with
186 [ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
187 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
188 [ mk_byte8 t4_h t4_l ⇒
189  plus_w16nc
190   (plus_w16nc
191    (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
192 ]]]]]].
193
194 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
195 definition div_b8 ≝
196 λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
197 (* 
198    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
199 *)
200  [ true ⇒ tripleT ??? 〈xF,xF〉 (w16l w) true
201  | false ⇒ match eq_w16 w 〈〈x0,x0〉:〈x0,x0〉〉 with
202 (* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
203   [ true ⇒ tripleT ??? 〈x0,x0〉 〈x0,x0〉 false
204 (* 1) e' una divisione sensata che produrra' overflow/risultato *)
205 (* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
206 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
207 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
208 (*    puo' essere sottratto al dividendo *) 
209   | false ⇒ let rec aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
210   let w' ≝ plus_w16nc divd (compl_w16 divs) in
211    match c with
212    [ O ⇒ match le_w16 divs divd with
213     [ true ⇒ tripleT ??? (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
214     | false ⇒ tripleT ??? q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
215    | S c' ⇒ match le_w16 divs divd with
216     [ true ⇒ aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
217     | false ⇒ aux divd (ror_w16 divs) (ror_b8 molt) q c' ]]
218   in aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
219
220 (* operatore x in [inf,sup] *)
221 definition in_range ≝
222 λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
223
224 (* iteratore sulle word *)
225 definition forall_word16 ≝
226  λP.
227   forall_byte8 (λbh.
228   forall_byte8 (λbl.
229    P (mk_word16 bh bl ))).
230
231 (* ********************** *)
232 (* TEOREMI/LEMMMI/ASSIOMI *)
233 (* ********************** *)
234
235 (* TODO: dimostrare diversamente *)
236 axiom word16_of_nat_nat_of_word16: ∀b. word16_of_nat (nat_of_word16 b) = b.
237
238 (* TODO: dimostrare diversamente *)
239 axiom lt_nat_of_word16_65536: ∀b. nat_of_word16 b < (256 * 256).
240
241 (* TODO: dimostrare diversamente *)
242 axiom nat_of_word16_word16_of_nat: ∀n. nat_of_word16 (word16_of_nat n) = n \mod (256 * 256).
243
244 (* TODO: dimostrare diversamente *)
245 axiom eq_nat_of_word16_n_nat_of_word16_mod_n_65536:
246  ∀n. word16_of_nat n = word16_of_nat (n \mod (256 * 256)).
247
248 lemma plusw16_ok:
249  ∀b1,b2,c.
250   match plus_w16 b1 b2 c with
251    [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_word16 r + nat_of_bool c' * (256 * 256)
252    ].
253  intros; elim daemon.
254 qed.
255
256 (* TODO: dimostrare diversamente *)
257 axiom plusw16_O_x:
258  ∀b. plus_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) b false = pair ?? b false.
259
260 lemma plusw16nc_O_x:
261  ∀x. plus_w16nc (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) x = x.
262  intros;
263  unfold plus_w16nc;
264  rewrite > plusw16_O_x;
265  reflexivity.
266 qed.
267
268 (* TODO: dimostrare diversamente *)
269 axiom eq_nat_of_word16_mod: ∀b. nat_of_word16 b = nat_of_word16 b \mod (256 * 256).
270
271 (* TODO: dimostrare diversamente *)
272 axiom plusw16nc_ok:
273  ∀b1,b2:word16. nat_of_word16 (plus_w16nc b1 b2) = (b1 + b2) \mod (256 * 256).
274
275 (* TODO: dimostrare diversamente *)
276 axiom eq_eqw16_x0_x0_x0_x0_word16_of_nat_S_false:
277  ∀b. b < (256 * 256 - 1) → eq_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) (word16_of_nat (S b)) = false.
278
279 axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
280
281 (* TODO: dimostrare diversamente *)
282 axiom eq_w16pred_S_a_a:
283  ∀a. a < (256 * 256 - 1) → pred_w16 (word16_of_nat (S a)) = word16_of_nat a.
284
285 (* TODO: dimostrare diversamente *)
286 axiom plusw16nc_S:
287  ∀x:word16.∀n.plus_w16nc (word16_of_nat (x*n)) x = word16_of_nat (x * S n).
288
289 (* TODO: dimostrare diversamente *)
290 axiom eq_plusw16c_x0_x0_x0_x0_x_false:
291  ∀x.plus_w16c (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) x = false.
292
293 (* TODO: dimostrare diversamente *)
294 axiom eqw16_true_to_eq: ∀b,b'. eq_w16 b b' = true → b=b'.
295
296 (* TODO: dimostrare diversamente *)
297 axiom eqw16_false_to_not_eq: ∀b,b'. eq_w16 b b' = false → b ≠ b'.
298
299 (* TODO: dimostrare diversamente *)
300 axiom word16_of_nat_mod: ∀n.word16_of_nat n = word16_of_nat (n \mod (256 * 256)).
301
302 (* nuovi *)
303
304 (*
305 lemma ok_mul_b8: ∀b1,b2:byte8. nat_of_word16 (mul_b8 b1 b2) = b1 * b2.
306  intros;
307  cases b1 (b1h b1l);
308  cases b2 (b2h b2l);
309  change in ⊢ (? ? (? %) ?) with
310   (match mul_ex b1l b2l with
311 [ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with
312 [ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
313 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
314 [ mk_byte8 t4_h t4_l ⇒
315  plus_w16nc
316   (plus_w16nc
317    (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
318 ]]]]);
319  lapply (ok_mul_ex b1l b2l) as ll;
320  lapply (ok_mul_ex b1h b2l) as hl;
321  lapply (ok_mul_ex b2h b1l) as lh;
322  lapply (ok_mul_ex b1h b2h) as hh;
323  elim (mul_ex b1l b2l) (t1_h t1_l);
324  change in ⊢ (? ? (? %) ?) with
325   (match mul_ex b1h b2l with
326 [ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
327 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
328 [ mk_byte8 t4_h t4_l ⇒
329  plus_w16nc
330   (plus_w16nc
331    (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
332 ]]]);
333  elim (mul_ex b1h b2l) (t2_h t2_l);
334  change in ⊢ (? ? (? %) ?) with
335   (match mul_ex b2h b1l with
336 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
337 [ mk_byte8 t4_h t4_l ⇒
338  plus_w16nc
339   (plus_w16nc
340    (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
341 ]]);
342  elim (mul_ex b2h b1l) (t3_h t3_l);
343  change in ⊢ (? ? (? %) ?) with
344   (match mul_ex b1h b2h with
345 [ mk_byte8 t4_h t4_l ⇒
346  plus_w16nc
347   (plus_w16nc
348    (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
349 ]);
350  elim (mul_ex b1h b2h) (t4_h t4_l);
351  change in ⊢ (? ? (? %) ?) with
352   (plus_w16nc
353   (plus_w16nc
354    (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉);
355  do 3 (rewrite > plusw16nc_ok);
356  unfold nat_of_word16;
357  unfold nat_of_byte8;
358 simplify in ⊢ (? ? (? (? (? (? (? (? (? (? ? (? (? ? (? (? %))) ?)) ?) ?) ?) ?) ?) ?) ?) ?);
359 simplify in ⊢ (? ? (? (? (? (? (? (? (? ? (? (? ? (? (? %))) ?)) ?) ?) ?) ?) ?) ?) ?);
360 simplify in ⊢ (? ? (? (? (? (? (? (? (? ? (? ? (? (? %)))) ?) ?) ?) ?) ?) ?) ?);
361 whd in ⊢ (? ? (? (? (? (? (? (? (? ? (? ? %)) ?) ?) ?) ?) ?) ?) ?);
362 whd in ⊢ (? ? (? (? (? (? (? (? (? ? %) ?) ?) ?) ?) ?) ?) ?);
363 simplify in ⊢ (? ? (? (? ? (? (? ? (? (? ? (? %)) ?)) ?)) ?) ?);
364 simplify in ⊢ (? ? (? (? ? (? (? ? (? ? (? (? %)))) ?)) ?) ?);
365 simplify in ⊢ (? ? (? (? ? (? (? ? (? ? %)) ?)) ?) ?);
366 whd in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
367 simplify in ⊢ (? ? (? (? ? (? ? (? (? ? (? (? %))) ?))) ?) ?);
368 simplify in ⊢ (? ? (? (? ? (? ? (? ? (? (? %))))) ?) ?);
369 simplify in ⊢ (? ? ? (? (? (? ? (? %)) ?) ?));
370 simplify in ⊢ (? ? ? (? (? ? (? %)) ?));
371 simplify in ⊢ (? ? ? (? ? (? (? ? (? %)) ?)));
372 simplify in ⊢ (? ? ? (? ? (? ? (? %))));
373 simplify in ⊢ (? ? (? (? ? (? ? (? (? ? (? %)) ?))) ?) ?);
374 simplify in ⊢ (? ? (? (? ? (? ? (? ? (? %)))) ?) ?);
375 simplify in ⊢ (? ? (? (? (? (? ? (? ? (? ? (? %)))) ?) ?) ?) ?);
376 simplify in ⊢ (? ? (? (? (? (? ? (? ? (? (? ? (? %)) ?))) ?) ?) ?) ?);
377 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? (? ? (? %))) ?)) ?) ?) ?) ?);
378 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? (? (? ? (? %)) ?)) ?)) ?) ?) ?) ?);
379 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? ? (? ? (? %)))) ?) ?) ?) ?) ?) ?);
380 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? (? ? (? %))) ?)) ?) ?) ?) ?) ?) ?);
381 simplify in ⊢ (? ? (? (? (? (? (? (? (? (? ? (? (? ? (? %)) ?)) ?) ?) ?) ?) ?) ?) ?) ?);
382 simplify in ⊢ (? ? (? (? (? (? (? (? (? (? ? (? ? (? %))) ?) ?) ?) ?) ?) ?) ?) ?);
383 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? ? (? (? ? (? %)) ?))) ?) ?) ?) ?) ?) ?);
384 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? (? (? ? (? %)) ?)) ?)) ?) ?) ?) ?) ?) ?);
385 rewrite < plus_n_O;
386 change in ⊢ (? ? (? (? ? %) ?) ?) with (16*nat_of_exadecim t1_h+nat_of_exadecim t1_l);
387 unfold nat_of_byte8 in H H1 H2 H3;
388 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? (? (? ? %) ?)) ?)) ?) ?) ?) ?) ?) ?);
389 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? ? (? ? %))) ?) ?) ?) ?) ?) ?);
390 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? (? (? ? %) ?)) ?)) ?) ?) ?) ?);
391 simplify in ⊢ (? ? (? (? (? (? ? (? ? (? ? %))) ?) ?) ?) ?);
392 rewrite < plus_n_O;
393 rewrite < plus_n_O;
394 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? %) ?)) ?) ?) ?) ?) ?) ?);
395 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? %) ?)) ?) ?) ?) ?);
396 elim daemon.
397 qed.
398 *)