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