matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_byte8.ml

   1 type byte8 =
   2 Mk_byte8 of Matita_freescale_exadecim.exadecim * Matita_freescale_exadecim.exadecim
   3 ;;
   4
   5 let byte8_rec =
   6 (function f -> (function b ->
   7 (match b with
   8    Mk_byte8(e,e1) -> (f e e1))
   9 ))
  10 ;;
  11
  12 let byte8_rect =
  13 (function f -> (function b ->
  14 (match b with
  15    Mk_byte8(e,e1) -> (f e e1))
  16 ))
  17 ;;
  18
  19 let b8h =
  20 (function w ->
  21 (match w with
  22    Mk_byte8(b8h,b8l) -> b8h)
  23 )
  24 ;;
  25
  26 let b8l =
  27 (function w ->
  28 (match w with
  29    Mk_byte8(b8h,b8l) -> b8l)
  30 )
  31 ;;
  32
  33 let eq_b8 =
  34 (function b1 -> (function b2 -> (Matita_freescale_extra.and_bool (Matita_freescale_exadecim.eq_ex (b8h b1) (b8h b2)) (Matita_freescale_exadecim.eq_ex (b8l b1) (b8l b2)))))
  35 ;;
  36
  37 let lt_b8 =
  38 (function b1 -> (function b2 ->
  39 (match (Matita_freescale_exadecim.lt_ex (b8h b1) (b8h b2)) with
  40    Matita_datatypes_bool.True -> Matita_datatypes_bool.True
  41  | Matita_datatypes_bool.False ->
  42 (match (Matita_freescale_exadecim.gt_ex (b8h b1) (b8h b2)) with
  43    Matita_datatypes_bool.True -> Matita_datatypes_bool.False
  44  | Matita_datatypes_bool.False -> (Matita_freescale_exadecim.lt_ex (b8l b1) (b8l b2)))
  45 )
  46 ))
  47 ;;
  48
  49 let le_b8 =
  50 (function b1 -> (function b2 -> (Matita_freescale_extra.or_bool (eq_b8 b1 b2) (lt_b8 b1 b2))))
  51 ;;
  52
  53 let gt_b8 =
  54 (function b1 -> (function b2 -> (Matita_freescale_extra.not_bool (le_b8 b1 b2))))
  55 ;;
  56
  57 let ge_b8 =
  58 (function b1 -> (function b2 -> (Matita_freescale_extra.not_bool (lt_b8 b1 b2))))
  59 ;;
  60
  61 let and_b8 =
  62 (function b1 -> (function b2 -> (Mk_byte8((Matita_freescale_exadecim.and_ex (b8h b1) (b8h b2)),(Matita_freescale_exadecim.and_ex (b8l b1) (b8l b2))))))
  63 ;;
  64
  65 let or_b8 =
  66 (function b1 -> (function b2 -> (Mk_byte8((Matita_freescale_exadecim.or_ex (b8h b1) (b8h b2)),(Matita_freescale_exadecim.or_ex (b8l b1) (b8l b2))))))
  67 ;;
  68
  69 let xor_b8 =
  70 (function b1 -> (function b2 -> (Mk_byte8((Matita_freescale_exadecim.xor_ex (b8h b1) (b8h b2)),(Matita_freescale_exadecim.xor_ex (b8l b1) (b8l b2))))))
  71 ;;
  72
  73 let rcr_b8 =
  74 (function b -> (function c ->
  75 (match (Matita_freescale_exadecim.rcr_ex (b8h b) c) with
  76    Matita_datatypes_constructors.Pair(bh',c') ->
  77 (match (Matita_freescale_exadecim.rcr_ex (b8l b) c') with
  78    Matita_datatypes_constructors.Pair(bl',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
  79 )
  80 ))
  81 ;;
  82
  83 let shr_b8 =
  84 (function b ->
  85 (match (Matita_freescale_exadecim.rcr_ex (b8h b) Matita_datatypes_bool.False) with
  86    Matita_datatypes_constructors.Pair(bh',c') ->
  87 (match (Matita_freescale_exadecim.rcr_ex (b8l b) c') with
  88    Matita_datatypes_constructors.Pair(bl',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
  89 )
  90 )
  91 ;;
  92
  93 let ror_b8 =
  94 (function b ->
  95 (match (Matita_freescale_exadecim.rcr_ex (b8h b) Matita_datatypes_bool.False) with
  96    Matita_datatypes_constructors.Pair(bh',c') ->
  97 (match (Matita_freescale_exadecim.rcr_ex (b8l b) c') with
  98    Matita_datatypes_constructors.Pair(bl',c'') ->
  99 (match c'' with
 100    Matita_datatypes_bool.True -> (Mk_byte8((Matita_freescale_exadecim.or_ex Matita_freescale_exadecim.X8 bh'),bl'))
 101  | Matita_datatypes_bool.False -> (Mk_byte8(bh',bl')))
 102 )
 103 )
 104 )
 105 ;;
 106
 107 let ror_b8_n =
 108 let rec ror_b8_n =
 109 (function b -> (function n ->
 110 (match n with
 111    Matita_nat_nat.O -> b
 112  | Matita_nat_nat.S(n') -> (ror_b8_n (ror_b8 b) n'))
 113 )) in ror_b8_n
 114 ;;
 115
 116 let rcl_b8 =
 117 (function b -> (function c ->
 118 (match (Matita_freescale_exadecim.rcl_ex (b8l b) c) with
 119    Matita_datatypes_constructors.Pair(bl',c') ->
 120 (match (Matita_freescale_exadecim.rcl_ex (b8h b) c') with
 121    Matita_datatypes_constructors.Pair(bh',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
 122 )
 123 ))
 124 ;;
 125
 126 let shl_b8 =
 127 (function b ->
 128 (match (Matita_freescale_exadecim.rcl_ex (b8l b) Matita_datatypes_bool.False) with
 129    Matita_datatypes_constructors.Pair(bl',c') ->
 130 (match (Matita_freescale_exadecim.rcl_ex (b8h b) c') with
 131    Matita_datatypes_constructors.Pair(bh',c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(bh',bl')),c'')))
 132 )
 133 )
 134 ;;
 135
 136 let rol_b8 =
 137 (function b ->
 138 (match (Matita_freescale_exadecim.rcl_ex (b8l b) Matita_datatypes_bool.False) with
 139    Matita_datatypes_constructors.Pair(bl',c') ->
 140 (match (Matita_freescale_exadecim.rcl_ex (b8h b) c') with
 141    Matita_datatypes_constructors.Pair(bh',c'') ->
 142 (match c'' with
 143    Matita_datatypes_bool.True -> (Mk_byte8(bh',(Matita_freescale_exadecim.or_ex Matita_freescale_exadecim.X1 bl')))
 144  | Matita_datatypes_bool.False -> (Mk_byte8(bh',bl')))
 145 )
 146 )
 147 )
 148 ;;
 149
 150 let rol_b8_n =
 151 let rec rol_b8_n =
 152 (function b -> (function n ->
 153 (match n with
 154    Matita_nat_nat.O -> b
 155  | Matita_nat_nat.S(n') -> (rol_b8_n (rol_b8 b) n'))
 156 )) in rol_b8_n
 157 ;;
 158
 159 let not_b8 =
 160 (function b -> (Mk_byte8((Matita_freescale_exadecim.not_ex (b8h b)),(Matita_freescale_exadecim.not_ex (b8l b)))))
 161 ;;
 162
 163 let plus_b8 =
 164 (function b1 -> (function b2 -> (function c ->
 165 (match (Matita_freescale_exadecim.plus_ex (b8l b1) (b8l b2) c) with
 166    Matita_datatypes_constructors.Pair(l,c') ->
 167 (match (Matita_freescale_exadecim.plus_ex (b8h b1) (b8h b2) c') with
 168    Matita_datatypes_constructors.Pair(h,c'') -> (Matita_datatypes_constructors.Pair((Mk_byte8(h,l)),c'')))
 169 )
 170 )))
 171 ;;
 172
 173 let plus_b8nc =
 174 (function b1 -> (function b2 -> (Matita_datatypes_constructors.fst (plus_b8 b1 b2 Matita_datatypes_bool.False))))
 175 ;;
 176
 177 let plus_b8c =
 178 (function b1 -> (function b2 -> (Matita_datatypes_constructors.snd (plus_b8 b1 b2 Matita_datatypes_bool.False))))
 179 ;;
 180
 181 let mSB_b8 =
 182 (function b -> (Matita_freescale_exadecim.eq_ex Matita_freescale_exadecim.X8 (Matita_freescale_exadecim.and_ex Matita_freescale_exadecim.X8 (b8h b))))
 183 ;;
 184
 185 let nat_of_byte8 =
 186 (function b -> (Matita_nat_plus.plus (Matita_nat_times.times (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))) (Matita_freescale_exadecim.nat_of_exadecim (b8h b))) (Matita_freescale_exadecim.nat_of_exadecim (b8l b))))
 187 ;;
 188
 189 let byte8_of_nat =
 190 (function n -> (Mk_byte8((Matita_freescale_exadecim.exadecim_of_nat (Matita_nat_div_and_mod.div n (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))),(Matita_freescale_exadecim.exadecim_of_nat n))))
 191 ;;
 192
 193 let pred_b8 =
 194 (function b ->
 195 (match (Matita_freescale_exadecim.eq_ex (b8l b) Matita_freescale_exadecim.X0) with
 196    Matita_datatypes_bool.True -> (Mk_byte8((Matita_freescale_exadecim.pred_ex (b8h b)),(Matita_freescale_exadecim.pred_ex (b8l b))))
 197  | Matita_datatypes_bool.False -> (Mk_byte8((b8h b),(Matita_freescale_exadecim.pred_ex (b8l b)))))
 198 )
 199 ;;
 200
 201 let succ_b8 =
 202 (function b ->
 203 (match (Matita_freescale_exadecim.eq_ex (b8l b) Matita_freescale_exadecim.XF) with
 204    Matita_datatypes_bool.True -> (Mk_byte8((Matita_freescale_exadecim.succ_ex (b8h b)),(Matita_freescale_exadecim.succ_ex (b8l b))))
 205  | Matita_datatypes_bool.False -> (Mk_byte8((b8h b),(Matita_freescale_exadecim.succ_ex (b8l b)))))
 206 )
 207 ;;
 208
 209 let compl_b8 =
 210 (function b ->
 211 (match (mSB_b8 b) with
 212    Matita_datatypes_bool.True -> (succ_b8 (not_b8 b))
 213  | Matita_datatypes_bool.False -> (not_b8 (pred_b8 b)))
 214 )
 215 ;;
 216
 217 let mul_ex =
 218 (function e1 -> (function e2 ->
 219 (match e1 with
 220    Matita_freescale_exadecim.X0 ->
 221 (match e2 with
 222    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 223  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 224  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 225  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 226  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 227  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 228  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 229  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 230  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 231  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 232  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 233  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 234  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 235  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 236  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 237  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 238
 239  | Matita_freescale_exadecim.X1 ->
 240 (match e2 with
 241    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 242  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))
 243  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
 244  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
 245  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 246  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
 247  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 248  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
 249  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 250  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
 251  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 252  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
 253  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 254  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
 255  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 256  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)))
 257
 258  | Matita_freescale_exadecim.X2 ->
 259 (match e2 with
 260    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 261  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
 262  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 263  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 264  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 265  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 266  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 267  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 268  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 269  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 270  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 271  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
 272  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 273  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
 274  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 275  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE)))
 276
 277  | Matita_freescale_exadecim.X3 ->
 278 (match e2 with
 279    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 280  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
 281  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 282  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
 283  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 284  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
 285  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 286  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
 287  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 288  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
 289  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 290  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))
 291  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
 292  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X7))
 293  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
 294  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD)))
 295
 296  | Matita_freescale_exadecim.X4 ->
 297 (match e2 with
 298    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 299  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 300  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 301  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 302  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 303  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 304  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 305  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 306  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))
 307  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
 308  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
 309  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC))
 310  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
 311  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4))
 312  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
 313  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC)))
 314
 315  | Matita_freescale_exadecim.X5 ->
 316 (match e2 with
 317    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 318  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
 319  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 320  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
 321  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 322  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9))
 323  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 324  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))
 325  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
 326  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
 327  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2))
 328  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X7))
 329  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
 330  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X1))
 331  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
 332  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB)))
 333
 334  | Matita_freescale_exadecim.X6 ->
 335 (match e2 with
 336    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 337  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 338  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 339  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 340  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 341  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 342  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
 343  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
 344  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
 345  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X6))
 346  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
 347  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X2))
 348  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
 349  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XE))
 350  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
 351  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA)))
 352
 353  | Matita_freescale_exadecim.X7 ->
 354 (match e2 with
 355    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 356  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
 357  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 358  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
 359  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 360  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))
 361  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
 362  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X1))
 363  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
 364  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))
 365  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
 366  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XD))
 367  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
 368  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XB))
 369  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X2))
 370  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X9)))
 371
 372  | Matita_freescale_exadecim.X8 ->
 373 (match e2 with
 374    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 375  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 376  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 377  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 378  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))
 379  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
 380  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
 381  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
 382  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0))
 383  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
 384  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0))
 385  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X8))
 386  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0))
 387  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X8))
 388  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))
 389  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8)))
 390
 391  | Matita_freescale_exadecim.X9 ->
 392 (match e2 with
 393    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 394  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
 395  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 396  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
 397  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
 398  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
 399  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X6))
 400  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))
 401  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
 402  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X1))
 403  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA))
 404  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X3))
 405  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XC))
 406  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X5))
 407  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XE))
 408  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X7)))
 409
 410  | Matita_freescale_exadecim.XA ->
 411 (match e2 with
 412    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 413  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 414  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 415  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 416  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
 417  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2))
 418  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
 419  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
 420  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0))
 421  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA))
 422  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4))
 423  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XE))
 424  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8))
 425  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X2))
 426  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XC))
 427  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X6)))
 428
 429  | Matita_freescale_exadecim.XB ->
 430 (match e2 with
 431    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 432  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
 433  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
 434  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))
 435  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC))
 436  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X7))
 437  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X2))
 438  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XD))
 439  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X8))
 440  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X3))
 441  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XE))
 442  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X9))
 443  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X4))
 444  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XF))
 445  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA))
 446  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X5)))
 447
 448  | Matita_freescale_exadecim.XC ->
 449 (match e2 with
 450    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 451  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 452  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 453  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
 454  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
 455  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
 456  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
 457  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
 458  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0))
 459  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XC))
 460  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8))
 461  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X4))
 462  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X0))
 463  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XC))
 464  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X8))
 465  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X4)))
 466
 467  | Matita_freescale_exadecim.XD ->
 468 (match e2 with
 469    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 470  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
 471  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
 472  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X7))
 473  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4))
 474  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X1))
 475  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XE))
 476  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XB))
 477  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X8))
 478  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X5))
 479  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X2))
 480  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XF))
 481  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XC))
 482  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X9))
 483  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X6))
 484  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X3)))
 485
 486  | Matita_freescale_exadecim.XE ->
 487 (match e2 with
 488    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 489  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 490  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 491  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
 492  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
 493  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
 494  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
 495  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X2))
 496  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))
 497  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XE))
 498  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XC))
 499  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA))
 500  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X8))
 501  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X6))
 502  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X4))
 503  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X2)))
 504
 505  | Matita_freescale_exadecim.XF ->
 506 (match e2 with
 507    Matita_freescale_exadecim.X0 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 508  | Matita_freescale_exadecim.X1 -> (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
 509  | Matita_freescale_exadecim.X2 -> (Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 510  | Matita_freescale_exadecim.X3 -> (Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
 511  | Matita_freescale_exadecim.X4 -> (Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
 512  | Matita_freescale_exadecim.X5 -> (Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB))
 513  | Matita_freescale_exadecim.X6 -> (Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA))
 514  | Matita_freescale_exadecim.X7 -> (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X9))
 515  | Matita_freescale_exadecim.X8 -> (Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8))
 516  | Matita_freescale_exadecim.X9 -> (Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X7))
 517  | Matita_freescale_exadecim.XA -> (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X6))
 518  | Matita_freescale_exadecim.XB -> (Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X5))
 519  | Matita_freescale_exadecim.XC -> (Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X4))
 520  | Matita_freescale_exadecim.XD -> (Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X3))
 521  | Matita_freescale_exadecim.XE -> (Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X2))
 522  | Matita_freescale_exadecim.XF -> (Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X1)))
 523 )
 524 ))
 525 ;;
 526
 527 let daa_b8 =
 528 (function h -> (function c -> (function x ->
 529 (match (lt_b8 x (Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA))) with
 530    Matita_datatypes_bool.True -> (let x' =
 531 (match (Matita_freescale_extra.and_bool (Matita_freescale_exadecim.lt_ex (b8l x) Matita_freescale_exadecim.XA) (Matita_freescale_extra.not_bool h)) with
 532    Matita_datatypes_bool.True -> x
 533  | Matita_datatypes_bool.False -> (plus_b8nc x (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))
 534  in (let x'' =
 535 (match c with
 536    Matita_datatypes_bool.True -> (plus_b8nc x' (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)))
 537  | Matita_datatypes_bool.False -> x')
 538  in (Matita_datatypes_constructors.Pair(x'',c))))
 539  | Matita_datatypes_bool.False -> (let x' =
 540 (match (Matita_freescale_extra.and_bool (Matita_freescale_exadecim.lt_ex (b8l x) Matita_freescale_exadecim.XA) (Matita_freescale_extra.not_bool h)) with
 541    Matita_datatypes_bool.True -> x
 542  | Matita_datatypes_bool.False -> (plus_b8nc x (Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))
 543  in (let x'' = (plus_b8nc x' (Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0))) in (Matita_datatypes_constructors.Pair(x'',Matita_datatypes_bool.True)))))
 544 )))
 545 ;;
 546
 547 let forall_byte8 =
 548 (function p -> (Matita_freescale_exadecim.forall_exadecim (function bh -> (Matita_freescale_exadecim.forall_exadecim (function bl -> (p (Mk_byte8(bh,bl))))))))
 549 ;;
 550