helm/software/matita/contribs/ng_assembly/freescale/exadecim.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/bool.ma".
  28 include "freescale/prod.ma".
  29 include "freescale/nat.ma".
  30
  31 (* *********** *)
  32 (* ESADECIMALI *)
  33 (* *********** *)
  34
  35 ninductive exadecim : Type ≝
  36   x0: exadecim
  37 | x1: exadecim
  38 | x2: exadecim
  39 | x3: exadecim
  40 | x4: exadecim
  41 | x5: exadecim
  42 | x6: exadecim
  43 | x7: exadecim
  44 | x8: exadecim
  45 | x9: exadecim
  46 | xA: exadecim
  47 | xB: exadecim
  48 | xC: exadecim
  49 | xD: exadecim
  50 | xE: exadecim
  51 | xF: exadecim.
  52
  53 ndefinition exadecim_ind :
  54  ΠP:exadecim → Prop.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
  55                     P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
  56 λP:exadecim → Prop.
  57 λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
  58 λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
  59  match e with
  60   [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
  61   | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].
  62
  63 ndefinition exadecim_rec :
  64  ΠP:exadecim → Set.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
  65                     P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
  66 λP:exadecim → Set.
  67 λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
  68 λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
  69  match e with
  70   [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
  71   | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].
  72
  73 ndefinition exadecim_rect :
  74  ΠP:exadecim → Type.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
  75                     P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
  76 λP:exadecim → Type.
  77 λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
  78 λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
  79  match e with
  80   [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
  81   | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].
  82
  83 (* operatore = *)
  84 ndefinition eq_ex ≝
  85 λe1,e2:exadecim.
  86  match e1 with
  87   [ x0 ⇒ match e2 with
  88    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  89    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  90    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  91    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  92   | x1 ⇒ match e2 with
  93    [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
  94    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  95    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  96    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  97   | x2 ⇒ match e2 with
  98    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
  99    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 100    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 101    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 102   | x3 ⇒ match e2 with
 103    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 104    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 105    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 106    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 107   | x4 ⇒ match e2 with
 108    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 109    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 110    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 111    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 112   | x5 ⇒ match e2 with
 113    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 114    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 115    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 116    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 117   | x6 ⇒ match e2 with
 118    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 119    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
 120    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 121    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 122   | x7 ⇒ match e2 with
 123    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 124    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 125    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 126    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 127   | x8 ⇒ match e2 with
 128    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 129    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 130    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 131    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 132   | x9 ⇒ match e2 with
 133    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 134    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 135    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 136    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 137   | xA ⇒ match e2 with
 138    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 139    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 140    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 141    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 142   | xB ⇒ match e2 with
 143    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 144    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 145    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 146    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 147   | xC ⇒ match e2 with
 148    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 149    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 150    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 151    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 152   | xD ⇒ match e2 with
 153    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 154    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 155    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 156    | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 157   | xE ⇒ match e2 with
 158    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 159    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 160    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 161    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ]
 162   | xF ⇒ match e2 with
 163    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 164    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 165    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 166    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
 167   ].
 168
 169 (* operatore < *)
 170 ndefinition lt_ex ≝
 171 λe1,e2:exadecim.
 172  match e1 with
 173   [ x0 ⇒ match e2 with
 174    [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
 175    | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
 176    | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true
 177    | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
 178   | x1 ⇒ match e2 with
 179    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
 180    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
 181    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true
 182    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ]
 183   | x2 ⇒ match e2 with
 184    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 185    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 186    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 187    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 188   | x3 ⇒ match e2 with
 189    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 190    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 191    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 192    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 193   | x4 ⇒ match e2 with
 194    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 195    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 196    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 197    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 198   | x5 ⇒ match e2 with
 199    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 200    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
 201    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 202    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 203   | x6 ⇒ match e2 with
 204    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 205    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 206    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 207    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 208   | x7 ⇒ match e2 with
 209    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 210    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 211    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 212    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 213   | x8 ⇒ match e2 with
 214    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 215    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 216    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 217    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 218   | x9 ⇒ match e2 with
 219    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 220    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 221    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true
 222    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 223   | xA ⇒ match e2 with
 224    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 225    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 226    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 227    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 228   | xB ⇒ match e2 with
 229    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 230    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 231    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 232    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 233   | xC ⇒ match e2 with
 234    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 235    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 236    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 237    | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 238   | xD ⇒ match e2 with
 239    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 240    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 241    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 242    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ]
 243   | xE ⇒ match e2 with
 244    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 245    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 246    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 247    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
 248   | xF ⇒ match e2 with
 249    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 250    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 251    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 252    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 253   ].
 254
 255 (* operatore ≤ *)
 256 ndefinition le_ex ≝
 257 λe1,e2:exadecim.
 258  match e1 with
 259   [ x0 ⇒ match e2 with
 260    [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
 261    | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
 262    | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
 263    | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
 264   | x1 ⇒ match e2 with
 265    [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
 266    | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
 267    | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true
 268    | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
 269   | x2 ⇒ match e2 with
 270    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
 271    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
 272    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true
 273    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ]
 274   | x3 ⇒ match e2 with
 275    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 276    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 277    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 278    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 279   | x4 ⇒ match e2 with
 280    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 281    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 282    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 283    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 284   | x5 ⇒ match e2 with
 285    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 286    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 287    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 288    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 289   | x6 ⇒ match e2 with
 290    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 291    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
 292    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 293    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 294   | x7 ⇒ match e2 with
 295    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 296    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 297    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 298    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 299   | x8 ⇒ match e2 with
 300    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 301    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 302    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 303    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 304   | x9 ⇒ match e2 with
 305    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 306    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 307    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 308    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 309   | xA ⇒ match e2 with
 310    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 311    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 312    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true
 313    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 314   | xB ⇒ match e2 with
 315    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 316    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 317    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 318    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 319   | xC ⇒ match e2 with
 320    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 321    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 322    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 323    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 324   | xD ⇒ match e2 with
 325    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 326    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 327    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 328    | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 329   | xE ⇒ match e2 with
 330    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 331    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 332    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 333    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ]
 334   | xF ⇒ match e2 with
 335    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 336    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 337    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 338    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
 339   ].
 340
 341 (* operatore > *)
 342 ndefinition gt_ex ≝
 343 λe1,e2:exadecim.
 344  match e1 with
 345   [ x0 ⇒ match e2 with
 346    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 347    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 348    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 349    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 350   | x1 ⇒ match e2 with
 351    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 352    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 353    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 354    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 355   | x2 ⇒ match e2 with
 356    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
 357    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 358    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 359    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 360   | x3 ⇒ match e2 with
 361    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false
 362    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 363    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 364    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 365   | x4 ⇒ match e2 with
 366    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 367    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 368    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 369    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 370   | x5 ⇒ match e2 with
 371    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 372    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 373    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 374    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 375   | x6 ⇒ match e2 with
 376    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 377    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 378    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 379    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 380   | x7 ⇒ match e2 with
 381    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 382    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
 383    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 384    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 385   | x8 ⇒ match e2 with
 386    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 387    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 388    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 389    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 390   | x9 ⇒ match e2 with
 391    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 392    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 393    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 394    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 395   | xA ⇒ match e2 with
 396    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 397    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 398    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 399    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 400   | xB ⇒ match e2 with
 401    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 402    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 403    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false
 404    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 405   | xC ⇒ match e2 with
 406    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 407    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 408    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 409    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 410   | xD ⇒ match e2 with
 411    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 412    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 413    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 414    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 415   | xE ⇒ match e2 with
 416    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 417    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 418    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 419    | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 420   | xF ⇒ match e2 with
 421    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 422    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 423    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 424    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
 425   ].
 426
 427 (* operatore ≥ *)
 428 ndefinition ge_ex ≝
 429 λe1,e2:exadecim.
 430  match e1 with
 431   [ x0 ⇒ match e2 with
 432    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 433    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 434    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 435    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 436   | x1 ⇒ match e2 with
 437    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
 438    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 439    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 440    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 441   | x2 ⇒ match e2 with
 442    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false
 443    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 444    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 445    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 446   | x3 ⇒ match e2 with
 447    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 448    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 449    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 450    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 451   | x4 ⇒ match e2 with
 452    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 453    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 454    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 455    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 456   | x5 ⇒ match e2 with
 457    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 458    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 459    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 460    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 461   | x6 ⇒ match e2 with
 462    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 463    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
 464    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 465    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 466   | x7 ⇒ match e2 with
 467    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 468    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 469    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 470    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 471   | x8 ⇒ match e2 with
 472    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 473    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 474    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 475    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 476   | x9 ⇒ match e2 with
 477    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 478    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 479    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 480    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 481   | xA ⇒ match e2 with
 482    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 483    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 484    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false
 485    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 486   | xB ⇒ match e2 with
 487    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 488    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 489    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 490    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 491   | xC ⇒ match e2 with
 492    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 493    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 494    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 495    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 496   | xD ⇒ match e2 with
 497    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 498    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 499    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 500    | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 501   | xE ⇒ match e2 with
 502    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 503    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 504    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 505    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
 506   | xF ⇒ match e2 with
 507    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 508    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 509    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 510    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 511   ].
 512
 513 (* operatore and *)
 514 ndefinition and_ex ≝
 515 λe1,e2:exadecim.match e1 with
 516  [ x0 ⇒ match e2 with
 517   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 518   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
 519   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
 520   | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
 521  | x1 ⇒ match e2 with
 522   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 523   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
 524   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
 525   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
 526  | x2 ⇒ match e2 with
 527   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 528   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
 529   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
 530   | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
 531  | x3 ⇒ match e2 with
 532   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 533   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
 534   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
 535   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
 536  | x4 ⇒ match e2 with
 537   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 538   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
 539   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
 540   | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
 541  | x5 ⇒ match e2 with
 542   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 543   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
 544   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
 545   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
 546  | x6 ⇒ match e2 with
 547   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 548   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
 549   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
 550   | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
 551  | x7 ⇒ match e2 with
 552   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 553   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 554   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
 555   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
 556  | x8 ⇒ match e2 with
 557   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 558   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
 559   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
 560   | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
 561  | x9 ⇒ match e2 with
 562   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 563   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
 564   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
 565   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
 566  | xA ⇒ match e2 with
 567   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 568   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
 569   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
 570   | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
 571  | xB ⇒ match e2 with
 572   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 573   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
 574   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 575   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
 576  | xC ⇒ match e2 with
 577   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 578   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
 579   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
 580   | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
 581  | xD ⇒ match e2 with
 582   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 583   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
 584   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
 585   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
 586  | xE ⇒ match e2 with
 587   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 588   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
 589   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
 590   | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
 591  | xF ⇒ match e2 with
 592   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 593   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 594   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 595   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 596  ].
 597
 598 (* operatore or *)
 599 ndefinition or_ex ≝
 600 λe1,e2:exadecim.match e1 with
 601  [ x0 ⇒ match e2 with
 602   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 603   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 604   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 605   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 606  | x1 ⇒ match e2 with
 607   [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
 608   | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
 609   | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
 610   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 611  | x2 ⇒ match e2 with
 612   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
 613   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
 614   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
 615   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 616  | x3 ⇒ match e2 with
 617   [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
 618   | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
 619   | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
 620   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 621  | x4 ⇒ match e2 with
 622   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
 623   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 624   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
 625   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 626  | x5 ⇒ match e2 with
 627   [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
 628   | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
 629   | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
 630   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 631  | x6 ⇒ match e2 with
 632   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
 633   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
 634   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
 635   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 636  | x7 ⇒ match e2 with
 637   [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
 638   | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
 639   | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
 640   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 641  | x8 ⇒ match e2 with
 642   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
 643   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
 644   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 645   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 646  | x9 ⇒ match e2 with
 647   [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
 648   | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
 649   | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
 650   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 651  | xA ⇒ match e2 with
 652   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
 653   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
 654   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
 655   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 656  | xB ⇒ match e2 with
 657   [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
 658   | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
 659   | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
 660   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 661  | xC ⇒ match e2 with
 662   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
 663   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
 664   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
 665   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 666  | xD ⇒ match e2 with
 667   [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
 668   | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
 669   | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
 670   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 671  | xE ⇒ match e2 with
 672   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
 673   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
 674   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
 675   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 676  | xF ⇒ match e2 with
 677   [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
 678   | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
 679   | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
 680   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 681  ].
 682
 683 (* operatore xor *)
 684 ndefinition xor_ex ≝
 685 λe1,e2:exadecim.match e1 with
 686  [ x0 ⇒ match e2 with
 687   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 688   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 689   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 690   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 691  | x1 ⇒ match e2 with
 692   [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
 693   | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
 694   | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
 695   | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
 696  | x2 ⇒ match e2 with
 697   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
 698   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
 699   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
 700   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
 701  | x3 ⇒ match e2 with
 702   [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
 703   | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
 704   | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
 705   | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
 706  | x4 ⇒ match e2 with
 707   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
 708   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
 709   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
 710   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
 711  | x5 ⇒ match e2 with
 712   [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
 713   | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
 714   | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
 715   | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
 716  | x6 ⇒ match e2 with
 717   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
 718   | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
 719   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
 720   | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
 721  | x7 ⇒ match e2 with
 722   [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
 723   | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
 724   | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
 725   | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
 726  | x8 ⇒ match e2 with
 727   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
 728   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
 729   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
 730   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
 731  | x9 ⇒ match e2 with
 732   [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
 733   | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
 734   | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
 735   | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
 736  | xA ⇒ match e2 with
 737   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
 738   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
 739   | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
 740   | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
 741  | xB ⇒ match e2 with
 742   [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
 743   | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
 744   | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
 745   | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
 746  | xC ⇒ match e2 with
 747   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
 748   | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
 749   | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
 750   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
 751  | xD ⇒ match e2 with
 752   [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
 753   | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
 754   | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
 755   | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
 756  | xE ⇒ match e2 with
 757   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
 758   | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
 759   | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
 760   | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
 761  | xF ⇒ match e2 with
 762   [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
 763   | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
 764   | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
 765   | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
 766  ].
 767
 768 (* operatore rotazione destra con carry *)
 769 ndefinition rcr_ex ≝
 770 λe:exadecim.λc:bool.match c with
 771  [ true ⇒ match e with
 772   [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
 773   | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
 774   | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
 775   | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
 776   | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
 777   | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
 778   | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
 779   | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
 780  | false ⇒ match e with
 781   [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
 782   | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
 783   | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
 784   | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
 785   | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
 786   | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
 787   | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
 788   | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
 789  ].
 790
 791 (* operatore shift destro *)
 792 ndefinition shr_ex ≝
 793 λe:exadecim.match e with
 794  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
 795  | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
 796  | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
 797  | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
 798  | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
 799  | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
 800  | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
 801  | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
 802
 803 (* operatore rotazione destra *)
 804 ndefinition ror_ex ≝
 805 λe:exadecim.match e with
 806  [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
 807  | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
 808  | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
 809  | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
 810
 811 (* operatore rotazione destra n-volte *)
 812 nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
 813  match n with
 814   [ O ⇒ e
 815   | S n' ⇒ ror_ex_n (ror_ex e) n' ].
 816
 817 (* operatore rotazione sinistra con carry *)
 818 ndefinition rcl_ex ≝
 819 λe:exadecim.λc:bool.match c with
 820  [ true ⇒ match e with
 821   [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
 822   | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
 823   | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
 824   | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
 825   | x8 ⇒ pair exadecim bool x1 true  | x9 ⇒ pair exadecim bool x3 true
 826   | xA ⇒ pair exadecim bool x5 true  | xB ⇒ pair exadecim bool x7 true
 827   | xC ⇒ pair exadecim bool x9 true  | xD ⇒ pair exadecim bool xB true
 828   | xE ⇒ pair exadecim bool xD true  | xF ⇒ pair exadecim bool xF true ]
 829  | false ⇒ match e with
 830   [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
 831   | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
 832   | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
 833   | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
 834   | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
 835   | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
 836   | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
 837   | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ]
 838  ].
 839
 840 (* operatore shift sinistro *)
 841 ndefinition shl_ex ≝
 842 λe:exadecim.match e with
 843  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
 844  | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
 845  | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
 846  | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
 847  | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
 848  | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
 849  | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
 850  | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ].
 851
 852 (* operatore rotazione sinistra *)
 853 ndefinition rol_ex ≝
 854 λe:exadecim.match e with
 855  [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
 856  | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
 857  | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
 858  | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
 859
 860 (* operatore rotazione sinistra n-volte *)
 861 nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
 862  match n with
 863   [ O ⇒ e
 864   | S n' ⇒ rol_ex_n (rol_ex e) n' ].
 865
 866 (* operatore not/complemento a 1 *)
 867 ndefinition not_ex ≝
 868 λe:exadecim.match e with
 869  [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
 870  | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
 871  | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
 872  | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
 873
 874 (* operatore somma con carry *)
 875 ndefinition plus_ex ≝
 876 λe1,e2:exadecim.λc:bool.
 877   match c with
 878    [ true ⇒
 879       match e1 with
 880        [ x0 ⇒
 881            match e2 with
 882             [ x0 ⇒ pair exadecim bool x1 false
 883             | x1 ⇒ pair exadecim bool x2 false
 884             | x2 ⇒ pair exadecim bool x3 false
 885             | x3 ⇒ pair exadecim bool x4 false
 886             | x4 ⇒ pair exadecim bool x5 false
 887             | x5 ⇒ pair exadecim bool x6 false
 888             | x6 ⇒ pair exadecim bool x7 false
 889             | x7 ⇒ pair exadecim bool x8 false
 890             | x8 ⇒ pair exadecim bool x9 false
 891             | x9 ⇒ pair exadecim bool xA false
 892             | xA ⇒ pair exadecim bool xB false
 893             | xB ⇒ pair exadecim bool xC false
 894             | xC ⇒ pair exadecim bool xD false
 895             | xD ⇒ pair exadecim bool xE false
 896             | xE ⇒ pair exadecim bool xF false
 897             | xF ⇒ pair exadecim bool x0 true ]
 898        | x1 ⇒
 899            match e2 with
 900             [ x0 ⇒ pair exadecim bool x2 false
 901             | x1 ⇒ pair exadecim bool x3 false
 902             | x2 ⇒ pair exadecim bool x4 false
 903             | x3 ⇒ pair exadecim bool x5 false
 904             | x4 ⇒ pair exadecim bool x6 false
 905             | x5 ⇒ pair exadecim bool x7 false
 906             | x6 ⇒ pair exadecim bool x8 false
 907             | x7 ⇒ pair exadecim bool x9 false
 908             | x8 ⇒ pair exadecim bool xA false
 909             | x9 ⇒ pair exadecim bool xB false
 910             | xA ⇒ pair exadecim bool xC false
 911             | xB ⇒ pair exadecim bool xD false
 912             | xC ⇒ pair exadecim bool xE false
 913             | xD ⇒ pair exadecim bool xF false
 914             | xE ⇒ pair exadecim bool x0 true
 915             | xF ⇒ pair exadecim bool x1 true ]
 916        | x2 ⇒
 917            match e2 with
 918             [ x0 ⇒ pair exadecim bool x3 false
 919             | x1 ⇒ pair exadecim bool x4 false
 920             | x2 ⇒ pair exadecim bool x5 false
 921             | x3 ⇒ pair exadecim bool x6 false
 922             | x4 ⇒ pair exadecim bool x7 false
 923             | x5 ⇒ pair exadecim bool x8 false
 924             | x6 ⇒ pair exadecim bool x9 false
 925             | x7 ⇒ pair exadecim bool xA false
 926             | x8 ⇒ pair exadecim bool xB false
 927             | x9 ⇒ pair exadecim bool xC false
 928             | xA ⇒ pair exadecim bool xD false
 929             | xB ⇒ pair exadecim bool xE false
 930             | xC ⇒ pair exadecim bool xF false
 931             | xD ⇒ pair exadecim bool x0 true
 932             | xE ⇒ pair exadecim bool x1 true
 933             | xF ⇒ pair exadecim bool x2 true ]
 934        | x3 ⇒
 935            match e2 with
 936             [ x0 ⇒ pair exadecim bool x4 false
 937             | x1 ⇒ pair exadecim bool x5 false
 938             | x2 ⇒ pair exadecim bool x6 false
 939             | x3 ⇒ pair exadecim bool x7 false
 940             | x4 ⇒ pair exadecim bool x8 false
 941             | x5 ⇒ pair exadecim bool x9 false
 942             | x6 ⇒ pair exadecim bool xA false
 943             | x7 ⇒ pair exadecim bool xB false
 944             | x8 ⇒ pair exadecim bool xC false
 945             | x9 ⇒ pair exadecim bool xD false
 946             | xA ⇒ pair exadecim bool xE false
 947             | xB ⇒ pair exadecim bool xF false
 948             | xC ⇒ pair exadecim bool x0 true
 949             | xD ⇒ pair exadecim bool x1 true
 950             | xE ⇒ pair exadecim bool x2 true
 951             | xF ⇒ pair exadecim bool x3 true ]
 952        | x4 ⇒
 953            match e2 with
 954             [ x0 ⇒ pair exadecim bool x5 false
 955             | x1 ⇒ pair exadecim bool x6 false
 956             | x2 ⇒ pair exadecim bool x7 false
 957             | x3 ⇒ pair exadecim bool x8 false
 958             | x4 ⇒ pair exadecim bool x9 false
 959             | x5 ⇒ pair exadecim bool xA false
 960             | x6 ⇒ pair exadecim bool xB false
 961             | x7 ⇒ pair exadecim bool xC false
 962             | x8 ⇒ pair exadecim bool xD false
 963             | x9 ⇒ pair exadecim bool xE false
 964             | xA ⇒ pair exadecim bool xF false
 965             | xB ⇒ pair exadecim bool x0 true
 966             | xC ⇒ pair exadecim bool x1 true
 967             | xD ⇒ pair exadecim bool x2 true
 968             | xE ⇒ pair exadecim bool x3 true
 969             | xF ⇒ pair exadecim bool x4 true ]
 970        | x5 ⇒
 971            match e2 with
 972             [ x0 ⇒ pair exadecim bool x6 false
 973             | x1 ⇒ pair exadecim bool x7 false
 974             | x2 ⇒ pair exadecim bool x8 false
 975             | x3 ⇒ pair exadecim bool x9 false
 976             | x4 ⇒ pair exadecim bool xA false
 977             | x5 ⇒ pair exadecim bool xB false
 978             | x6 ⇒ pair exadecim bool xC false
 979             | x7 ⇒ pair exadecim bool xD false
 980             | x8 ⇒ pair exadecim bool xE false
 981             | x9 ⇒ pair exadecim bool xF false
 982             | xA ⇒ pair exadecim bool x0 true
 983             | xB ⇒ pair exadecim bool x1 true
 984             | xC ⇒ pair exadecim bool x2 true
 985             | xD ⇒ pair exadecim bool x3 true
 986             | xE ⇒ pair exadecim bool x4 true
 987             | xF ⇒ pair exadecim bool x5 true ]
 988        | x6 ⇒
 989            match e2 with
 990             [ x0 ⇒ pair exadecim bool x7 false
 991             | x1 ⇒ pair exadecim bool x8 false
 992             | x2 ⇒ pair exadecim bool x9 false
 993             | x3 ⇒ pair exadecim bool xA false
 994             | x4 ⇒ pair exadecim bool xB false
 995             | x5 ⇒ pair exadecim bool xC false
 996             | x6 ⇒ pair exadecim bool xD false
 997             | x7 ⇒ pair exadecim bool xE false
 998             | x8 ⇒ pair exadecim bool xF false
 999             | x9 ⇒ pair exadecim bool x0 true
1000             | xA ⇒ pair exadecim bool x1 true
1001             | xB ⇒ pair exadecim bool x2 true
1002             | xC ⇒ pair exadecim bool x3 true
1003             | xD ⇒ pair exadecim bool x4 true
1004             | xE ⇒ pair exadecim bool x5 true
1005             | xF ⇒ pair exadecim bool x6 true ]
1006        | x7 ⇒
1007            match e2 with
1008             [ x0 ⇒ pair exadecim bool x8 false
1009             | x1 ⇒ pair exadecim bool x9 false
1010             | x2 ⇒ pair exadecim bool xA false
1011             | x3 ⇒ pair exadecim bool xB false
1012             | x4 ⇒ pair exadecim bool xC false
1013             | x5 ⇒ pair exadecim bool xD false
1014             | x6 ⇒ pair exadecim bool xE false
1015             | x7 ⇒ pair exadecim bool xF false
1016             | x8 ⇒ pair exadecim bool x0 true
1017             | x9 ⇒ pair exadecim bool x1 true
1018             | xA ⇒ pair exadecim bool x2 true
1019             | xB ⇒ pair exadecim bool x3 true
1020             | xC ⇒ pair exadecim bool x4 true
1021             | xD ⇒ pair exadecim bool x5 true
1022             | xE ⇒ pair exadecim bool x6 true
1023             | xF ⇒ pair exadecim bool x7 true ]
1024        | x8 ⇒
1025            match e2 with
1026             [ x0 ⇒ pair exadecim bool x9 false
1027             | x1 ⇒ pair exadecim bool xA false
1028             | x2 ⇒ pair exadecim bool xB false
1029             | x3 ⇒ pair exadecim bool xC false
1030             | x4 ⇒ pair exadecim bool xD false
1031             | x5 ⇒ pair exadecim bool xE false
1032             | x6 ⇒ pair exadecim bool xF false
1033             | x7 ⇒ pair exadecim bool x0 true
1034             | x8 ⇒ pair exadecim bool x1 true
1035             | x9 ⇒ pair exadecim bool x2 true
1036             | xA ⇒ pair exadecim bool x3 true
1037             | xB ⇒ pair exadecim bool x4 true
1038             | xC ⇒ pair exadecim bool x5 true
1039             | xD ⇒ pair exadecim bool x6 true
1040             | xE ⇒ pair exadecim bool x7 true
1041             | xF ⇒ pair exadecim bool x8 true ]
1042        | x9 ⇒
1043            match e2 with
1044             [ x0 ⇒ pair exadecim bool xA false
1045             | x1 ⇒ pair exadecim bool xB false
1046             | x2 ⇒ pair exadecim bool xC false
1047             | x3 ⇒ pair exadecim bool xD false
1048             | x4 ⇒ pair exadecim bool xE false
1049             | x5 ⇒ pair exadecim bool xF false
1050             | x6 ⇒ pair exadecim bool x0 true
1051             | x7 ⇒ pair exadecim bool x1 true
1052             | x8 ⇒ pair exadecim bool x2 true
1053             | x9 ⇒ pair exadecim bool x3 true
1054             | xA ⇒ pair exadecim bool x4 true
1055             | xB ⇒ pair exadecim bool x5 true
1056             | xC ⇒ pair exadecim bool x6 true
1057             | xD ⇒ pair exadecim bool x7 true
1058             | xE ⇒ pair exadecim bool x8 true
1059             | xF ⇒ pair exadecim bool x9 true ]
1060        | xA ⇒
1061            match e2 with
1062             [ x0 ⇒ pair exadecim bool xB false
1063             | x1 ⇒ pair exadecim bool xC false
1064             | x2 ⇒ pair exadecim bool xD false
1065             | x3 ⇒ pair exadecim bool xE false
1066             | x4 ⇒ pair exadecim bool xF false
1067             | x5 ⇒ pair exadecim bool x0 true
1068             | x6 ⇒ pair exadecim bool x1 true
1069             | x7 ⇒ pair exadecim bool x2 true
1070             | x8 ⇒ pair exadecim bool x3 true
1071             | x9 ⇒ pair exadecim bool x4 true
1072             | xA ⇒ pair exadecim bool x5 true
1073             | xB ⇒ pair exadecim bool x6 true
1074             | xC ⇒ pair exadecim bool x7 true
1075             | xD ⇒ pair exadecim bool x8 true
1076             | xE ⇒ pair exadecim bool x9 true
1077             | xF ⇒ pair exadecim bool xA true ]
1078        | xB ⇒
1079            match e2 with
1080             [ x0 ⇒ pair exadecim bool xC false
1081             | x1 ⇒ pair exadecim bool xD false
1082             | x2 ⇒ pair exadecim bool xE false
1083             | x3 ⇒ pair exadecim bool xF false
1084             | x4 ⇒ pair exadecim bool x0 true
1085             | x5 ⇒ pair exadecim bool x1 true
1086             | x6 ⇒ pair exadecim bool x2 true
1087             | x7 ⇒ pair exadecim bool x3 true
1088             | x8 ⇒ pair exadecim bool x4 true
1089             | x9 ⇒ pair exadecim bool x5 true
1090             | xA ⇒ pair exadecim bool x6 true
1091             | xB ⇒ pair exadecim bool x7 true
1092             | xC ⇒ pair exadecim bool x8 true
1093             | xD ⇒ pair exadecim bool x9 true
1094             | xE ⇒ pair exadecim bool xA true
1095             | xF ⇒ pair exadecim bool xB true ]
1096        | xC ⇒
1097            match e2 with
1098             [ x0 ⇒ pair exadecim bool xD false
1099             | x1 ⇒ pair exadecim bool xE false
1100             | x2 ⇒ pair exadecim bool xF false
1101             | x3 ⇒ pair exadecim bool x0 true
1102             | x4 ⇒ pair exadecim bool x1 true
1103             | x5 ⇒ pair exadecim bool x2 true
1104             | x6 ⇒ pair exadecim bool x3 true
1105             | x7 ⇒ pair exadecim bool x4 true
1106             | x8 ⇒ pair exadecim bool x5 true
1107             | x9 ⇒ pair exadecim bool x6 true
1108             | xA ⇒ pair exadecim bool x7 true
1109             | xB ⇒ pair exadecim bool x8 true
1110             | xC ⇒ pair exadecim bool x9 true
1111             | xD ⇒ pair exadecim bool xA true
1112             | xE ⇒ pair exadecim bool xB true
1113             | xF ⇒ pair exadecim bool xC true ]
1114        | xD ⇒
1115            match e2 with
1116             [ x0 ⇒ pair exadecim bool xE false
1117             | x1 ⇒ pair exadecim bool xF false
1118             | x2 ⇒ pair exadecim bool x0 true
1119             | x3 ⇒ pair exadecim bool x1 true
1120             | x4 ⇒ pair exadecim bool x2 true
1121             | x5 ⇒ pair exadecim bool x3 true
1122             | x6 ⇒ pair exadecim bool x4 true
1123             | x7 ⇒ pair exadecim bool x5 true
1124             | x8 ⇒ pair exadecim bool x6 true
1125             | x9 ⇒ pair exadecim bool x7 true
1126             | xA ⇒ pair exadecim bool x8 true
1127             | xB ⇒ pair exadecim bool x9 true
1128             | xC ⇒ pair exadecim bool xA true
1129             | xD ⇒ pair exadecim bool xB true
1130             | xE ⇒ pair exadecim bool xC true
1131             | xF ⇒ pair exadecim bool xD true ]
1132        | xE ⇒
1133            match e2 with
1134             [ x0 ⇒ pair exadecim bool xF false
1135             | x1 ⇒ pair exadecim bool x0 true
1136             | x2 ⇒ pair exadecim bool x1 true
1137             | x3 ⇒ pair exadecim bool x2 true
1138             | x4 ⇒ pair exadecim bool x3 true
1139             | x5 ⇒ pair exadecim bool x4 true
1140             | x6 ⇒ pair exadecim bool x5 true
1141             | x7 ⇒ pair exadecim bool x6 true
1142             | x8 ⇒ pair exadecim bool x7 true
1143             | x9 ⇒ pair exadecim bool x8 true
1144             | xA ⇒ pair exadecim bool x9 true
1145             | xB ⇒ pair exadecim bool xA true
1146             | xC ⇒ pair exadecim bool xB true
1147             | xD ⇒ pair exadecim bool xC true
1148             | xE ⇒ pair exadecim bool xD true
1149             | xF ⇒ pair exadecim bool xE true ]
1150        | xF ⇒
1151            match e2 with
1152             [ x0 ⇒ pair exadecim bool x0 true
1153             | x1 ⇒ pair exadecim bool x1 true
1154             | x2 ⇒ pair exadecim bool x2 true
1155             | x3 ⇒ pair exadecim bool x3 true
1156             | x4 ⇒ pair exadecim bool x4 true
1157             | x5 ⇒ pair exadecim bool x5 true
1158             | x6 ⇒ pair exadecim bool x6 true
1159             | x7 ⇒ pair exadecim bool x7 true
1160             | x8 ⇒ pair exadecim bool x8 true
1161             | x9 ⇒ pair exadecim bool x9 true
1162             | xA ⇒ pair exadecim bool xA true
1163             | xB ⇒ pair exadecim bool xB true
1164             | xC ⇒ pair exadecim bool xC true
1165             | xD ⇒ pair exadecim bool xD true
1166             | xE ⇒ pair exadecim bool xE true
1167             | xF ⇒ pair exadecim bool xF true ]
1168        ]
1169    | false ⇒
1170       match e1 with
1171        [ x0 ⇒
1172            match e2 with
1173             [ x0 ⇒ pair exadecim bool x0 false
1174             | x1 ⇒ pair exadecim bool x1 false
1175             | x2 ⇒ pair exadecim bool x2 false
1176             | x3 ⇒ pair exadecim bool x3 false
1177             | x4 ⇒ pair exadecim bool x4 false
1178             | x5 ⇒ pair exadecim bool x5 false
1179             | x6 ⇒ pair exadecim bool x6 false
1180             | x7 ⇒ pair exadecim bool x7 false
1181             | x8 ⇒ pair exadecim bool x8 false
1182             | x9 ⇒ pair exadecim bool x9 false
1183             | xA ⇒ pair exadecim bool xA false
1184             | xB ⇒ pair exadecim bool xB false
1185             | xC ⇒ pair exadecim bool xC false
1186             | xD ⇒ pair exadecim bool xD false
1187             | xE ⇒ pair exadecim bool xE false
1188             | xF ⇒ pair exadecim bool xF false ]
1189        | x1 ⇒
1190            match e2 with
1191             [ x0 ⇒ pair exadecim bool x1 false
1192             | x1 ⇒ pair exadecim bool x2 false
1193             | x2 ⇒ pair exadecim bool x3 false
1194             | x3 ⇒ pair exadecim bool x4 false
1195             | x4 ⇒ pair exadecim bool x5 false
1196             | x5 ⇒ pair exadecim bool x6 false
1197             | x6 ⇒ pair exadecim bool x7 false
1198             | x7 ⇒ pair exadecim bool x8 false
1199             | x8 ⇒ pair exadecim bool x9 false
1200             | x9 ⇒ pair exadecim bool xA false
1201             | xA ⇒ pair exadecim bool xB false
1202             | xB ⇒ pair exadecim bool xC false
1203             | xC ⇒ pair exadecim bool xD false
1204             | xD ⇒ pair exadecim bool xE false
1205             | xE ⇒ pair exadecim bool xF false
1206             | xF ⇒ pair exadecim bool x0 true ]
1207        | x2 ⇒
1208            match e2 with
1209             [ x0 ⇒ pair exadecim bool x2 false
1210             | x1 ⇒ pair exadecim bool x3 false
1211             | x2 ⇒ pair exadecim bool x4 false
1212             | x3 ⇒ pair exadecim bool x5 false
1213             | x4 ⇒ pair exadecim bool x6 false
1214             | x5 ⇒ pair exadecim bool x7 false
1215             | x6 ⇒ pair exadecim bool x8 false
1216             | x7 ⇒ pair exadecim bool x9 false
1217             | x8 ⇒ pair exadecim bool xA false
1218             | x9 ⇒ pair exadecim bool xB false
1219             | xA ⇒ pair exadecim bool xC false
1220             | xB ⇒ pair exadecim bool xD false
1221             | xC ⇒ pair exadecim bool xE false
1222             | xD ⇒ pair exadecim bool xF false
1223             | xE ⇒ pair exadecim bool x0 true
1224             | xF ⇒ pair exadecim bool x1 true ]
1225        | x3 ⇒
1226            match e2 with
1227             [ x0 ⇒ pair exadecim bool x3 false
1228             | x1 ⇒ pair exadecim bool x4 false
1229             | x2 ⇒ pair exadecim bool x5 false
1230             | x3 ⇒ pair exadecim bool x6 false
1231             | x4 ⇒ pair exadecim bool x7 false
1232             | x5 ⇒ pair exadecim bool x8 false
1233             | x6 ⇒ pair exadecim bool x9 false
1234             | x7 ⇒ pair exadecim bool xA false
1235             | x8 ⇒ pair exadecim bool xB false
1236             | x9 ⇒ pair exadecim bool xC false
1237             | xA ⇒ pair exadecim bool xD false
1238             | xB ⇒ pair exadecim bool xE false
1239             | xC ⇒ pair exadecim bool xF false
1240             | xD ⇒ pair exadecim bool x0 true
1241             | xE ⇒ pair exadecim bool x1 true
1242             | xF ⇒ pair exadecim bool x2 true ]
1243        | x4 ⇒
1244            match e2 with
1245             [ x0 ⇒ pair exadecim bool x4 false
1246             | x1 ⇒ pair exadecim bool x5 false
1247             | x2 ⇒ pair exadecim bool x6 false
1248             | x3 ⇒ pair exadecim bool x7 false
1249             | x4 ⇒ pair exadecim bool x8 false
1250             | x5 ⇒ pair exadecim bool x9 false
1251             | x6 ⇒ pair exadecim bool xA false
1252             | x7 ⇒ pair exadecim bool xB false
1253             | x8 ⇒ pair exadecim bool xC false
1254             | x9 ⇒ pair exadecim bool xD false
1255             | xA ⇒ pair exadecim bool xE false
1256             | xB ⇒ pair exadecim bool xF false
1257             | xC ⇒ pair exadecim bool x0 true
1258             | xD ⇒ pair exadecim bool x1 true
1259             | xE ⇒ pair exadecim bool x2 true
1260             | xF ⇒ pair exadecim bool x3 true ]
1261        | x5 ⇒
1262            match e2 with
1263             [ x0 ⇒ pair exadecim bool x5 false
1264             | x1 ⇒ pair exadecim bool x6 false
1265             | x2 ⇒ pair exadecim bool x7 false
1266             | x3 ⇒ pair exadecim bool x8 false
1267             | x4 ⇒ pair exadecim bool x9 false
1268             | x5 ⇒ pair exadecim bool xA false
1269             | x6 ⇒ pair exadecim bool xB false
1270             | x7 ⇒ pair exadecim bool xC false
1271             | x8 ⇒ pair exadecim bool xD false
1272             | x9 ⇒ pair exadecim bool xE false
1273             | xA ⇒ pair exadecim bool xF false
1274             | xB ⇒ pair exadecim bool x0 true
1275             | xC ⇒ pair exadecim bool x1 true
1276             | xD ⇒ pair exadecim bool x2 true
1277             | xE ⇒ pair exadecim bool x3 true
1278             | xF ⇒ pair exadecim bool x4 true ]
1279        | x6 ⇒
1280            match e2 with
1281             [ x0 ⇒ pair exadecim bool x6 false
1282             | x1 ⇒ pair exadecim bool x7 false
1283             | x2 ⇒ pair exadecim bool x8 false
1284             | x3 ⇒ pair exadecim bool x9 false
1285             | x4 ⇒ pair exadecim bool xA false
1286             | x5 ⇒ pair exadecim bool xB false
1287             | x6 ⇒ pair exadecim bool xC false
1288             | x7 ⇒ pair exadecim bool xD false
1289             | x8 ⇒ pair exadecim bool xE false
1290             | x9 ⇒ pair exadecim bool xF false
1291             | xA ⇒ pair exadecim bool x0 true
1292             | xB ⇒ pair exadecim bool x1 true
1293             | xC ⇒ pair exadecim bool x2 true
1294             | xD ⇒ pair exadecim bool x3 true
1295             | xE ⇒ pair exadecim bool x4 true
1296             | xF ⇒ pair exadecim bool x5 true ]
1297        | x7 ⇒
1298            match e2 with
1299             [ x0 ⇒ pair exadecim bool x7 false
1300             | x1 ⇒ pair exadecim bool x8 false
1301             | x2 ⇒ pair exadecim bool x9 false
1302             | x3 ⇒ pair exadecim bool xA false
1303             | x4 ⇒ pair exadecim bool xB false
1304             | x5 ⇒ pair exadecim bool xC false
1305             | x6 ⇒ pair exadecim bool xD false
1306             | x7 ⇒ pair exadecim bool xE false
1307             | x8 ⇒ pair exadecim bool xF false
1308             | x9 ⇒ pair exadecim bool x0 true
1309             | xA ⇒ pair exadecim bool x1 true
1310             | xB ⇒ pair exadecim bool x2 true
1311             | xC ⇒ pair exadecim bool x3 true
1312             | xD ⇒ pair exadecim bool x4 true
1313             | xE ⇒ pair exadecim bool x5 true
1314             | xF ⇒ pair exadecim bool x6 true ]
1315        | x8 ⇒
1316            match e2 with
1317             [ x0 ⇒ pair exadecim bool x8 false
1318             | x1 ⇒ pair exadecim bool x9 false
1319             | x2 ⇒ pair exadecim bool xA false
1320             | x3 ⇒ pair exadecim bool xB false
1321             | x4 ⇒ pair exadecim bool xC false
1322             | x5 ⇒ pair exadecim bool xD false
1323             | x6 ⇒ pair exadecim bool xE false
1324             | x7 ⇒ pair exadecim bool xF false
1325             | x8 ⇒ pair exadecim bool x0 true
1326             | x9 ⇒ pair exadecim bool x1 true
1327             | xA ⇒ pair exadecim bool x2 true
1328             | xB ⇒ pair exadecim bool x3 true
1329             | xC ⇒ pair exadecim bool x4 true
1330             | xD ⇒ pair exadecim bool x5 true
1331             | xE ⇒ pair exadecim bool x6 true
1332             | xF ⇒ pair exadecim bool x7 true ]
1333        | x9 ⇒
1334            match e2 with
1335             [ x0 ⇒ pair exadecim bool x9 false
1336             | x1 ⇒ pair exadecim bool xA false
1337             | x2 ⇒ pair exadecim bool xB false
1338             | x3 ⇒ pair exadecim bool xC false
1339             | x4 ⇒ pair exadecim bool xD false
1340             | x5 ⇒ pair exadecim bool xE false
1341             | x6 ⇒ pair exadecim bool xF false
1342             | x7 ⇒ pair exadecim bool x0 true
1343             | x8 ⇒ pair exadecim bool x1 true
1344             | x9 ⇒ pair exadecim bool x2 true
1345             | xA ⇒ pair exadecim bool x3 true
1346             | xB ⇒ pair exadecim bool x4 true
1347             | xC ⇒ pair exadecim bool x5 true
1348             | xD ⇒ pair exadecim bool x6 true
1349             | xE ⇒ pair exadecim bool x7 true
1350             | xF ⇒ pair exadecim bool x8 true ]
1351        | xA ⇒
1352            match e2 with
1353             [ x0 ⇒ pair exadecim bool xA false
1354             | x1 ⇒ pair exadecim bool xB false
1355             | x2 ⇒ pair exadecim bool xC false
1356             | x3 ⇒ pair exadecim bool xD false
1357             | x4 ⇒ pair exadecim bool xE false
1358             | x5 ⇒ pair exadecim bool xF false
1359             | x6 ⇒ pair exadecim bool x0 true
1360             | x7 ⇒ pair exadecim bool x1 true
1361             | x8 ⇒ pair exadecim bool x2 true
1362             | x9 ⇒ pair exadecim bool x3 true
1363             | xA ⇒ pair exadecim bool x4 true
1364             | xB ⇒ pair exadecim bool x5 true
1365             | xC ⇒ pair exadecim bool x6 true
1366             | xD ⇒ pair exadecim bool x7 true
1367             | xE ⇒ pair exadecim bool x8 true
1368             | xF ⇒ pair exadecim bool x9 true ]
1369        | xB ⇒
1370            match e2 with
1371             [ x0 ⇒ pair exadecim bool xB false
1372             | x1 ⇒ pair exadecim bool xC false
1373             | x2 ⇒ pair exadecim bool xD false
1374             | x3 ⇒ pair exadecim bool xE false
1375             | x4 ⇒ pair exadecim bool xF false
1376             | x5 ⇒ pair exadecim bool x0 true
1377             | x6 ⇒ pair exadecim bool x1 true
1378             | x7 ⇒ pair exadecim bool x2 true
1379             | x8 ⇒ pair exadecim bool x3 true
1380             | x9 ⇒ pair exadecim bool x4 true
1381             | xA ⇒ pair exadecim bool x5 true
1382             | xB ⇒ pair exadecim bool x6 true
1383             | xC ⇒ pair exadecim bool x7 true
1384             | xD ⇒ pair exadecim bool x8 true
1385             | xE ⇒ pair exadecim bool x9 true
1386             | xF ⇒ pair exadecim bool xA true ]
1387        | xC ⇒
1388            match e2 with
1389             [ x0 ⇒ pair exadecim bool xC false
1390             | x1 ⇒ pair exadecim bool xD false
1391             | x2 ⇒ pair exadecim bool xE false
1392             | x3 ⇒ pair exadecim bool xF false
1393             | x4 ⇒ pair exadecim bool x0 true
1394             | x5 ⇒ pair exadecim bool x1 true
1395             | x6 ⇒ pair exadecim bool x2 true
1396             | x7 ⇒ pair exadecim bool x3 true
1397             | x8 ⇒ pair exadecim bool x4 true
1398             | x9 ⇒ pair exadecim bool x5 true
1399             | xA ⇒ pair exadecim bool x6 true
1400             | xB ⇒ pair exadecim bool x7 true
1401             | xC ⇒ pair exadecim bool x8 true
1402             | xD ⇒ pair exadecim bool x9 true
1403             | xE ⇒ pair exadecim bool xA true
1404             | xF ⇒ pair exadecim bool xB true ]
1405        | xD ⇒
1406            match e2 with
1407             [ x0 ⇒ pair exadecim bool xD false
1408             | x1 ⇒ pair exadecim bool xE false
1409             | x2 ⇒ pair exadecim bool xF false
1410             | x3 ⇒ pair exadecim bool x0 true
1411             | x4 ⇒ pair exadecim bool x1 true
1412             | x5 ⇒ pair exadecim bool x2 true
1413             | x6 ⇒ pair exadecim bool x3 true
1414             | x7 ⇒ pair exadecim bool x4 true
1415             | x8 ⇒ pair exadecim bool x5 true
1416             | x9 ⇒ pair exadecim bool x6 true
1417             | xA ⇒ pair exadecim bool x7 true
1418             | xB ⇒ pair exadecim bool x8 true
1419             | xC ⇒ pair exadecim bool x9 true
1420             | xD ⇒ pair exadecim bool xA true
1421             | xE ⇒ pair exadecim bool xB true
1422             | xF ⇒ pair exadecim bool xC true ]
1423        | xE ⇒
1424            match e2 with
1425             [ x0 ⇒ pair exadecim bool xE false
1426             | x1 ⇒ pair exadecim bool xF false
1427             | x2 ⇒ pair exadecim bool x0 true
1428             | x3 ⇒ pair exadecim bool x1 true
1429             | x4 ⇒ pair exadecim bool x2 true
1430             | x5 ⇒ pair exadecim bool x3 true
1431             | x6 ⇒ pair exadecim bool x4 true
1432             | x7 ⇒ pair exadecim bool x5 true
1433             | x8 ⇒ pair exadecim bool x6 true
1434             | x9 ⇒ pair exadecim bool x7 true
1435             | xA ⇒ pair exadecim bool x8 true
1436             | xB ⇒ pair exadecim bool x9 true
1437             | xC ⇒ pair exadecim bool xA true
1438             | xD ⇒ pair exadecim bool xB true
1439             | xE ⇒ pair exadecim bool xC true
1440             | xF ⇒ pair exadecim bool xD true ]
1441        | xF ⇒
1442            match e2 with
1443             [ x0 ⇒ pair exadecim bool xF false
1444             | x1 ⇒ pair exadecim bool x0 true
1445             | x2 ⇒ pair exadecim bool x1 true
1446             | x3 ⇒ pair exadecim bool x2 true
1447             | x4 ⇒ pair exadecim bool x3 true
1448             | x5 ⇒ pair exadecim bool x4 true
1449             | x6 ⇒ pair exadecim bool x5 true
1450             | x7 ⇒ pair exadecim bool x6 true
1451             | x8 ⇒ pair exadecim bool x7 true
1452             | x9 ⇒ pair exadecim bool x8 true
1453             | xA ⇒ pair exadecim bool x9 true
1454             | xB ⇒ pair exadecim bool xA true
1455             | xC ⇒ pair exadecim bool xB true
1456             | xD ⇒ pair exadecim bool xC true
1457             | xE ⇒ pair exadecim bool xD true
1458             | xF ⇒ pair exadecim bool xE true ]
1459        ]
1460    ].
1461
1462 (* operatore somma senza carry *)
1463 ndefinition plus_exnc ≝
1464 λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
1465
1466 (* operatore carry della somma *)
1467 ndefinition plus_exc ≝
1468 λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
1469
1470 (* operatore Most Significant Bit *)
1471 ndefinition MSB_ex ≝
1472 λe:exadecim.match e with
1473  [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1474  | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1475  | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
1476  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ].
1477
1478 (* esadecimali → naturali *)
1479 ndefinition nat_of_exadecim : exadecim → nat ≝
1480 λe:exadecim.
1481  match e with
1482   [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2  | x3 ⇒ 3  | x4 ⇒ 4  | x5 ⇒ 5  | x6 ⇒ 6  | x7 ⇒ 7
1483   | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
1484
1485 (* operatore predecessore *)
1486 ndefinition pred_ex ≝
1487 λe:exadecim.
1488  match e with
1489   [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1490   | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1491
1492 (* operatore successore *)
1493 ndefinition succ_ex ≝
1494 λe:exadecim.
1495  match e with
1496   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1497   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1498
1499 (* operatore neg/complemento a 2 *)
1500 ndefinition compl_ex ≝
1501 λe:exadecim.match e with
1502  [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1503  | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1504  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1505  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1506
1507 (* iteratore sugli esadecimali *)
1508 ndefinition forall_exadecim ≝ λP.
1509  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1510  P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.