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