helm/software/matita/contribs/ng_assembly/freescale/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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/exadecim.ma".
  24
  25 (* **** *)
  26 (* BYTE *)
  27 (* **** *)
  28
  29 nrecord byte8 : Type ≝
  30  {
  31  b8h: exadecim;
  32  b8l: exadecim
  33  }.
  34
  35 ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
  36 λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
  37  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
  38
  39 ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
  40 λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
  41  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
  42
  43 ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
  44 λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
  45  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
  46
  47 ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
  48 ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].
  49
  50 (* \langle \rangle *)
  51 notation "〈x,y〉" non associative with precedence 80
  52  for @{ 'mk_byte8 $x $y }.
  53 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
  54
  55 (* operatore = *)
  56 ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
  57
  58 (* operatore < *)
  59 ndefinition lt_b8 ≝
  60 λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
  61  [ true ⇒ true
  62  | false ⇒ match gt_ex (b8h b1) (b8h b2) with
  63   [ true ⇒ false
  64   | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
  65
  66 (* operatore ≤ *)
  67 ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2).
  68
  69 (* operatore > *)
  70 ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
  71
  72 (* operatore ≥ *)
  73 ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
  74
  75 (* operatore and *)
  76 ndefinition and_b8 ≝
  77 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
  78
  79 (* operatore or *)
  80 ndefinition or_b8 ≝
  81 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
  82
  83 (* operatore xor *)
  84 ndefinition xor_b8 ≝
  85 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
  86
  87 (* operatore rotazione destra con carry *)
  88 ndefinition rcr_b8 ≝
  89 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
  90  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  91   [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
  92
  93 (* operatore shift destro *)
  94 ndefinition shr_b8 ≝
  95 λb:byte8.match rcr_ex (b8h b) false with
  96  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  97   [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
  98
  99 (* operatore rotazione destra *)
 100 ndefinition ror_b8 ≝
 101 λb:byte8.match rcr_ex (b8h b) false with
 102  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
 103   [ pair bl' c'' ⇒ match c'' with
 104    [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
 105    | false ⇒ mk_byte8 bh' bl' ]]].
 106
 107 (* operatore rotazione destra n-volte *)
 108 nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
 109  match n with
 110   [ O ⇒ b
 111   | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
 112
 113 (* operatore rotazione sinistra con carry *)
 114 ndefinition rcl_b8 ≝
 115 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
 116  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 117   [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
 118
 119 (* operatore shift sinistro *)
 120 ndefinition shl_b8 ≝
 121 λb:byte8.match rcl_ex (b8l b) false with
 122  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 123   [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
 124
 125 (* operatore rotazione sinistra *)
 126 ndefinition rol_b8 ≝
 127 λb:byte8.match rcl_ex (b8l b) false with
 128  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 129   [ pair bh' c'' ⇒ match c'' with
 130    [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
 131    | false ⇒ mk_byte8 bh' bl' ]]].
 132
 133 (* operatore rotazione sinistra n-volte *)
 134 nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
 135  match n with
 136   [ O ⇒ b
 137   | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
 138
 139 (* operatore not/complemento a 1 *)
 140 ndefinition not_b8 ≝
 141 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
 142
 143 (* operatore somma con data+carry → data+carry *)
 144 ndefinition plus_b8_dc_dc ≝
 145 λb1,b2:byte8.λc:bool.
 146  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
 147   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
 148    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
 149
 150 (* operatore somma con data+carry → data *)
 151 ndefinition plus_b8_dc_d ≝
 152 λb1,b2:byte8.λc:bool.
 153  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
 154   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
 155
 156 (* operatore somma con data+carry → c *)
 157 ndefinition plus_b8_dc_c ≝
 158 λb1,b2:byte8.λc:bool.
 159  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
 160
 161 (* operatore somma con data → data+carry *)
 162 ndefinition plus_b8_d_dc ≝
 163 λb1,b2:byte8.
 164  match plus_ex_d_dc (b8l b1) (b8l b2) with
 165   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
 166    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
 167
 168 (* operatore somma con data → data *)
 169 ndefinition plus_b8_d_d ≝
 170 λb1,b2:byte8.
 171  match plus_ex_d_dc (b8l b1) (b8l b2) with
 172   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
 173
 174 (* operatore somma con data → c *)
 175 ndefinition plus_b8_d_c ≝
 176 λb1,b2:byte8.
 177  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
 178
 179 (* operatore Most Significant Bit *)
 180 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 181
 182 (* byte → naturali *)
 183 ndefinition nat_of_byte8 ≝ λb:byte8.(16*(nat_of_exadecim (b8h b))) + (nat_of_exadecim (b8l b)).
 184
 185 (* operatore predecessore *)
 186 ndefinition pred_b8 ≝
 187 λb:byte8.match eq_ex (b8l b) x0 with
 188  [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
 189  | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
 190
 191 (* operatore successore *)
 192 ndefinition succ_b8 ≝
 193 λb:byte8.match eq_ex (b8l b) xF with
 194  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
 195  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
 196
 197 (* operatore neg/complemento a 2 *)
 198 ndefinition compl_b8 ≝
 199 λb:byte8.match MSB_b8 b with
 200  [ true ⇒ succ_b8 (not_b8 b)
 201  | false ⇒ not_b8 (pred_b8 b) ].
 202
 203 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
 204 ndefinition mul_ex ≝
 205 λe1,e2:exadecim.match e1 with
 206  [ x0 ⇒ match e2 with
 207   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x0〉   | x2 ⇒ 〈x0,x0〉   | x3 ⇒ 〈x0,x0〉
 208   | x4 ⇒ 〈x0,x0〉   | x5 ⇒ 〈x0,x0〉   | x6 ⇒ 〈x0,x0〉   | x7 ⇒ 〈x0,x0〉
 209   | x8 ⇒ 〈x0,x0〉   | x9 ⇒ 〈x0,x0〉   | xA ⇒ 〈x0,x0〉   | xB ⇒ 〈x0,x0〉
 210   | xC ⇒ 〈x0,x0〉   | xD ⇒ 〈x0,x0〉   | xE ⇒ 〈x0,x0〉   | xF ⇒ 〈x0,x0〉 ]
 211  | x1 ⇒ match e2 with
 212   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x1〉   | x2 ⇒ 〈x0,x2〉   | x3 ⇒ 〈x0,x3〉
 213   | x4 ⇒ 〈x0,x4〉   | x5 ⇒ 〈x0,x5〉   | x6 ⇒ 〈x0,x6〉   | x7 ⇒ 〈x0,x7〉
 214   | x8 ⇒ 〈x0,x8〉   | x9 ⇒ 〈x0,x9〉   | xA ⇒ 〈x0,xA〉   | xB ⇒ 〈x0,xB〉
 215   | xC ⇒ 〈x0,xC〉   | xD ⇒ 〈x0,xD〉   | xE ⇒ 〈x0,xE〉   | xF ⇒ 〈x0,xF〉 ]
 216  | x2 ⇒ match e2 with
 217   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x2〉   | x2 ⇒ 〈x0,x4〉   | x3 ⇒ 〈x0,x6〉
 218   | x4 ⇒ 〈x0,x8〉   | x5 ⇒ 〈x0,xA〉   | x6 ⇒ 〈x0,xC〉   | x7 ⇒ 〈x0,xE〉
 219   | x8 ⇒ 〈x1,x0〉   | x9 ⇒ 〈x1,x2〉   | xA ⇒ 〈x1,x4〉   | xB ⇒ 〈x1,x6〉
 220   | xC ⇒ 〈x1,x8〉   | xD ⇒ 〈x1,xA〉   | xE ⇒ 〈x1,xC〉   | xF ⇒ 〈x1,xE〉 ]
 221  | x3 ⇒ match e2 with
 222   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x3〉   | x2 ⇒ 〈x0,x6〉   | x3 ⇒ 〈x0,x9〉
 223   | x4 ⇒ 〈x0,xC〉   | x5 ⇒ 〈x0,xF〉   | x6 ⇒ 〈x1,x2〉   | x7 ⇒ 〈x1,x5〉
 224   | x8 ⇒ 〈x1,x8〉   | x9 ⇒ 〈x1,xB〉   | xA ⇒ 〈x1,xE〉   | xB ⇒ 〈x2,x1〉
 225   | xC ⇒ 〈x2,x4〉   | xD ⇒ 〈x2,x7〉   | xE ⇒ 〈x2,xA〉   | xF ⇒ 〈x2,xD〉 ]
 226  | x4 ⇒ match e2 with
 227   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x4〉   | x2 ⇒ 〈x0,x8〉   | x3 ⇒ 〈x0,xC〉
 228   | x4 ⇒ 〈x1,x0〉   | x5 ⇒ 〈x1,x4〉   | x6 ⇒ 〈x1,x8〉   | x7 ⇒ 〈x1,xC〉
 229   | x8 ⇒ 〈x2,x0〉   | x9 ⇒ 〈x2,x4〉   | xA ⇒ 〈x2,x8〉   | xB ⇒ 〈x2,xC〉
 230   | xC ⇒ 〈x3,x0〉   | xD ⇒ 〈x3,x4〉   | xE ⇒ 〈x3,x8〉   | xF ⇒ 〈x3,xC〉 ]
 231  | x5 ⇒ match e2 with
 232   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x5〉   | x2 ⇒ 〈x0,xA〉   | x3 ⇒ 〈x0,xF〉
 233   | x4 ⇒ 〈x1,x4〉   | x5 ⇒ 〈x1,x9〉   | x6 ⇒ 〈x1,xE〉   | x7 ⇒ 〈x2,x3〉
 234   | x8 ⇒ 〈x2,x8〉   | x9 ⇒ 〈x2,xD〉   | xA ⇒ 〈x3,x2〉   | xB ⇒ 〈x3,x7〉
 235   | xC ⇒ 〈x3,xC〉   | xD ⇒ 〈x4,x1〉   | xE ⇒ 〈x4,x6〉   | xF ⇒ 〈x4,xB〉 ]
 236  | x6 ⇒ match e2 with
 237   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x6〉   | x2 ⇒ 〈x0,xC〉   | x3 ⇒ 〈x1,x2〉
 238   | x4 ⇒ 〈x1,x8〉   | x5 ⇒ 〈x1,xE〉   | x6 ⇒ 〈x2,x4〉   | x7 ⇒ 〈x2,xA〉
 239   | x8 ⇒ 〈x3,x0〉   | x9 ⇒ 〈x3,x6〉   | xA ⇒ 〈x3,xC〉   | xB ⇒ 〈x4,x2〉
 240   | xC ⇒ 〈x4,x8〉   | xD ⇒ 〈x4,xE〉   | xE ⇒ 〈x5,x4〉   | xF ⇒ 〈x5,xA〉 ]
 241  | x7 ⇒ match e2 with
 242   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x7〉   | x2 ⇒ 〈x0,xE〉   | x3 ⇒ 〈x1,x5〉
 243   | x4 ⇒ 〈x1,xC〉   | x5 ⇒ 〈x2,x3〉   | x6 ⇒ 〈x2,xA〉   | x7 ⇒ 〈x3,x1〉
 244   | x8 ⇒ 〈x3,x8〉   | x9 ⇒ 〈x3,xF〉   | xA ⇒ 〈x4,x6〉   | xB ⇒ 〈x4,xD〉
 245   | xC ⇒ 〈x5,x4〉   | xD ⇒ 〈x5,xB〉   | xE ⇒ 〈x6,x2〉   | xF ⇒ 〈x6,x9〉 ]
 246  | x8 ⇒ match e2 with
 247   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x8〉   | x2 ⇒ 〈x1,x0〉   | x3 ⇒ 〈x1,x8〉
 248   | x4 ⇒ 〈x2,x0〉   | x5 ⇒ 〈x2,x8〉   | x6 ⇒ 〈x3,x0〉   | x7 ⇒ 〈x3,x8〉
 249   | x8 ⇒ 〈x4,x0〉   | x9 ⇒ 〈x4,x8〉   | xA ⇒ 〈x5,x0〉   | xB ⇒ 〈x5,x8〉
 250   | xC ⇒ 〈x6,x0〉   | xD ⇒ 〈x6,x8〉   | xE ⇒ 〈x7,x0〉   | xF ⇒ 〈x7,x8〉 ]
 251  | x9 ⇒ match e2 with
 252   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x9〉   | x2 ⇒ 〈x1,x2〉   | x3 ⇒ 〈x1,xB〉
 253   | x4 ⇒ 〈x2,x4〉   | x5 ⇒ 〈x2,xD〉   | x6 ⇒ 〈x3,x6〉   | x7 ⇒ 〈x3,xF〉
 254   | x8 ⇒ 〈x4,x8〉   | x9 ⇒ 〈x5,x1〉   | xA ⇒ 〈x5,xA〉   | xB ⇒ 〈x6,x3〉
 255   | xC ⇒ 〈x6,xC〉   | xD ⇒ 〈x7,x5〉   | xE ⇒ 〈x7,xE〉   | xF ⇒ 〈x8,x7〉 ]
 256  | xA ⇒ match e2 with
 257   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xA〉   | x2 ⇒ 〈x1,x4〉   | x3 ⇒ 〈x1,xE〉
 258   | x4 ⇒ 〈x2,x8〉   | x5 ⇒ 〈x3,x2〉   | x6 ⇒ 〈x3,xC〉   | x7 ⇒ 〈x4,x6〉
 259   | x8 ⇒ 〈x5,x0〉   | x9 ⇒ 〈x5,xA〉   | xA ⇒ 〈x6,x4〉   | xB ⇒ 〈x6,xE〉
 260   | xC ⇒ 〈x7,x8〉   | xD ⇒ 〈x8,x2〉   | xE ⇒ 〈x8,xC〉   | xF ⇒ 〈x9,x6〉 ]
 261  | xB ⇒ match e2 with
 262   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xB〉   | x2 ⇒ 〈x1,x6〉   | x3 ⇒ 〈x2,x1〉
 263   | x4 ⇒ 〈x2,xC〉   | x5 ⇒ 〈x3,x7〉   | x6 ⇒ 〈x4,x2〉   | x7 ⇒ 〈x4,xD〉
 264   | x8 ⇒ 〈x5,x8〉   | x9 ⇒ 〈x6,x3〉   | xA ⇒ 〈x6,xE〉   | xB ⇒ 〈x7,x9〉
 265   | xC ⇒ 〈x8,x4〉   | xD ⇒ 〈x8,xF〉   | xE ⇒ 〈x9,xA〉   | xF ⇒ 〈xA,x5〉 ]
 266  | xC ⇒ match e2 with
 267   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xC〉   | x2 ⇒ 〈x1,x8〉   | x3 ⇒ 〈x2,x4〉
 268   | x4 ⇒ 〈x3,x0〉   | x5 ⇒ 〈x3,xC〉   | x6 ⇒ 〈x4,x8〉   | x7 ⇒ 〈x5,x4〉
 269   | x8 ⇒ 〈x6,x0〉   | x9 ⇒ 〈x6,xC〉   | xA ⇒ 〈x7,x8〉   | xB ⇒ 〈x8,x4〉
 270   | xC ⇒ 〈x9,x0〉   | xD ⇒ 〈x9,xC〉   | xE ⇒ 〈xA,x8〉   | xF ⇒ 〈xB,x4〉 ]
 271  | xD ⇒ match e2 with
 272   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xD〉   | x2 ⇒ 〈x1,xA〉   | x3 ⇒ 〈x2,x7〉
 273   | x4 ⇒ 〈x3,x4〉   | x5 ⇒ 〈x4,x1〉   | x6 ⇒ 〈x4,xE〉   | x7 ⇒ 〈x5,xB〉
 274   | x8 ⇒ 〈x6,x8〉   | x9 ⇒ 〈x7,x5〉   | xA ⇒ 〈x8,x2〉   | xB ⇒ 〈x8,xF〉
 275   | xC ⇒ 〈x9,xC〉   | xD ⇒ 〈xA,x9〉   | xE ⇒ 〈xB,x6〉   | xF ⇒ 〈xC,x3〉 ]
 276  | xE ⇒ match e2 with
 277   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xE〉   | x2 ⇒ 〈x1,xC〉   | x3 ⇒ 〈x2,xA〉
 278   | x4 ⇒ 〈x3,x8〉   | x5 ⇒ 〈x4,x6〉   | x6 ⇒ 〈x5,x4〉   | x7 ⇒ 〈x6,x2〉
 279   | x8 ⇒ 〈x7,x0〉   | x9 ⇒ 〈x7,xE〉   | xA ⇒ 〈x8,xC〉   | xB ⇒ 〈x9,xA〉
 280   | xC ⇒ 〈xA,x8〉   | xD ⇒ 〈xB,x6〉   | xE ⇒ 〈xC,x4〉   | xF ⇒ 〈xD,x2〉 ]
 281  | xF ⇒ match e2 with
 282   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xF〉   | x2 ⇒ 〈x1,xE〉   | x3 ⇒ 〈x2,xD〉
 283   | x4 ⇒ 〈x3,xC〉   | x5 ⇒ 〈x4,xB〉   | x6 ⇒ 〈x5,xA〉   | x7 ⇒ 〈x6,x9〉
 284   | x8 ⇒ 〈x7,x8〉   | x9 ⇒ 〈x8,x7〉   | xA ⇒ 〈x9,x6〉   | xB ⇒ 〈xA,x5〉
 285   | xC ⇒ 〈xB,x4〉   | xD ⇒ 〈xC,x3〉   | xE ⇒ 〈xD,x2〉   | xF ⇒ 〈xE,x1〉 ]
 286  ].
 287
 288 (* correzione per somma su BCD *)
 289 (* input: halfcarry,carry,X(BCD+BCD) *)
 290 (* output: X',carry' *)
 291 ndefinition daa_b8 ≝
 292 λh,c:bool.λX:byte8.
 293  match lt_b8 X 〈x9,xA〉 with
 294   (* [X:0x00-0x99] *)
 295   (* c' = c *)
 296   (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
 297           [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
 298   [ true ⇒
 299    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
 300     [ true ⇒ X
 301     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
 302    let X'' ≝ match c with
 303     [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
 304     | false ⇒ X' ] in
 305    pair ?? X'' c
 306   (* [X:0x9A-0xFF] *)
 307   (* c' = 1 *)
 308   (* X' = [X:0x9A-0xFF]
 309           [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
 310           [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
 311   | false ⇒
 312    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
 313     [ true ⇒ X
 314     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
 315    let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
 316    pair ?? X'' true
 317   ].
 318
 319 (* iteratore sui byte *)
 320 ndefinition forall_byte8 ≝
 321  λP.
 322   forall_exadecim (λbh.
 323   forall_exadecim (λbl.
 324    P (mk_byte8 bh bl))).