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