helm/software/matita/contribs/ng_assembly/num/byte8.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/exadecim.ma".
  24 include "num/bitrigesim.ma".
  25
  26 (* **** *)
  27 (* BYTE *)
  28 (* **** *)
  29
  30 nrecord byte8 : Type ≝
  31  {
  32  b8h: exadecim;
  33  b8l: exadecim
  34  }.
  35
  36 (* \langle \rangle *)
  37 notation "〈x,y〉" non associative with precedence 80
  38  for @{ 'mk_byte8 $x $y }.
  39 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
  40
  41 (* operatore = *)
  42 ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
  43
  44 (* operatore < *)
  45 ndefinition lt_b8 ≝
  46 λb1,b2:byte8.
  47  (lt_ex (b8h b1) (b8h b2)) ⊕
  48  ((eq_ex (b8h b1) (b8h b2)) ⊗ (lt_ex (b8l b1) (b8l b2))).
  49
  50 (* operatore ≤ *)
  51 ndefinition le_b8 ≝
  52 λb1,b2:byte8.
  53  (lt_ex (b8h b1) (b8h b2)) ⊕
  54  ((eq_ex (b8h b1) (b8h b2)) ⊗ (le_ex (b8l b1) (b8l b2))).
  55
  56 (* operatore > *)
  57 ndefinition gt_b8 ≝
  58 λb1,b2:byte8.
  59  (gt_ex (b8h b1) (b8h b2)) ⊕
  60  ((eq_ex (b8h b1) (b8h b2)) ⊗ (gt_ex (b8l b1) (b8l b2))).
  61
  62 (* operatore ≥ *)
  63 ndefinition ge_b8 ≝
  64 λb1,b2:byte8.
  65  (gt_ex (b8h b1) (b8h b2)) ⊕
  66  ((eq_ex (b8h b1) (b8h b2)) ⊗ (ge_ex (b8l b1) (b8l b2))).
  67
  68 (* operatore and *)
  69 ndefinition and_b8 ≝
  70 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
  71
  72 (* operatore or *)
  73 ndefinition or_b8 ≝
  74 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
  75
  76 (* operatore xor *)
  77 ndefinition xor_b8 ≝
  78 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
  79
  80 (* operatore rotazione destra con carry *)
  81 ndefinition rcr_b8 ≝
  82 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
  83  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  84   [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
  85
  86 (* operatore shift destro *)
  87 ndefinition shr_b8 ≝
  88 λb:byte8.match rcr_ex (b8h b) false with
  89  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  90   [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
  91
  92 (* operatore rotazione destra *)
  93 ndefinition ror_b8 ≝
  94 λb:byte8.match rcr_ex (b8h b) false with
  95  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  96   [ pair bl' c'' ⇒ match c'' with
  97    [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
  98    | false ⇒ mk_byte8 bh' bl' ]]].
  99
 100 (* operatore rotazione destra n-volte *)
 101 nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
 102  match n with
 103   [ O ⇒ b
 104   | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
 105
 106 (* operatore rotazione sinistra con carry *)
 107 ndefinition rcl_b8 ≝
 108 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
 109  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 110   [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
 111
 112 (* operatore shift sinistro *)
 113 ndefinition shl_b8 ≝
 114 λb:byte8.match rcl_ex (b8l b) false with
 115  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 116   [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
 117
 118 (* operatore rotazione sinistra *)
 119 ndefinition rol_b8 ≝
 120 λb:byte8.match rcl_ex (b8l b) false with
 121  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 122   [ pair bh' c'' ⇒ match c'' with
 123    [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
 124    | false ⇒ mk_byte8 bh' bl' ]]].
 125
 126 (* operatore rotazione sinistra n-volte *)
 127 nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
 128  match n with
 129   [ O ⇒ b
 130   | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
 131
 132 (* operatore not/complemento a 1 *)
 133 ndefinition not_b8 ≝
 134 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
 135
 136 (* operatore somma con data+carry → data+carry *)
 137 ndefinition plus_b8_dc_dc ≝
 138 λb1,b2:byte8.λc:bool.
 139  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
 140   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
 141    [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
 142
 143 (* operatore somma con data+carry → data *)
 144 ndefinition plus_b8_dc_d ≝
 145 λb1,b2:byte8.λc:bool.
 146  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
 147   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
 148
 149 (* operatore somma con data+carry → c *)
 150 ndefinition plus_b8_dc_c ≝
 151 λb1,b2:byte8.λc:bool.
 152  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
 153
 154 (* operatore somma con data → data+carry *)
 155 ndefinition plus_b8_d_dc ≝
 156 λb1,b2:byte8.
 157  match plus_ex_d_dc (b8l b1) (b8l b2) with
 158   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
 159    [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
 160
 161 (* operatore somma con data → data *)
 162 ndefinition plus_b8_d_d ≝
 163 λb1,b2:byte8.
 164  match plus_ex_d_dc (b8l b1) (b8l b2) with
 165   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
 166
 167 (* operatore somma con data → c *)
 168 ndefinition plus_b8_d_c ≝
 169 λb1,b2:byte8.
 170  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
 171
 172 (* operatore Most Significant Bit *)
 173 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 174
 175 (* operatore predecessore *)
 176 ndefinition pred_b8 ≝
 177 λb:byte8.match eq_ex (b8l b) x0 with
 178  [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
 179  | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
 180
 181 (* operatore successore *)
 182 ndefinition succ_b8 ≝
 183 λb:byte8.match eq_ex (b8l b) xF with
 184  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
 185  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
 186
 187 (* operatore neg/complemento a 2 *)
 188 ndefinition compl_b8 ≝
 189 λb:byte8.match MSB_b8 b with
 190  [ true ⇒ succ_b8 (not_b8 b)
 191  | false ⇒ not_b8 (pred_b8 b) ].
 192
 193 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
 194 ndefinition mul_ex ≝
 195 λe1,e2:exadecim.match e1 with
 196  [ x0 ⇒ match e2 with
 197   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x0〉   | x2 ⇒ 〈x0,x0〉   | x3 ⇒ 〈x0,x0〉
 198   | x4 ⇒ 〈x0,x0〉   | x5 ⇒ 〈x0,x0〉   | x6 ⇒ 〈x0,x0〉   | x7 ⇒ 〈x0,x0〉
 199   | x8 ⇒ 〈x0,x0〉   | x9 ⇒ 〈x0,x0〉   | xA ⇒ 〈x0,x0〉   | xB ⇒ 〈x0,x0〉
 200   | xC ⇒ 〈x0,x0〉   | xD ⇒ 〈x0,x0〉   | xE ⇒ 〈x0,x0〉   | xF ⇒ 〈x0,x0〉 ]
 201  | x1 ⇒ match e2 with
 202   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x1〉   | x2 ⇒ 〈x0,x2〉   | x3 ⇒ 〈x0,x3〉
 203   | x4 ⇒ 〈x0,x4〉   | x5 ⇒ 〈x0,x5〉   | x6 ⇒ 〈x0,x6〉   | x7 ⇒ 〈x0,x7〉
 204   | x8 ⇒ 〈x0,x8〉   | x9 ⇒ 〈x0,x9〉   | xA ⇒ 〈x0,xA〉   | xB ⇒ 〈x0,xB〉
 205   | xC ⇒ 〈x0,xC〉   | xD ⇒ 〈x0,xD〉   | xE ⇒ 〈x0,xE〉   | xF ⇒ 〈x0,xF〉 ]
 206  | x2 ⇒ match e2 with
 207   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x2〉   | x2 ⇒ 〈x0,x4〉   | x3 ⇒ 〈x0,x6〉
 208   | x4 ⇒ 〈x0,x8〉   | x5 ⇒ 〈x0,xA〉   | x6 ⇒ 〈x0,xC〉   | x7 ⇒ 〈x0,xE〉
 209   | x8 ⇒ 〈x1,x0〉   | x9 ⇒ 〈x1,x2〉   | xA ⇒ 〈x1,x4〉   | xB ⇒ 〈x1,x6〉
 210   | xC ⇒ 〈x1,x8〉   | xD ⇒ 〈x1,xA〉   | xE ⇒ 〈x1,xC〉   | xF ⇒ 〈x1,xE〉 ]
 211  | x3 ⇒ match e2 with
 212   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x3〉   | x2 ⇒ 〈x0,x6〉   | x3 ⇒ 〈x0,x9〉
 213   | x4 ⇒ 〈x0,xC〉   | x5 ⇒ 〈x0,xF〉   | x6 ⇒ 〈x1,x2〉   | x7 ⇒ 〈x1,x5〉
 214   | x8 ⇒ 〈x1,x8〉   | x9 ⇒ 〈x1,xB〉   | xA ⇒ 〈x1,xE〉   | xB ⇒ 〈x2,x1〉
 215   | xC ⇒ 〈x2,x4〉   | xD ⇒ 〈x2,x7〉   | xE ⇒ 〈x2,xA〉   | xF ⇒ 〈x2,xD〉 ]
 216  | x4 ⇒ match e2 with
 217   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x4〉   | x2 ⇒ 〈x0,x8〉   | x3 ⇒ 〈x0,xC〉
 218   | x4 ⇒ 〈x1,x0〉   | x5 ⇒ 〈x1,x4〉   | x6 ⇒ 〈x1,x8〉   | x7 ⇒ 〈x1,xC〉
 219   | x8 ⇒ 〈x2,x0〉   | x9 ⇒ 〈x2,x4〉   | xA ⇒ 〈x2,x8〉   | xB ⇒ 〈x2,xC〉
 220   | xC ⇒ 〈x3,x0〉   | xD ⇒ 〈x3,x4〉   | xE ⇒ 〈x3,x8〉   | xF ⇒ 〈x3,xC〉 ]
 221  | x5 ⇒ match e2 with
 222   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x5〉   | x2 ⇒ 〈x0,xA〉   | x3 ⇒ 〈x0,xF〉
 223   | x4 ⇒ 〈x1,x4〉   | x5 ⇒ 〈x1,x9〉   | x6 ⇒ 〈x1,xE〉   | x7 ⇒ 〈x2,x3〉
 224   | x8 ⇒ 〈x2,x8〉   | x9 ⇒ 〈x2,xD〉   | xA ⇒ 〈x3,x2〉   | xB ⇒ 〈x3,x7〉
 225   | xC ⇒ 〈x3,xC〉   | xD ⇒ 〈x4,x1〉   | xE ⇒ 〈x4,x6〉   | xF ⇒ 〈x4,xB〉 ]
 226  | x6 ⇒ match e2 with
 227   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x6〉   | x2 ⇒ 〈x0,xC〉   | x3 ⇒ 〈x1,x2〉
 228   | x4 ⇒ 〈x1,x8〉   | x5 ⇒ 〈x1,xE〉   | x6 ⇒ 〈x2,x4〉   | x7 ⇒ 〈x2,xA〉
 229   | x8 ⇒ 〈x3,x0〉   | x9 ⇒ 〈x3,x6〉   | xA ⇒ 〈x3,xC〉   | xB ⇒ 〈x4,x2〉
 230   | xC ⇒ 〈x4,x8〉   | xD ⇒ 〈x4,xE〉   | xE ⇒ 〈x5,x4〉   | xF ⇒ 〈x5,xA〉 ]
 231  | x7 ⇒ match e2 with
 232   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x7〉   | x2 ⇒ 〈x0,xE〉   | x3 ⇒ 〈x1,x5〉
 233   | x4 ⇒ 〈x1,xC〉   | x5 ⇒ 〈x2,x3〉   | x6 ⇒ 〈x2,xA〉   | x7 ⇒ 〈x3,x1〉
 234   | x8 ⇒ 〈x3,x8〉   | x9 ⇒ 〈x3,xF〉   | xA ⇒ 〈x4,x6〉   | xB ⇒ 〈x4,xD〉
 235   | xC ⇒ 〈x5,x4〉   | xD ⇒ 〈x5,xB〉   | xE ⇒ 〈x6,x2〉   | xF ⇒ 〈x6,x9〉 ]
 236  | x8 ⇒ match e2 with
 237   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x8〉   | x2 ⇒ 〈x1,x0〉   | x3 ⇒ 〈x1,x8〉
 238   | x4 ⇒ 〈x2,x0〉   | x5 ⇒ 〈x2,x8〉   | x6 ⇒ 〈x3,x0〉   | x7 ⇒ 〈x3,x8〉
 239   | x8 ⇒ 〈x4,x0〉   | x9 ⇒ 〈x4,x8〉   | xA ⇒ 〈x5,x0〉   | xB ⇒ 〈x5,x8〉
 240   | xC ⇒ 〈x6,x0〉   | xD ⇒ 〈x6,x8〉   | xE ⇒ 〈x7,x0〉   | xF ⇒ 〈x7,x8〉 ]
 241  | x9 ⇒ match e2 with
 242   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x9〉   | x2 ⇒ 〈x1,x2〉   | x3 ⇒ 〈x1,xB〉
 243   | x4 ⇒ 〈x2,x4〉   | x5 ⇒ 〈x2,xD〉   | x6 ⇒ 〈x3,x6〉   | x7 ⇒ 〈x3,xF〉
 244   | x8 ⇒ 〈x4,x8〉   | x9 ⇒ 〈x5,x1〉   | xA ⇒ 〈x5,xA〉   | xB ⇒ 〈x6,x3〉
 245   | xC ⇒ 〈x6,xC〉   | xD ⇒ 〈x7,x5〉   | xE ⇒ 〈x7,xE〉   | xF ⇒ 〈x8,x7〉 ]
 246  | xA ⇒ match e2 with
 247   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xA〉   | x2 ⇒ 〈x1,x4〉   | x3 ⇒ 〈x1,xE〉
 248   | x4 ⇒ 〈x2,x8〉   | x5 ⇒ 〈x3,x2〉   | x6 ⇒ 〈x3,xC〉   | x7 ⇒ 〈x4,x6〉
 249   | x8 ⇒ 〈x5,x0〉   | x9 ⇒ 〈x5,xA〉   | xA ⇒ 〈x6,x4〉   | xB ⇒ 〈x6,xE〉
 250   | xC ⇒ 〈x7,x8〉   | xD ⇒ 〈x8,x2〉   | xE ⇒ 〈x8,xC〉   | xF ⇒ 〈x9,x6〉 ]
 251  | xB ⇒ match e2 with
 252   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xB〉   | x2 ⇒ 〈x1,x6〉   | x3 ⇒ 〈x2,x1〉
 253   | x4 ⇒ 〈x2,xC〉   | x5 ⇒ 〈x3,x7〉   | x6 ⇒ 〈x4,x2〉   | x7 ⇒ 〈x4,xD〉
 254   | x8 ⇒ 〈x5,x8〉   | x9 ⇒ 〈x6,x3〉   | xA ⇒ 〈x6,xE〉   | xB ⇒ 〈x7,x9〉
 255   | xC ⇒ 〈x8,x4〉   | xD ⇒ 〈x8,xF〉   | xE ⇒ 〈x9,xA〉   | xF ⇒ 〈xA,x5〉 ]
 256  | xC ⇒ match e2 with
 257   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xC〉   | x2 ⇒ 〈x1,x8〉   | x3 ⇒ 〈x2,x4〉
 258   | x4 ⇒ 〈x3,x0〉   | x5 ⇒ 〈x3,xC〉   | x6 ⇒ 〈x4,x8〉   | x7 ⇒ 〈x5,x4〉
 259   | x8 ⇒ 〈x6,x0〉   | x9 ⇒ 〈x6,xC〉   | xA ⇒ 〈x7,x8〉   | xB ⇒ 〈x8,x4〉
 260   | xC ⇒ 〈x9,x0〉   | xD ⇒ 〈x9,xC〉   | xE ⇒ 〈xA,x8〉   | xF ⇒ 〈xB,x4〉 ]
 261  | xD ⇒ match e2 with
 262   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xD〉   | x2 ⇒ 〈x1,xA〉   | x3 ⇒ 〈x2,x7〉
 263   | x4 ⇒ 〈x3,x4〉   | x5 ⇒ 〈x4,x1〉   | x6 ⇒ 〈x4,xE〉   | x7 ⇒ 〈x5,xB〉
 264   | x8 ⇒ 〈x6,x8〉   | x9 ⇒ 〈x7,x5〉   | xA ⇒ 〈x8,x2〉   | xB ⇒ 〈x8,xF〉
 265   | xC ⇒ 〈x9,xC〉   | xD ⇒ 〈xA,x9〉   | xE ⇒ 〈xB,x6〉   | xF ⇒ 〈xC,x3〉 ]
 266  | xE ⇒ match e2 with
 267   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xE〉   | x2 ⇒ 〈x1,xC〉   | x3 ⇒ 〈x2,xA〉
 268   | x4 ⇒ 〈x3,x8〉   | x5 ⇒ 〈x4,x6〉   | x6 ⇒ 〈x5,x4〉   | x7 ⇒ 〈x6,x2〉
 269   | x8 ⇒ 〈x7,x0〉   | x9 ⇒ 〈x7,xE〉   | xA ⇒ 〈x8,xC〉   | xB ⇒ 〈x9,xA〉
 270   | xC ⇒ 〈xA,x8〉   | xD ⇒ 〈xB,x6〉   | xE ⇒ 〈xC,x4〉   | xF ⇒ 〈xD,x2〉 ]
 271  | xF ⇒ match e2 with
 272   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xF〉   | x2 ⇒ 〈x1,xE〉   | x3 ⇒ 〈x2,xD〉
 273   | x4 ⇒ 〈x3,xC〉   | x5 ⇒ 〈x4,xB〉   | x6 ⇒ 〈x5,xA〉   | x7 ⇒ 〈x6,x9〉
 274   | x8 ⇒ 〈x7,x8〉   | x9 ⇒ 〈x8,x7〉   | xA ⇒ 〈x9,x6〉   | xB ⇒ 〈xA,x5〉
 275   | xC ⇒ 〈xB,x4〉   | xD ⇒ 〈xC,x3〉   | xE ⇒ 〈xD,x2〉   | xF ⇒ 〈xE,x1〉 ]
 276  ].
 277
 278 (* correzione per somma su BCD *)
 279 (* input: halfcarry,carry,X(BCD+BCD) *)
 280 (* output: X',carry' *)
 281 ndefinition daa_b8 ≝
 282 λh,c:bool.λX:byte8.
 283  match lt_b8 X 〈x9,xA〉 with
 284   (* [X:0x00-0x99] *)
 285   (* c' = c *)
 286   (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
 287           [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
 288   [ true ⇒
 289    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
 290     [ true ⇒ X
 291     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
 292    let X'' ≝ match c with
 293     [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
 294     | false ⇒ X' ] in
 295    pair … X'' c
 296   (* [X:0x9A-0xFF] *)
 297   (* c' = 1 *)
 298   (* X' = [X:0x9A-0xFF]
 299           [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
 300           [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
 301   | false ⇒
 302    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
 303     [ true ⇒ X
 304     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
 305    let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
 306    pair … X'' true
 307   ].
 308
 309 (* operatore x in [inf,sup] *)
 310 ndefinition inrange_b8 ≝
 311 λx,inf,sup:byte8.(le_b8 inf x) ⊗ (le_b8 x sup).
 312
 313 (* iteratore sui byte *)
 314 ndefinition forall_b8 ≝
 315  λP.
 316   forall_ex (λbh.
 317   forall_ex (λbl.
 318    P (mk_byte8 bh bl))).
 319
 320 (* byte ricorsivi *)
 321 ninductive rec_byte8 : byte8 → Type ≝
 322   b8_O : rec_byte8 〈x0,x0〉
 323 | b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n).
 324
 325 (* byte → byte ricorsivi *)
 326 ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝
 327 λn.λrecb:rec_byte8 〈n,x0〉.
 328  b8_S 〈n,xF〉 (b8_S 〈n,xE〉 (b8_S 〈n,xD〉 (b8_S 〈n,xC〉 (
 329  b8_S 〈n,xB〉 (b8_S 〈n,xA〉 (b8_S 〈n,x9〉 (b8_S 〈n,x8〉 (
 330  b8_S 〈n,x7〉 (b8_S 〈n,x6〉 (b8_S 〈n,x5〉 (b8_S 〈n,x4〉 (
 331  b8_S 〈n,x3〉 (b8_S 〈n,x2〉 (b8_S 〈n,x1〉 (b8_S 〈n,x0〉 recb))))))))))))))).
 332
 333 (* ... cifra esadecimale superiore *)
 334 nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
 335  match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
 336   [ ex_O ⇒ b8_O
 337   | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
 338   ].
 339
 340 (* ... cifra esadecimale inferiore *)
 341 ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
 342 λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
 343  match n2 return λx.rec_byte8 〈n1,x〉 with
 344   [ x0 ⇒ recb
 345   | x1 ⇒ b8_S 〈n1,x0〉 recb
 346   | x2 ⇒ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)
 347   | x3 ⇒ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))
 348   | x4 ⇒ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))
 349   | x5 ⇒ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
 350          b8_S 〈n1,x0〉 recb))))
 351   | x6 ⇒ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
 352          b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))
 353   | x7 ⇒ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
 354          b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))
 355   | x8 ⇒ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
 356          b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))
 357   | x9 ⇒ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
 358          b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
 359          b8_S 〈n1,x0〉 recb))))))))
 360   | xA ⇒ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
 361          b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
 362          b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))
 363   | xB ⇒ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
 364          b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
 365          b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))
 366   | xC ⇒ b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (
 367          b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
 368          b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))
 369   | xD ⇒ b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (
 370          b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
 371          b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
 372          b8_S 〈n1,x0〉 recb))))))))))))
 373   | xE ⇒ b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (
 374          b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
 375          b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
 376          b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))))
 377   | xF ⇒ b8_S 〈n1,xE〉 (b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (
 378          b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
 379          b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
 380          b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))))))
 381   ].
 382
 383 (*
 384 nlemma b8_to_recb8 : Πb.rec_byte8 b.
 385  #b; nletin K ≝ (b8_to_recb8_aux3
 386      (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
 387  ncases b in K; #e1; #e2; #K; napply K;
 388 nqed.
 389 *)
 390
 391 ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
 392 λb.match b with [ mk_byte8 h l ⇒ b8_to_recb8_aux3 h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
 393
 394 (* ottali → esadecimali *)
 395 ndefinition b8_of_bit ≝
 396 λn.match n with
 397  [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
 398  | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
 399  | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
 400  | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
 401  | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
 402  | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
 403  | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
 404  | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉
 405  ].