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 data+carry → data+carry *)
 875 ndefinition plus_ex_dc_dc ≝
 876 λe1,e2:exadecim.λc:bool.
 877  match c with
 878   [ true ⇒ match e1 with
 879    [ x0 ⇒ match e2 with
 880     [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
 881     | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
 882     | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
 883     | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ]
 884    | x1 ⇒ match e2 with
 885     [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
 886     | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
 887     | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
 888     | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true  | xF ⇒ pair ?? x1 true ]
 889    | x2 ⇒ match e2 with
 890     [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
 891     | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
 892     | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
 893     | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true  | xE ⇒ pair ?? x1 true  | xF ⇒ pair ?? x2 true ]
 894    | x3 ⇒ match e2 with
 895     [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
 896     | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
 897     | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
 898     | xC ⇒ pair ?? x0 true  | xD ⇒ pair ?? x1 true  | xE ⇒ pair ?? x2 true  | xF ⇒ pair ?? x3 true ]
 899    | x4 ⇒ match e2 with
 900     [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
 901     | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
 902     | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
 903     | xC ⇒ pair ?? x1 true  | xD ⇒ pair ?? x2 true  | xE ⇒ pair ?? x3 true  | xF ⇒ pair ?? x4 true ]
 904    | x5 ⇒ match e2 with
 905     [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
 906     | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
 907     | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true  | xB ⇒ pair ?? x1 true
 908     | xC ⇒ pair ?? x2 true  | xD ⇒ pair ?? x3 true  | xE ⇒ pair ?? x4 true  | xF ⇒ pair ?? x5 true ]
 909    | x6 ⇒ match e2 with
 910     [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
 911     | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
 912     | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true  | xA ⇒ pair ?? x1 true  | xB ⇒ pair ?? x2 true
 913     | xC ⇒ pair ?? x3 true  | xD ⇒ pair ?? x4 true  | xE ⇒ pair ?? x5 true  | xF ⇒ pair ?? x6 true ]
 914    | x7 ⇒ match e2 with
 915     [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
 916     | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
 917     | x8 ⇒ pair ?? x0 true  | x9 ⇒ pair ?? x1 true  | xA ⇒ pair ?? x2 true  | xB ⇒ pair ?? x3 true
 918     | xC ⇒ pair ?? x4 true  | xD ⇒ pair ?? x5 true  | xE ⇒ pair ?? x6 true  | xF ⇒ pair ?? x7 true ]
 919    | x8 ⇒ match e2 with
 920     [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
 921     | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
 922     | x8 ⇒ pair ?? x1 true  | x9 ⇒ pair ?? x2 true  | xA ⇒ pair ?? x3 true  | xB ⇒ pair ?? x4 true
 923     | xC ⇒ pair ?? x5 true  | xD ⇒ pair ?? x6 true  | xE ⇒ pair ?? x7 true  | xF ⇒ pair ?? x8 true ]
 924    | x9 ⇒ match e2 with
 925     [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
 926     | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true  | x7 ⇒ pair ?? x1 true
 927     | x8 ⇒ pair ?? x2 true  | x9 ⇒ pair ?? x3 true  | xA ⇒ pair ?? x4 true  | xB ⇒ pair ?? x5 true
 928     | xC ⇒ pair ?? x6 true  | xD ⇒ pair ?? x7 true  | xE ⇒ pair ?? x8 true  | xF ⇒ pair ?? x9 true ]
 929    | xA ⇒ match e2 with
 930     [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
 931     | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true  | x6 ⇒ pair ?? x1 true  | x7 ⇒ pair ?? x2 true
 932     | x8 ⇒ pair ?? x3 true  | x9 ⇒ pair ?? x4 true  | xA ⇒ pair ?? x5 true  | xB ⇒ pair ?? x6 true
 933     | xC ⇒ pair ?? x7 true  | xD ⇒ pair ?? x8 true  | xE ⇒ pair ?? x9 true  | xF ⇒ pair ?? xA true ]
 934    | xB ⇒ match e2 with
 935     [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
 936     | x4 ⇒ pair ?? x0 true  | x5 ⇒ pair ?? x1 true  | x6 ⇒ pair ?? x2 true  | x7 ⇒ pair ?? x3 true
 937     | x8 ⇒ pair ?? x4 true  | x9 ⇒ pair ?? x5 true  | xA ⇒ pair ?? x6 true  | xB ⇒ pair ?? x7 true
 938     | xC ⇒ pair ?? x8 true  | xD ⇒ pair ?? x9 true  | xE ⇒ pair ?? xA true  | xF ⇒ pair ?? xB true ]
 939    | xC ⇒ match e2 with
 940     [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
 941     | x4 ⇒ pair ?? x1 true  | x5 ⇒ pair ?? x2 true  | x6 ⇒ pair ?? x3 true  | x7 ⇒ pair ?? x4 true
 942     | x8 ⇒ pair ?? x5 true  | x9 ⇒ pair ?? x6 true  | xA ⇒ pair ?? x7 true  | xB ⇒ pair ?? x8 true
 943     | xC ⇒ pair ?? x9 true  | xD ⇒ pair ?? xA true  | xE ⇒ pair ?? xB true  | xF ⇒ pair ?? xC true ]
 944    | xD ⇒ match e2 with
 945     [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true  | x3 ⇒ pair ?? x1 true
 946     | x4 ⇒ pair ?? x2 true  | x5 ⇒ pair ?? x3 true  | x6 ⇒ pair ?? x4 true  | x7 ⇒ pair ?? x5 true
 947     | x8 ⇒ pair ?? x6 true  | x9 ⇒ pair ?? x7 true  | xA ⇒ pair ?? x8 true  | xB ⇒ pair ?? x9 true
 948     | xC ⇒ pair ?? xA true  | xD ⇒ pair ?? xB true  | xE ⇒ pair ?? xC true  | xF ⇒ pair ?? xD true ]
 949    | xE ⇒ match e2 with
 950     [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true  | x2 ⇒ pair ?? x1 true  | x3 ⇒ pair ?? x2 true
 951     | x4 ⇒ pair ?? x3 true  | x5 ⇒ pair ?? x4 true  | x6 ⇒ pair ?? x5 true  | x7 ⇒ pair ?? x6 true
 952     | x8 ⇒ pair ?? x7 true  | x9 ⇒ pair ?? x8 true  | xA ⇒ pair ?? x9 true  | xB ⇒ pair ?? xA true
 953     | xC ⇒ pair ?? xB true  | xD ⇒ pair ?? xC true  | xE ⇒ pair ?? xD true  | xF ⇒ pair ?? xE true ]
 954    | xF ⇒ match e2 with
 955     [ x0 ⇒ pair ?? x0 true  | x1 ⇒ pair ?? x1 true  | x2 ⇒ pair ?? x2 true  | x3 ⇒ pair ?? x3 true
 956     | x4 ⇒ pair ?? x4 true  | x5 ⇒ pair ?? x5 true  | x6 ⇒ pair ?? x6 true  | x7 ⇒ pair ?? x7 true
 957     | x8 ⇒ pair ?? x8 true  | x9 ⇒ pair ?? x9 true  | xA ⇒ pair ?? xA true  | xB ⇒ pair ?? xB true
 958     | xC ⇒ pair ?? xC true  | xD ⇒ pair ?? xD true  | xE ⇒ pair ?? xE true  | xF ⇒ pair ?? xF true ]
 959    ]
 960   | false ⇒ match e1 with
 961    [ x0 ⇒ match e2 with
 962     [ x0 ⇒ pair ?? x0 false | x1 ⇒ pair ?? x1 false | x2 ⇒ pair ?? x2 false | x3 ⇒ pair ?? x3 false
 963     | x4 ⇒ pair ?? x4 false | x5 ⇒ pair ?? x5 false | x6 ⇒ pair ?? x6 false | x7 ⇒ pair ?? x7 false
 964     | x8 ⇒ pair ?? x8 false | x9 ⇒ pair ?? x9 false | xA ⇒ pair ?? xA false | xB ⇒ pair ?? xB false
 965     | xC ⇒ pair ?? xC false | xD ⇒ pair ?? xD false | xE ⇒ pair ?? xE false | xF ⇒ pair ?? xF false ]
 966    | x1 ⇒ match e2 with
 967     [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
 968     | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
 969     | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
 970     | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ]
 971    | x2 ⇒ match e2 with
 972     [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
 973     | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
 974     | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
 975     | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true  | xF ⇒ pair ?? x1 true ]
 976    | x3 ⇒ match e2 with
 977     [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
 978     | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
 979     | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
 980     | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true  | xE ⇒ pair ?? x1 true  | xF ⇒ pair ?? x2 true ]
 981    | x4 ⇒ match e2 with
 982     [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
 983     | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
 984     | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
 985     | xC ⇒ pair ?? x0 true  | xD ⇒ pair ?? x1 true  | xE ⇒ pair ?? x2 true  | xF ⇒ pair ?? x3 true ]
 986    | x5 ⇒ match e2 with
 987     [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
 988     | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
 989     | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
 990     | xC ⇒ pair ?? x1 true  | xD ⇒ pair ?? x2 true  | xE ⇒ pair ?? x3 true  | xF ⇒ pair ?? x4 true ]
 991    | x6 ⇒ match e2 with
 992     [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
 993     | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
 994     | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true  | xB ⇒ pair ?? x1 true
 995     | xC ⇒ pair ?? x2 true  | xD ⇒ pair ?? x3 true  | xE ⇒ pair ?? x4 true  | xF ⇒ pair ?? x5 true ]
 996    | x7 ⇒ match e2 with
 997     [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
 998     | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
 999     | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true  | xA ⇒ pair ?? x1 true  | xB ⇒ pair ?? x2 true
1000     | xC ⇒ pair ?? x3 true  | xD ⇒ pair ?? x4 true  | xE ⇒ pair ?? x5 true  | xF ⇒ pair ?? x6 true ]
1001    | x8 ⇒ match e2 with
1002     [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
1003     | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
1004     | x8 ⇒ pair ?? x0 true  | x9 ⇒ pair ?? x1 true  | xA ⇒ pair ?? x2 true  | xB ⇒ pair ?? x3 true
1005     | xC ⇒ pair ?? x4 true  | xD ⇒ pair ?? x5 true  | xE ⇒ pair ?? x6 true  | xF ⇒ pair ?? x7 true ]
1006    | x9 ⇒ match e2 with
1007     [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
1008     | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
1009     | x8 ⇒ pair ?? x1 true  | x9 ⇒ pair ?? x2 true  | xA ⇒ pair ?? x3 true  | xB ⇒ pair ?? x4 true
1010     | xC ⇒ pair ?? x5 true  | xD ⇒ pair ?? x6 true  | xE ⇒ pair ?? x7 true  | xF ⇒ pair ?? x8 true ]
1011    | xA ⇒ match e2 with
1012     [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
1013     | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true  | x7 ⇒ pair ?? x1 true
1014     | x8 ⇒ pair ?? x2 true  | x9 ⇒ pair ?? x3 true  | xA ⇒ pair ?? x4 true  | xB ⇒ pair ?? x5 true
1015     | xC ⇒ pair ?? x6 true  | xD ⇒ pair ?? x7 true  | xE ⇒ pair ?? x8 true  | xF ⇒ pair ?? x9 true ]
1016    | xB ⇒ match e2 with
1017     [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
1018     | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true  | x6 ⇒ pair ?? x1 true  | x7 ⇒ pair ?? x2 true
1019     | x8 ⇒ pair ?? x3 true  | x9 ⇒ pair ?? x4 true  | xA ⇒ pair ?? x5 true  | xB ⇒ pair ?? x6 true
1020     | xC ⇒ pair ?? x7 true  | xD ⇒ pair ?? x8 true  | xE ⇒ pair ?? x9 true  | xF ⇒ pair ?? xA true ]
1021    | xC ⇒ match e2 with
1022     [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
1023     | x4 ⇒ pair ?? x0 true  | x5 ⇒ pair ?? x1 true  | x6 ⇒ pair ?? x2 true  | x7 ⇒ pair ?? x3 true
1024     | x8 ⇒ pair ?? x4 true  | x9 ⇒ pair ?? x5 true  | xA ⇒ pair ?? x6 true  | xB ⇒ pair ?? x7 true
1025     | xC ⇒ pair ?? x8 true  | xD ⇒ pair ?? x9 true  | xE ⇒ pair ?? xA true  | xF ⇒ pair ?? xB true ]
1026    | xD ⇒ match e2 with
1027     [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
1028     | x4 ⇒ pair ?? x1 true  | x5 ⇒ pair ?? x2 true  | x6 ⇒ pair ?? x3 true  | x7 ⇒ pair ?? x4 true
1029     | x8 ⇒ pair ?? x5 true  | x9 ⇒ pair ?? x6 true  | xA ⇒ pair ?? x7 true  | xB ⇒ pair ?? x8 true
1030     | xC ⇒ pair ?? x9 true  | xD ⇒ pair ?? xA true  | xE ⇒ pair ?? xB true  | xF ⇒ pair ?? xC true ]
1031    | xE ⇒ match e2 with
1032     [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true  | x3 ⇒ pair ?? x1 true
1033     | x4 ⇒ pair ?? x2 true  | x5 ⇒ pair ?? x3 true  | x6 ⇒ pair ?? x4 true  | x7 ⇒ pair ?? x5 true
1034     | x8 ⇒ pair ?? x6 true  | x9 ⇒ pair ?? x7 true  | xA ⇒ pair ?? x8 true  | xB ⇒ pair ?? x9 true
1035     | xC ⇒ pair ?? xA true  | xD ⇒ pair ?? xB true  | xE ⇒ pair ?? xC true  | xF ⇒ pair ?? xD true ]
1036    | xF ⇒ match e2 with
1037     [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true  | x2 ⇒ pair ?? x1 true  | x3 ⇒ pair ?? x2 true
1038     | x4 ⇒ pair ?? x3 true  | x5 ⇒ pair ?? x4 true  | x6 ⇒ pair ?? x5 true  | x7 ⇒ pair ?? x6 true
1039     | x8 ⇒ pair ?? x7 true  | x9 ⇒ pair ?? x8 true  | xA ⇒ pair ?? x9 true  | xB ⇒ pair ?? xA true
1040     | xC ⇒ pair ?? xB true  | xD ⇒ pair ?? xC true  | xE ⇒ pair ?? xD true  | xF ⇒ pair ?? xE true ]
1041    ]].
1042
1043 (* operatore somma con data → data+carry *)
1044 ndefinition plus_ex_d_dc ≝
1045 λe1,e2:exadecim.
1046  match e1 with
1047   [ x0 ⇒ match e2 with
1048    [ x0 ⇒ pair ?? x0 false | x1 ⇒ pair ?? x1 false | x2 ⇒ pair ?? x2 false | x3 ⇒ pair ?? x3 false
1049    | x4 ⇒ pair ?? x4 false | x5 ⇒ pair ?? x5 false | x6 ⇒ pair ?? x6 false | x7 ⇒ pair ?? x7 false
1050    | x8 ⇒ pair ?? x8 false | x9 ⇒ pair ?? x9 false | xA ⇒ pair ?? xA false | xB ⇒ pair ?? xB false
1051    | xC ⇒ pair ?? xC false | xD ⇒ pair ?? xD false | xE ⇒ pair ?? xE false | xF ⇒ pair ?? xF false ]
1052   | x1 ⇒ match e2 with
1053    [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
1054    | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
1055    | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
1056    | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ]
1057   | x2 ⇒ match e2 with
1058    [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
1059    | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
1060    | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
1061    | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true  | xF ⇒ pair ?? x1 true ]
1062   | x3 ⇒ match e2 with
1063    [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
1064    | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
1065    | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
1066    | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true  | xE ⇒ pair ?? x1 true  | xF ⇒ pair ?? x2 true ]
1067   | x4 ⇒ match e2 with
1068    [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
1069    | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
1070    | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
1071    | xC ⇒ pair ?? x0 true  | xD ⇒ pair ?? x1 true  | xE ⇒ pair ?? x2 true  | xF ⇒ pair ?? x3 true ]
1072   | x5 ⇒ match e2 with
1073    [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
1074    | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
1075    | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
1076    | xC ⇒ pair ?? x1 true  | xD ⇒ pair ?? x2 true  | xE ⇒ pair ?? x3 true  | xF ⇒ pair ?? x4 true ]
1077   | x6 ⇒ match e2 with
1078    [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
1079    | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
1080    | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true  | xB ⇒ pair ?? x1 true
1081    | xC ⇒ pair ?? x2 true  | xD ⇒ pair ?? x3 true  | xE ⇒ pair ?? x4 true  | xF ⇒ pair ?? x5 true ]
1082   | x7 ⇒ match e2 with
1083    [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
1084    | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
1085    | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true  | xA ⇒ pair ?? x1 true  | xB ⇒ pair ?? x2 true
1086    | xC ⇒ pair ?? x3 true  | xD ⇒ pair ?? x4 true  | xE ⇒ pair ?? x5 true  | xF ⇒ pair ?? x6 true ]
1087   | x8 ⇒ match e2 with
1088    [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
1089    | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
1090    | x8 ⇒ pair ?? x0 true  | x9 ⇒ pair ?? x1 true  | xA ⇒ pair ?? x2 true  | xB ⇒ pair ?? x3 true
1091    | xC ⇒ pair ?? x4 true  | xD ⇒ pair ?? x5 true  | xE ⇒ pair ?? x6 true  | xF ⇒ pair ?? x7 true ]
1092   | x9 ⇒ match e2 with
1093    [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
1094    | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
1095    | x8 ⇒ pair ?? x1 true  | x9 ⇒ pair ?? x2 true  | xA ⇒ pair ?? x3 true  | xB ⇒ pair ?? x4 true
1096    | xC ⇒ pair ?? x5 true  | xD ⇒ pair ?? x6 true  | xE ⇒ pair ?? x7 true  | xF ⇒ pair ?? x8 true ]
1097   | xA ⇒ match e2 with
1098    [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
1099    | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true  | x7 ⇒ pair ?? x1 true
1100    | x8 ⇒ pair ?? x2 true  | x9 ⇒ pair ?? x3 true  | xA ⇒ pair ?? x4 true  | xB ⇒ pair ?? x5 true
1101    | xC ⇒ pair ?? x6 true  | xD ⇒ pair ?? x7 true  | xE ⇒ pair ?? x8 true  | xF ⇒ pair ?? x9 true ]
1102   | xB ⇒ match e2 with
1103    [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
1104    | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true  | x6 ⇒ pair ?? x1 true  | x7 ⇒ pair ?? x2 true
1105    | x8 ⇒ pair ?? x3 true  | x9 ⇒ pair ?? x4 true  | xA ⇒ pair ?? x5 true  | xB ⇒ pair ?? x6 true
1106    | xC ⇒ pair ?? x7 true  | xD ⇒ pair ?? x8 true  | xE ⇒ pair ?? x9 true  | xF ⇒ pair ?? xA true ]
1107   | xC ⇒ match e2 with
1108    [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
1109    | x4 ⇒ pair ?? x0 true  | x5 ⇒ pair ?? x1 true  | x6 ⇒ pair ?? x2 true  | x7 ⇒ pair ?? x3 true
1110    | x8 ⇒ pair ?? x4 true  | x9 ⇒ pair ?? x5 true  | xA ⇒ pair ?? x6 true  | xB ⇒ pair ?? x7 true
1111    | xC ⇒ pair ?? x8 true  | xD ⇒ pair ?? x9 true  | xE ⇒ pair ?? xA true  | xF ⇒ pair ?? xB true ]
1112   | xD ⇒ match e2 with
1113    [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
1114    | x4 ⇒ pair ?? x1 true  | x5 ⇒ pair ?? x2 true  | x6 ⇒ pair ?? x3 true  | x7 ⇒ pair ?? x4 true
1115    | x8 ⇒ pair ?? x5 true  | x9 ⇒ pair ?? x6 true  | xA ⇒ pair ?? x7 true  | xB ⇒ pair ?? x8 true
1116    | xC ⇒ pair ?? x9 true  | xD ⇒ pair ?? xA true  | xE ⇒ pair ?? xB true  | xF ⇒ pair ?? xC true ]
1117   | xE ⇒ match e2 with
1118    [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true  | x3 ⇒ pair ?? x1 true
1119    | x4 ⇒ pair ?? x2 true  | x5 ⇒ pair ?? x3 true  | x6 ⇒ pair ?? x4 true  | x7 ⇒ pair ?? x5 true
1120    | x8 ⇒ pair ?? x6 true  | x9 ⇒ pair ?? x7 true  | xA ⇒ pair ?? x8 true  | xB ⇒ pair ?? x9 true
1121    | xC ⇒ pair ?? xA true  | xD ⇒ pair ?? xB true  | xE ⇒ pair ?? xC true  | xF ⇒ pair ?? xD true ]
1122   | xF ⇒ match e2 with
1123    [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true  | x2 ⇒ pair ?? x1 true  | x3 ⇒ pair ?? x2 true
1124    | x4 ⇒ pair ?? x3 true  | x5 ⇒ pair ?? x4 true  | x6 ⇒ pair ?? x5 true  | x7 ⇒ pair ?? x6 true
1125    | x8 ⇒ pair ?? x7 true  | x9 ⇒ pair ?? x8 true  | xA ⇒ pair ?? x9 true  | xB ⇒ pair ?? xA true
1126    | xC ⇒ pair ?? xB true  | xD ⇒ pair ?? xC true  | xE ⇒ pair ?? xD true  | xF ⇒ pair ?? xE true ]
1127   ].
1128
1129 (* operatore somma con data+carry → data *)
1130 ndefinition plus_ex_dc_d ≝
1131 λe1,e2:exadecim.λc:bool.
1132  match c with
1133   [ true ⇒ match e1 with
1134    [ x0 ⇒ match e2 with
1135     [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1136     | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1137    | x1 ⇒ match e2 with
1138     [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1139     | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1140    | x2 ⇒ match e2 with
1141     [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1142     | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1143    | x3 ⇒ match e2 with
1144     [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1145     | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1146    | x4 ⇒ match e2 with
1147     [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1148     | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1149    | x5 ⇒ match e2 with
1150     [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1151     | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1152    | x6 ⇒ match e2 with
1153     [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1154     | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1155    | x7 ⇒ match e2 with
1156     [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1157     | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1158    | x8 ⇒ match e2 with
1159     [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1160     | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1161    | x9 ⇒ match e2 with
1162     [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1163     | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1164    | xA ⇒ match e2 with
1165     [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1166     | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1167    | xB ⇒ match e2 with
1168     [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1169     | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1170    | xC ⇒ match e2 with
1171      [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1172     | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1173    | xD ⇒ match e2 with
1174     [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1175     | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1176    | xE ⇒ match e2 with
1177     [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1178     | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1179    | xF ⇒ match e2 with
1180     [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1181     | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1182    ]
1183   | false ⇒ match e1 with
1184    [ x0 ⇒ match e2 with
1185     [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1186     | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1187    | x1 ⇒ match e2 with
1188     [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1189     | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1190    | x2 ⇒ match e2 with
1191     [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1192     | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1193    | x3 ⇒ match e2 with
1194     [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1195     | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1196    | x4 ⇒ match e2 with
1197     [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1198     | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1199    | x5 ⇒ match e2 with
1200     [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1201     | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1202    | x6 ⇒ match e2 with
1203     [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1204     | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1205    | x7 ⇒ match e2 with
1206     [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1207     | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1208    | x8 ⇒ match e2 with
1209     [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1210     | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1211    | x9 ⇒ match e2 with
1212     [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1213     | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1214    | xA ⇒ match e2 with
1215     [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1216     | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1217    | xB ⇒ match e2 with
1218     [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1219     | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1220    | xC ⇒ match e2 with
1221     [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1222     | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1223    | xD ⇒ match e2 with
1224      [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1225     | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1226    | xE ⇒ match e2 with
1227     [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1228     | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1229    | xF ⇒ match e2 with
1230     [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1231     | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1232    ]].
1233
1234 (* operatore somma con data → data *)
1235 ndefinition plus_ex_d_d ≝
1236 λe1,e2:exadecim.
1237  match e1 with
1238   [ x0 ⇒ match e2 with
1239    [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1240    | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1241   | x1 ⇒ match e2 with
1242    [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1243    | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1244   | x2 ⇒ match e2 with
1245    [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1246    | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1247   | x3 ⇒ match e2 with
1248    [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1249    | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1250   | x4 ⇒ match e2 with
1251    [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1252    | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1253   | x5 ⇒ match e2 with
1254    [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1255    | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1256   | x6 ⇒ match e2 with
1257    [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1258    | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1259   | x7 ⇒ match e2 with
1260    [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1261    | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1262   | x8 ⇒ match e2 with
1263    [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1264    | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1265   | x9 ⇒ match e2 with
1266    [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1267    | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1268   | xA ⇒ match e2 with
1269    [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1270    | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1271   | xB ⇒ match e2 with
1272    [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1273    | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1274   | xC ⇒ match e2 with
1275    [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1276    | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1277   | xD ⇒ match e2 with
1278    [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1279    | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1280   | xE ⇒ match e2 with
1281    [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1282    | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1283   | xF ⇒ match e2 with
1284    [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1285    | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1286   ].
1287
1288 (* operatore somma con data+carry → carry *)
1289 ndefinition plus_ex_dc_c ≝
1290 λe1,e2:exadecim.λc:bool.
1291  match c with
1292   [ true ⇒ match e1 with
1293    [ x0 ⇒ match e2 with
1294     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1295     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]
1296    | x1 ⇒ match e2 with
1297     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1298     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ]
1299    | x2 ⇒ match e2 with
1300     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1301     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1302    | x3 ⇒ match e2 with
1303     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1304     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1305    | x4 ⇒ match e2 with
1306     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1307     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1308    | x5 ⇒ match e2 with
1309     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1310     | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1311    | x6 ⇒ match e2 with
1312     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1313     | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1314    | x7 ⇒ match e2 with
1315     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1316     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1317    | x8 ⇒ match e2 with
1318     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1319     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1320    | x9 ⇒ match e2 with
1321     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
1322     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1323    | xA ⇒ match e2 with
1324     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1325     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1326    | xB ⇒ match e2 with
1327     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1328     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1329    | xC ⇒ match e2 with
1330     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1331     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1332    | xD ⇒ match e2 with
1333     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1334     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1335    | xE ⇒ match e2 with
1336     [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1337     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1338    | xF ⇒ match e2 with
1339     [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1340     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1341    ]
1342   | false ⇒ match e1 with
1343    [ x0 ⇒ match e2 with
1344     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1345     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1346    | x1 ⇒ match e2 with
1347     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1348     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]
1349    | x2 ⇒ match e2 with
1350     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1351     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ]
1352    | x3 ⇒ match e2 with
1353     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1354     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1355    | x4 ⇒ match e2 with
1356     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1357     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1358    | x5 ⇒ match e2 with
1359     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1360     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1361    | x6 ⇒ match e2 with
1362     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1363     | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1364    | x7 ⇒ match e2 with
1365     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1366     | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1367    | x8 ⇒ match e2 with
1368     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1369     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1370    | x9 ⇒ match e2 with
1371     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1372     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1373    | xA ⇒ match e2 with
1374     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
1375     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1376    | xB ⇒ match e2 with
1377     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1378     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1379    | xC ⇒ match e2 with
1380     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1381     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1382    | xD ⇒ match e2 with
1383     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1384     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1385    | xE ⇒ match e2 with
1386     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1387     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1388    | xF ⇒ match e2 with
1389     [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1390     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1391    ]].
1392
1393 (* operatore somma con data → carry *)
1394 ndefinition plus_ex_d_c ≝
1395 λe1,e2:exadecim.
1396  match e1 with
1397   [ x0 ⇒ match e2 with
1398    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1399    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1400   | x1 ⇒ match e2 with
1401    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1402    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]
1403   | x2 ⇒ match e2 with
1404    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1405    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ]
1406   | x3 ⇒ match e2 with
1407    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1408    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1409   | x4 ⇒ match e2 with
1410    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1411    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1412   | x5 ⇒ match e2 with
1413    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1414    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1415   | x6 ⇒ match e2 with
1416    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1417    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1418   | x7 ⇒ match e2 with
1419    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1420    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1421   | x8 ⇒ match e2 with
1422    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1423    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1424   | x9 ⇒ match e2 with
1425    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1426    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1427   | xA ⇒ match e2 with
1428    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
1429    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1430   | xB ⇒ match e2 with
1431    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1432    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1433   | xC ⇒ match e2 with
1434    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1435    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1436   | xD ⇒ match e2 with
1437    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1438    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1439   | xE ⇒ match e2 with
1440    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1441    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1442   | xF ⇒ match e2 with
1443    [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1444    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1445   ].
1446
1447 (* operatore Most Significant Bit *)
1448 ndefinition MSB_ex ≝
1449 λe:exadecim.match e with
1450  [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1451  | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1452  | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
1453  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ].
1454
1455 (* esadecimali → naturali *)
1456 ndefinition nat_of_exadecim : exadecim → nat ≝
1457 λe:exadecim.
1458  match e with
1459   [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2  | x3 ⇒ 3  | x4 ⇒ 4  | x5 ⇒ 5  | x6 ⇒ 6  | x7 ⇒ 7
1460   | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
1461
1462 (* operatore predecessore *)
1463 ndefinition pred_ex ≝
1464 λe:exadecim.
1465  match e with
1466   [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1467   | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1468
1469 (* operatore successore *)
1470 ndefinition succ_ex ≝
1471 λe:exadecim.
1472  match e with
1473   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1474   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1475
1476 (* operatore neg/complemento a 2 *)
1477 ndefinition compl_ex ≝
1478 λe:exadecim.match e with
1479  [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1480  | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1481  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1482  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1483
1484 (* iteratore sugli esadecimali *)
1485 ndefinition forall_exadecim ≝ λP.
1486  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1487  P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.