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