matita/contribs/assembly/freescale/exadecim.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/extra.ma".
  28
  29 (* ***************************** *)
  30 (* DEFINIZIONE DEGLI ESADECIMALI *)
  31 (* ***************************** *)
  32
  33 inductive exadecim : Type ≝
  34   x0: exadecim
  35 | x1: exadecim
  36 | x2: exadecim
  37 | x3: exadecim
  38 | x4: exadecim
  39 | x5: exadecim
  40 | x6: exadecim
  41 | x7: exadecim
  42 | x8: exadecim
  43 | x9: exadecim
  44 | xA: exadecim
  45 | xB: exadecim
  46 | xC: exadecim
  47 | xD: exadecim
  48 | xE: exadecim
  49 | xF: exadecim.
  50
  51 (* operatore = *)
  52 definition eq_ex ≝
  53 λe1,e2:exadecim.
  54  match e1 with
  55   [ x0 ⇒ match e2 with
  56    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  57    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  58    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  59    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  60   | x1 ⇒ match e2 with
  61    [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
  62    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  63    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  64    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  65   | x2 ⇒ match e2 with
  66    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
  67    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  68    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  69    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  70   | x3 ⇒ match e2 with
  71    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
  72    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  73    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  74    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  75   | x4 ⇒ match e2 with
  76    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  77    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  78    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  79    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  80   | x5 ⇒ match e2 with
  81    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  82    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
  83    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  84    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  85   | x6 ⇒ match e2 with
  86    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  87    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
  88    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  89    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  90   | x7 ⇒ match e2 with
  91    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  92    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
  93    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  94    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  95   | x8 ⇒ match e2 with
  96    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  97    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  98    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  99    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 100   | x9 ⇒ match e2 with
 101    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 102    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 103    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 104    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 105   | xA ⇒ match e2 with
 106    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 107    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 108    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 109    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 110   | xB ⇒ match e2 with
 111    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 112    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 113    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 114    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 115   | xC ⇒ match e2 with
 116    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 117    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 118    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 119    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 120   | xD ⇒ match e2 with
 121    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 122    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 123    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 124    | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 125   | xE ⇒ match e2 with
 126    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 127    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 128    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 129    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ]
 130   | xF ⇒ match e2 with
 131    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 132    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 133    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 134    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
 135   ].
 136
 137 (* operatore < *)
 138 definition lt_ex ≝
 139 λe1,e2:exadecim.
 140  match e1 with
 141   [ x0 ⇒ match e2 with
 142    [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
 143    | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
 144    | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true
 145    | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
 146   | x1 ⇒ match e2 with
 147    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
 148    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
 149    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true
 150    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ]
 151   | x2 ⇒ match e2 with
 152    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 153    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 154    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 155    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 156   | x3 ⇒ match e2 with
 157    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 158    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 159    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 160    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 161   | x4 ⇒ match e2 with
 162    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 163    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 164    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 165    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 166   | x5 ⇒ match e2 with
 167    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 168    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
 169    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 170    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 171   | x6 ⇒ match e2 with
 172    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 173    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 174    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 175    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 176   | x7 ⇒ match e2 with
 177    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 178    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 179    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 180    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 181   | x8 ⇒ match e2 with
 182    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 183    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 184    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 185    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 186   | x9 ⇒ match e2 with
 187    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 188    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 189    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true
 190    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 191   | xA ⇒ match e2 with
 192    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 193    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 194    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 195    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 196   | xB ⇒ match e2 with
 197    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 198    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 199    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 200    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 201   | xC ⇒ match e2 with
 202    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 203    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 204    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 205    | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 206   | xD ⇒ match e2 with
 207    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 208    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 209    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 210    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ]
 211   | xE ⇒ match e2 with
 212    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 213    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 214    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 215    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
 216   | xF ⇒ match e2 with
 217    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 218    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 219    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 220    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 221   ].
 222
 223 (* operatore ≤ *)
 224 definition le_ex ≝
 225 λe1,e2:exadecim.
 226  match e1 with
 227   [ x0 ⇒ match e2 with
 228    [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
 229    | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
 230    | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
 231    | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
 232   | x1 ⇒ match e2 with
 233    [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
 234    | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
 235    | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true
 236    | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
 237   | x2 ⇒ match e2 with
 238    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
 239    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
 240    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true
 241    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ]
 242   | x3 ⇒ match e2 with
 243    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 244    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 245    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 246    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 247   | x4 ⇒ match e2 with
 248    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 249    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 250    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 251    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 252   | x5 ⇒ match e2 with
 253    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 254    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 255    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 256    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 257   | x6 ⇒ match e2 with
 258    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 259    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
 260    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 261    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 262   | x7 ⇒ match e2 with
 263    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 264    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 265    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 266    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 267   | x8 ⇒ match e2 with
 268    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 269    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 270    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 271    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 272   | x9 ⇒ match e2 with
 273    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 274    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 275    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 276    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 277   | xA ⇒ match e2 with
 278    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 279    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 280    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true
 281    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 282   | xB ⇒ match e2 with
 283    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 284    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 285    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 286    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 287   | xC ⇒ match e2 with
 288    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 289    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 290    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 291    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 292   | xD ⇒ match e2 with
 293    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 294    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 295    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 296    | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 297   | xE ⇒ match e2 with
 298    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 299    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 300    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 301    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ]
 302   | xF ⇒ match e2 with
 303    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 304    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 305    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 306    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
 307   ].
 308
 309 (* operatore > *)
 310 definition gt_ex ≝
 311 λe1,e2:exadecim.
 312  match e1 with
 313   [ x0 ⇒ match e2 with
 314    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 315    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 316    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 317    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 318   | x1 ⇒ match e2 with
 319    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 320    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 321    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 322    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 323   | x2 ⇒ match e2 with
 324    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
 325    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 326    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 327    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 328   | x3 ⇒ match e2 with
 329    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false
 330    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 331    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 332    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 333   | x4 ⇒ match e2 with
 334    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 335    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 336    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 337    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 338   | x5 ⇒ match e2 with
 339    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 340    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 341    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 342    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 343   | x6 ⇒ match e2 with
 344    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 345    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 346    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 347    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 348   | x7 ⇒ match e2 with
 349    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 350    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
 351    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 352    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 353   | x8 ⇒ match e2 with
 354    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 355    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 356    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 357    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 358   | x9 ⇒ match e2 with
 359    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 360    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 361    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 362    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 363   | xA ⇒ match e2 with
 364    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 365    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 366    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 367    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 368   | xB ⇒ match e2 with
 369    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 370    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 371    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false
 372    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 373   | xC ⇒ match e2 with
 374    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 375    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 376    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 377    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 378   | xD ⇒ match e2 with
 379    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 380    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 381    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 382    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 383   | xE ⇒ match e2 with
 384    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 385    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 386    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 387    | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 388   | xF ⇒ match e2 with
 389    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 390    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 391    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 392    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
 393   ].
 394
 395 (* operatore ≥ *)
 396 definition ge_ex ≝
 397 λe1,e2:exadecim.
 398  match e1 with
 399   [ x0 ⇒ match e2 with
 400    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 401    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 402    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 403    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 404   | x1 ⇒ match e2 with
 405    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
 406    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 407    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 408    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 409   | x2 ⇒ match e2 with
 410    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false
 411    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 412    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 413    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 414   | x3 ⇒ match e2 with
 415    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 416    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 417    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 418    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 419   | x4 ⇒ match e2 with
 420    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 421    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 422    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 423    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 424   | x5 ⇒ match e2 with
 425    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 426    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 427    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 428    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 429   | x6 ⇒ match e2 with
 430    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 431    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
 432    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 433    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 434   | x7 ⇒ match e2 with
 435    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 436    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 437    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 438    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 439   | x8 ⇒ match e2 with
 440    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 441    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 442    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 443    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 444   | x9 ⇒ match e2 with
 445    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 446    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 447    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 448    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 449   | xA ⇒ match e2 with
 450    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 451    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 452    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false
 453    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 454   | xB ⇒ match e2 with
 455    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 456    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 457    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 458    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 459   | xC ⇒ match e2 with
 460    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 461    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 462    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 463    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 464   | xD ⇒ match e2 with
 465    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 466    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 467    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 468    | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 469   | xE ⇒ match e2 with
 470    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 471    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 472    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 473    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
 474   | xF ⇒ match e2 with
 475    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true
 476    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
 477    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
 478    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
 479   ].
 480
 481 (* operatore and *)
 482 definition and_ex ≝
 483 λe1,e2:exadecim.match e1 with
 484  [ x0 ⇒ match e2 with
 485   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 486   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
 487   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
 488   | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
 489  | x1 ⇒ match e2 with
 490   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 491   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
 492   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
 493   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
 494  | x2 ⇒ match e2 with
 495   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 496   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
 497   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
 498   | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
 499  | x3 ⇒ match e2 with
 500   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 501   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
 502   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
 503   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
 504  | x4 ⇒ match e2 with
 505   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 506   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
 507   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
 508   | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
 509  | x5 ⇒ match e2 with
 510   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 511   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
 512   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
 513   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
 514  | x6 ⇒ match e2 with
 515   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 516   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
 517   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
 518   | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
 519  | x7 ⇒ match e2 with
 520   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 521   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 522   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
 523   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
 524  | x8 ⇒ match e2 with
 525   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 526   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
 527   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
 528   | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
 529  | x9 ⇒ match e2 with
 530   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 531   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
 532   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
 533   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
 534  | xA ⇒ match e2 with
 535   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 536   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
 537   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
 538   | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
 539  | xB ⇒ match e2 with
 540   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 541   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
 542   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 543   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
 544  | xC ⇒ match e2 with
 545   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
 546   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
 547   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
 548   | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
 549  | xD ⇒ match e2 with
 550   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
 551   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
 552   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
 553   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
 554  | xE ⇒ match e2 with
 555   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
 556   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
 557   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
 558   | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
 559  | xF ⇒ match e2 with
 560   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 561   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 562   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 563   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 564  ].
 565
 566 (* operatore or *)
 567 definition or_ex ≝
 568 λe1,e2:exadecim.match e1 with
 569  [ x0 ⇒ match e2 with
 570   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 571   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 572   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 573   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 574  | x1 ⇒ match e2 with
 575   [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
 576   | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
 577   | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
 578   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 579  | x2 ⇒ match e2 with
 580   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
 581   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
 582   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
 583   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 584  | x3 ⇒ match e2 with
 585   [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
 586   | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
 587   | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
 588   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 589  | x4 ⇒ match e2 with
 590   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
 591   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 592   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
 593   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 594  | x5 ⇒ match e2 with
 595   [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
 596   | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
 597   | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
 598   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 599  | x6 ⇒ match e2 with
 600   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
 601   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
 602   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
 603   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 604  | x7 ⇒ match e2 with
 605   [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
 606   | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
 607   | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
 608   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 609  | x8 ⇒ match e2 with
 610   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
 611   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
 612   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 613   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 614  | x9 ⇒ match e2 with
 615   [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
 616   | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
 617   | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
 618   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 619  | xA ⇒ match e2 with
 620   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
 621   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
 622   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
 623   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 624  | xB ⇒ match e2 with
 625   [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
 626   | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
 627   | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
 628   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 629  | xC ⇒ match e2 with
 630   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
 631   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
 632   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
 633   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 634  | xD ⇒ match e2 with
 635   [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
 636   | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
 637   | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
 638   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 639  | xE ⇒ match e2 with
 640   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
 641   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
 642   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
 643   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 644  | xF ⇒ match e2 with
 645   [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
 646   | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
 647   | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
 648   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 649  ].
 650
 651 (* operatore xor *)
 652 definition xor_ex ≝
 653 λe1,e2:exadecim.match e1 with
 654  [ x0 ⇒ match e2 with
 655   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
 656   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
 657   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
 658   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 659  | x1 ⇒ match e2 with
 660   [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
 661   | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
 662   | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
 663   | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
 664  | x2 ⇒ match e2 with
 665   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
 666   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
 667   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
 668   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
 669  | x3 ⇒ match e2 with
 670   [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
 671   | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
 672   | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
 673   | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
 674  | x4 ⇒ match e2 with
 675   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
 676   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
 677   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
 678   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
 679  | x5 ⇒ match e2 with
 680   [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
 681   | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
 682   | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
 683   | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
 684  | x6 ⇒ match e2 with
 685   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
 686   | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
 687   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
 688   | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
 689  | x7 ⇒ match e2 with
 690   [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
 691   | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
 692   | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
 693   | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
 694  | x8 ⇒ match e2 with
 695   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
 696   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
 697   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
 698   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
 699  | x9 ⇒ match e2 with
 700   [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
 701   | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
 702   | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
 703   | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
 704  | xA ⇒ match e2 with
 705   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
 706   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
 707   | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
 708   | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
 709  | xB ⇒ match e2 with
 710   [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
 711   | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
 712   | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
 713   | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
 714  | xC ⇒ match e2 with
 715   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
 716   | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
 717   | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
 718   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
 719  | xD ⇒ match e2 with
 720   [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
 721   | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
 722   | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
 723   | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
 724  | xE ⇒ match e2 with
 725   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
 726   | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
 727   | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
 728   | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
 729  | xF ⇒ match e2 with
 730   [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
 731   | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
 732   | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
 733   | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
 734  ].
 735
 736 (* operatore rotazione destra con carry *)
 737 definition rcr_ex ≝
 738 λe:exadecim.λc:bool.match c with
 739  [ true ⇒ match e with
 740   [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
 741   | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
 742   | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
 743   | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
 744   | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
 745   | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
 746   | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
 747   | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
 748  | false ⇒ match e with
 749   [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
 750   | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
 751   | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
 752   | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
 753   | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
 754   | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
 755   | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
 756   | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
 757  ].
 758
 759 (* operatore shift destro *)
 760 definition shr_ex ≝
 761 λe:exadecim.match e with
 762  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
 763  | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
 764  | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
 765  | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
 766  | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
 767  | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
 768  | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
 769  | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
 770
 771 (* operatore rotazione destra *)
 772 definition ror_ex ≝
 773 λe:exadecim.match e with
 774  [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
 775  | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
 776  | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
 777  | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
 778
 779 (* operatore rotazione destra n-volte *)
 780 let rec ror_ex_n (e:exadecim) (n:nat) on n ≝
 781  match n with
 782   [ O ⇒ e
 783   | S n' ⇒ ror_ex_n (ror_ex e) n' ].
 784
 785 (* operatore rotazione sinistra con carry *)
 786 definition rcl_ex ≝
 787 λe:exadecim.λc:bool.match c with
 788  [ true ⇒ match e with
 789   [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
 790   | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
 791   | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
 792   | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
 793   | x8 ⇒ pair exadecim bool x1 true  | x9 ⇒ pair exadecim bool x3 true
 794   | xA ⇒ pair exadecim bool x5 true  | xB ⇒ pair exadecim bool x7 true
 795   | xC ⇒ pair exadecim bool x9 true  | xD ⇒ pair exadecim bool xB true
 796   | xE ⇒ pair exadecim bool xD true  | xF ⇒ pair exadecim bool xF true ]
 797  | false ⇒ match e with
 798   [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
 799   | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
 800   | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
 801   | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
 802   | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
 803   | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
 804   | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
 805   | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ]
 806  ].
 807
 808 (* operatore shift sinistro *)
 809 definition shl_ex ≝
 810 λe:exadecim.match e with
 811  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
 812  | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
 813  | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
 814  | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
 815  | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
 816  | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
 817  | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
 818  | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ].
 819
 820 (* operatore rotazione sinistra *)
 821 definition rol_ex ≝
 822 λe:exadecim.match e with
 823  [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
 824  | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
 825  | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
 826  | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
 827
 828 (* operatore rotazione sinistra n-volte *)
 829 let rec rol_ex_n (e:exadecim) (n:nat) on n ≝
 830  match n with
 831   [ O ⇒ e
 832   | S n' ⇒ rol_ex_n (rol_ex e) n' ].
 833
 834 (* operatore not/complemento a 1 *)
 835 definition not_ex ≝
 836 λe:exadecim.match e with
 837  [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
 838  | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
 839  | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
 840  | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
 841
 842 (* operatore somma con carry *)
 843 definition plus_ex ≝
 844 λe1,e2:exadecim.λc:bool.
 845   match c with
 846    [ true ⇒
 847       match e1 with
 848        [ x0 ⇒
 849            match e2 with
 850             [ x0 ⇒ pair exadecim bool x1 false
 851             | x1 ⇒ pair exadecim bool x2 false
 852             | x2 ⇒ pair exadecim bool x3 false
 853             | x3 ⇒ pair exadecim bool x4 false
 854             | x4 ⇒ pair exadecim bool x5 false
 855             | x5 ⇒ pair exadecim bool x6 false
 856             | x6 ⇒ pair exadecim bool x7 false
 857             | x7 ⇒ pair exadecim bool x8 false
 858             | x8 ⇒ pair exadecim bool x9 false
 859             | x9 ⇒ pair exadecim bool xA false
 860             | xA ⇒ pair exadecim bool xB false
 861             | xB ⇒ pair exadecim bool xC false
 862             | xC ⇒ pair exadecim bool xD false
 863             | xD ⇒ pair exadecim bool xE false
 864             | xE ⇒ pair exadecim bool xF false
 865             | xF ⇒ pair exadecim bool x0 true ]
 866        | x1 ⇒
 867            match e2 with
 868             [ x0 ⇒ pair exadecim bool x2 false
 869             | x1 ⇒ pair exadecim bool x3 false
 870             | x2 ⇒ pair exadecim bool x4 false
 871             | x3 ⇒ pair exadecim bool x5 false
 872             | x4 ⇒ pair exadecim bool x6 false
 873             | x5 ⇒ pair exadecim bool x7 false
 874             | x6 ⇒ pair exadecim bool x8 false
 875             | x7 ⇒ pair exadecim bool x9 false
 876             | x8 ⇒ pair exadecim bool xA false
 877             | x9 ⇒ pair exadecim bool xB false
 878             | xA ⇒ pair exadecim bool xC false
 879             | xB ⇒ pair exadecim bool xD false
 880             | xC ⇒ pair exadecim bool xE false
 881             | xD ⇒ pair exadecim bool xF false
 882             | xE ⇒ pair exadecim bool x0 true
 883             | xF ⇒ pair exadecim bool x1 true ]
 884        | x2 ⇒
 885            match e2 with
 886             [ x0 ⇒ pair exadecim bool x3 false
 887             | x1 ⇒ pair exadecim bool x4 false
 888             | x2 ⇒ pair exadecim bool x5 false
 889             | x3 ⇒ pair exadecim bool x6 false
 890             | x4 ⇒ pair exadecim bool x7 false
 891             | x5 ⇒ pair exadecim bool x8 false
 892             | x6 ⇒ pair exadecim bool x9 false
 893             | x7 ⇒ pair exadecim bool xA false
 894             | x8 ⇒ pair exadecim bool xB false
 895             | x9 ⇒ pair exadecim bool xC false
 896             | xA ⇒ pair exadecim bool xD false
 897             | xB ⇒ pair exadecim bool xE false
 898             | xC ⇒ pair exadecim bool xF false
 899             | xD ⇒ pair exadecim bool x0 true
 900             | xE ⇒ pair exadecim bool x1 true
 901             | xF ⇒ pair exadecim bool x2 true ]
 902        | x3 ⇒
 903            match e2 with
 904             [ x0 ⇒ pair exadecim bool x4 false
 905             | x1 ⇒ pair exadecim bool x5 false
 906             | x2 ⇒ pair exadecim bool x6 false
 907             | x3 ⇒ pair exadecim bool x7 false
 908             | x4 ⇒ pair exadecim bool x8 false
 909             | x5 ⇒ pair exadecim bool x9 false
 910             | x6 ⇒ pair exadecim bool xA false
 911             | x7 ⇒ pair exadecim bool xB false
 912             | x8 ⇒ pair exadecim bool xC false
 913             | x9 ⇒ pair exadecim bool xD false
 914             | xA ⇒ pair exadecim bool xE false
 915             | xB ⇒ pair exadecim bool xF false
 916             | xC ⇒ pair exadecim bool x0 true
 917             | xD ⇒ pair exadecim bool x1 true
 918             | xE ⇒ pair exadecim bool x2 true
 919             | xF ⇒ pair exadecim bool x3 true ]
 920        | x4 ⇒
 921            match e2 with
 922             [ x0 ⇒ pair exadecim bool x5 false
 923             | x1 ⇒ pair exadecim bool x6 false
 924             | x2 ⇒ pair exadecim bool x7 false
 925             | x3 ⇒ pair exadecim bool x8 false
 926             | x4 ⇒ pair exadecim bool x9 false
 927             | x5 ⇒ pair exadecim bool xA false
 928             | x6 ⇒ pair exadecim bool xB false
 929             | x7 ⇒ pair exadecim bool xC false
 930             | x8 ⇒ pair exadecim bool xD false
 931             | x9 ⇒ pair exadecim bool xE false
 932             | xA ⇒ pair exadecim bool xF false
 933             | xB ⇒ pair exadecim bool x0 true
 934             | xC ⇒ pair exadecim bool x1 true
 935             | xD ⇒ pair exadecim bool x2 true
 936             | xE ⇒ pair exadecim bool x3 true
 937             | xF ⇒ pair exadecim bool x4 true ]
 938        | x5 ⇒
 939            match e2 with
 940             [ x0 ⇒ pair exadecim bool x6 false
 941             | x1 ⇒ pair exadecim bool x7 false
 942             | x2 ⇒ pair exadecim bool x8 false
 943             | x3 ⇒ pair exadecim bool x9 false
 944             | x4 ⇒ pair exadecim bool xA false
 945             | x5 ⇒ pair exadecim bool xB false
 946             | x6 ⇒ pair exadecim bool xC false
 947             | x7 ⇒ pair exadecim bool xD false
 948             | x8 ⇒ pair exadecim bool xE false
 949             | x9 ⇒ pair exadecim bool xF false
 950             | xA ⇒ pair exadecim bool x0 true
 951             | xB ⇒ pair exadecim bool x1 true
 952             | xC ⇒ pair exadecim bool x2 true
 953             | xD ⇒ pair exadecim bool x3 true
 954             | xE ⇒ pair exadecim bool x4 true
 955             | xF ⇒ pair exadecim bool x5 true ]
 956        | x6 ⇒
 957            match e2 with
 958             [ x0 ⇒ pair exadecim bool x7 false
 959             | x1 ⇒ pair exadecim bool x8 false
 960             | x2 ⇒ pair exadecim bool x9 false
 961             | x3 ⇒ pair exadecim bool xA false
 962             | x4 ⇒ pair exadecim bool xB false
 963             | x5 ⇒ pair exadecim bool xC false
 964             | x6 ⇒ pair exadecim bool xD false
 965             | x7 ⇒ pair exadecim bool xE false
 966             | x8 ⇒ pair exadecim bool xF false
 967             | x9 ⇒ pair exadecim bool x0 true
 968             | xA ⇒ pair exadecim bool x1 true
 969             | xB ⇒ pair exadecim bool x2 true
 970             | xC ⇒ pair exadecim bool x3 true
 971             | xD ⇒ pair exadecim bool x4 true
 972             | xE ⇒ pair exadecim bool x5 true
 973             | xF ⇒ pair exadecim bool x6 true ]
 974        | x7 ⇒
 975            match e2 with
 976             [ x0 ⇒ pair exadecim bool x8 false
 977             | x1 ⇒ pair exadecim bool x9 false
 978             | x2 ⇒ pair exadecim bool xA false
 979             | x3 ⇒ pair exadecim bool xB false
 980             | x4 ⇒ pair exadecim bool xC false
 981             | x5 ⇒ pair exadecim bool xD false
 982             | x6 ⇒ pair exadecim bool xE false
 983             | x7 ⇒ pair exadecim bool xF false
 984             | x8 ⇒ pair exadecim bool x0 true
 985             | x9 ⇒ pair exadecim bool x1 true
 986             | xA ⇒ pair exadecim bool x2 true
 987             | xB ⇒ pair exadecim bool x3 true
 988             | xC ⇒ pair exadecim bool x4 true
 989             | xD ⇒ pair exadecim bool x5 true
 990             | xE ⇒ pair exadecim bool x6 true
 991             | xF ⇒ pair exadecim bool x7 true ]
 992        | x8 ⇒
 993            match e2 with
 994             [ x0 ⇒ pair exadecim bool x9 false
 995             | x1 ⇒ pair exadecim bool xA false
 996             | x2 ⇒ pair exadecim bool xB false
 997             | x3 ⇒ pair exadecim bool xC false
 998             | x4 ⇒ pair exadecim bool xD false
 999             | x5 ⇒ pair exadecim bool xE false
1000             | x6 ⇒ pair exadecim bool xF false
1001             | x7 ⇒ pair exadecim bool x0 true
1002             | x8 ⇒ pair exadecim bool x1 true
1003             | x9 ⇒ pair exadecim bool x2 true
1004             | xA ⇒ pair exadecim bool x3 true
1005             | xB ⇒ pair exadecim bool x4 true
1006             | xC ⇒ pair exadecim bool x5 true
1007             | xD ⇒ pair exadecim bool x6 true
1008             | xE ⇒ pair exadecim bool x7 true
1009             | xF ⇒ pair exadecim bool x8 true ]
1010        | x9 ⇒
1011            match e2 with
1012             [ x0 ⇒ pair exadecim bool xA false
1013             | x1 ⇒ pair exadecim bool xB false
1014             | x2 ⇒ pair exadecim bool xC false
1015             | x3 ⇒ pair exadecim bool xD false
1016             | x4 ⇒ pair exadecim bool xE false
1017             | x5 ⇒ pair exadecim bool xF false
1018             | x6 ⇒ pair exadecim bool x0 true
1019             | x7 ⇒ pair exadecim bool x1 true
1020             | x8 ⇒ pair exadecim bool x2 true
1021             | x9 ⇒ pair exadecim bool x3 true
1022             | xA ⇒ pair exadecim bool x4 true
1023             | xB ⇒ pair exadecim bool x5 true
1024             | xC ⇒ pair exadecim bool x6 true
1025             | xD ⇒ pair exadecim bool x7 true
1026             | xE ⇒ pair exadecim bool x8 true
1027             | xF ⇒ pair exadecim bool x9 true ]
1028        | xA ⇒
1029            match e2 with
1030             [ x0 ⇒ pair exadecim bool xB false
1031             | x1 ⇒ pair exadecim bool xC false
1032             | x2 ⇒ pair exadecim bool xD false
1033             | x3 ⇒ pair exadecim bool xE false
1034             | x4 ⇒ pair exadecim bool xF false
1035             | x5 ⇒ pair exadecim bool x0 true
1036             | x6 ⇒ pair exadecim bool x1 true
1037             | x7 ⇒ pair exadecim bool x2 true
1038             | x8 ⇒ pair exadecim bool x3 true
1039             | x9 ⇒ pair exadecim bool x4 true
1040             | xA ⇒ pair exadecim bool x5 true
1041             | xB ⇒ pair exadecim bool x6 true
1042             | xC ⇒ pair exadecim bool x7 true
1043             | xD ⇒ pair exadecim bool x8 true
1044             | xE ⇒ pair exadecim bool x9 true
1045             | xF ⇒ pair exadecim bool xA true ]
1046        | xB ⇒
1047            match e2 with
1048             [ x0 ⇒ pair exadecim bool xC false
1049             | x1 ⇒ pair exadecim bool xD false
1050             | x2 ⇒ pair exadecim bool xE false
1051             | x3 ⇒ pair exadecim bool xF false
1052             | x4 ⇒ pair exadecim bool x0 true
1053             | x5 ⇒ pair exadecim bool x1 true
1054             | x6 ⇒ pair exadecim bool x2 true
1055             | x7 ⇒ pair exadecim bool x3 true
1056             | x8 ⇒ pair exadecim bool x4 true
1057             | x9 ⇒ pair exadecim bool x5 true
1058             | xA ⇒ pair exadecim bool x6 true
1059             | xB ⇒ pair exadecim bool x7 true
1060             | xC ⇒ pair exadecim bool x8 true
1061             | xD ⇒ pair exadecim bool x9 true
1062             | xE ⇒ pair exadecim bool xA true
1063             | xF ⇒ pair exadecim bool xB true ]
1064        | xC ⇒
1065            match e2 with
1066             [ x0 ⇒ pair exadecim bool xD false
1067             | x1 ⇒ pair exadecim bool xE false
1068             | x2 ⇒ pair exadecim bool xF false
1069             | x3 ⇒ pair exadecim bool x0 true
1070             | x4 ⇒ pair exadecim bool x1 true
1071             | x5 ⇒ pair exadecim bool x2 true
1072             | x6 ⇒ pair exadecim bool x3 true
1073             | x7 ⇒ pair exadecim bool x4 true
1074             | x8 ⇒ pair exadecim bool x5 true
1075             | x9 ⇒ pair exadecim bool x6 true
1076             | xA ⇒ pair exadecim bool x7 true
1077             | xB ⇒ pair exadecim bool x8 true
1078             | xC ⇒ pair exadecim bool x9 true
1079             | xD ⇒ pair exadecim bool xA true
1080             | xE ⇒ pair exadecim bool xB true
1081             | xF ⇒ pair exadecim bool xC true ]
1082        | xD ⇒
1083            match e2 with
1084             [ x0 ⇒ pair exadecim bool xE false
1085             | x1 ⇒ pair exadecim bool xF false
1086             | x2 ⇒ pair exadecim bool x0 true
1087             | x3 ⇒ pair exadecim bool x1 true
1088             | x4 ⇒ pair exadecim bool x2 true
1089             | x5 ⇒ pair exadecim bool x3 true
1090             | x6 ⇒ pair exadecim bool x4 true
1091             | x7 ⇒ pair exadecim bool x5 true
1092             | x8 ⇒ pair exadecim bool x6 true
1093             | x9 ⇒ pair exadecim bool x7 true
1094             | xA ⇒ pair exadecim bool x8 true
1095             | xB ⇒ pair exadecim bool x9 true
1096             | xC ⇒ pair exadecim bool xA true
1097             | xD ⇒ pair exadecim bool xB true
1098             | xE ⇒ pair exadecim bool xC true
1099             | xF ⇒ pair exadecim bool xD true ]
1100        | xE ⇒
1101            match e2 with
1102             [ x0 ⇒ pair exadecim bool xF false
1103             | x1 ⇒ pair exadecim bool x0 true
1104             | x2 ⇒ pair exadecim bool x1 true
1105             | x3 ⇒ pair exadecim bool x2 true
1106             | x4 ⇒ pair exadecim bool x3 true
1107             | x5 ⇒ pair exadecim bool x4 true
1108             | x6 ⇒ pair exadecim bool x5 true
1109             | x7 ⇒ pair exadecim bool x6 true
1110             | x8 ⇒ pair exadecim bool x7 true
1111             | x9 ⇒ pair exadecim bool x8 true
1112             | xA ⇒ pair exadecim bool x9 true
1113             | xB ⇒ pair exadecim bool xA true
1114             | xC ⇒ pair exadecim bool xB true
1115             | xD ⇒ pair exadecim bool xC true
1116             | xE ⇒ pair exadecim bool xD true
1117             | xF ⇒ pair exadecim bool xE true ]
1118        | xF ⇒
1119            match e2 with
1120             [ x0 ⇒ pair exadecim bool x0 true
1121             | x1 ⇒ pair exadecim bool x1 true
1122             | x2 ⇒ pair exadecim bool x2 true
1123             | x3 ⇒ pair exadecim bool x3 true
1124             | x4 ⇒ pair exadecim bool x4 true
1125             | x5 ⇒ pair exadecim bool x5 true
1126             | x6 ⇒ pair exadecim bool x6 true
1127             | x7 ⇒ pair exadecim bool x7 true
1128             | x8 ⇒ pair exadecim bool x8 true
1129             | x9 ⇒ pair exadecim bool x9 true
1130             | xA ⇒ pair exadecim bool xA true
1131             | xB ⇒ pair exadecim bool xB true
1132             | xC ⇒ pair exadecim bool xC true
1133             | xD ⇒ pair exadecim bool xD true
1134             | xE ⇒ pair exadecim bool xE true
1135             | xF ⇒ pair exadecim bool xF true ]
1136        ]
1137    | false ⇒
1138       match e1 with
1139        [ x0 ⇒
1140            match e2 with
1141             [ x0 ⇒ pair exadecim bool x0 false
1142             | x1 ⇒ pair exadecim bool x1 false
1143             | x2 ⇒ pair exadecim bool x2 false
1144             | x3 ⇒ pair exadecim bool x3 false
1145             | x4 ⇒ pair exadecim bool x4 false
1146             | x5 ⇒ pair exadecim bool x5 false
1147             | x6 ⇒ pair exadecim bool x6 false
1148             | x7 ⇒ pair exadecim bool x7 false
1149             | x8 ⇒ pair exadecim bool x8 false
1150             | x9 ⇒ pair exadecim bool x9 false
1151             | xA ⇒ pair exadecim bool xA false
1152             | xB ⇒ pair exadecim bool xB false
1153             | xC ⇒ pair exadecim bool xC false
1154             | xD ⇒ pair exadecim bool xD false
1155             | xE ⇒ pair exadecim bool xE false
1156             | xF ⇒ pair exadecim bool xF false ]
1157        | x1 ⇒
1158            match e2 with
1159             [ x0 ⇒ pair exadecim bool x1 false
1160             | x1 ⇒ pair exadecim bool x2 false
1161             | x2 ⇒ pair exadecim bool x3 false
1162             | x3 ⇒ pair exadecim bool x4 false
1163             | x4 ⇒ pair exadecim bool x5 false
1164             | x5 ⇒ pair exadecim bool x6 false
1165             | x6 ⇒ pair exadecim bool x7 false
1166             | x7 ⇒ pair exadecim bool x8 false
1167             | x8 ⇒ pair exadecim bool x9 false
1168             | x9 ⇒ pair exadecim bool xA false
1169             | xA ⇒ pair exadecim bool xB false
1170             | xB ⇒ pair exadecim bool xC false
1171             | xC ⇒ pair exadecim bool xD false
1172             | xD ⇒ pair exadecim bool xE false
1173             | xE ⇒ pair exadecim bool xF false
1174             | xF ⇒ pair exadecim bool x0 true ]
1175        | x2 ⇒
1176            match e2 with
1177             [ x0 ⇒ pair exadecim bool x2 false
1178             | x1 ⇒ pair exadecim bool x3 false
1179             | x2 ⇒ pair exadecim bool x4 false
1180             | x3 ⇒ pair exadecim bool x5 false
1181             | x4 ⇒ pair exadecim bool x6 false
1182             | x5 ⇒ pair exadecim bool x7 false
1183             | x6 ⇒ pair exadecim bool x8 false
1184             | x7 ⇒ pair exadecim bool x9 false
1185             | x8 ⇒ pair exadecim bool xA false
1186             | x9 ⇒ pair exadecim bool xB false
1187             | xA ⇒ pair exadecim bool xC false
1188             | xB ⇒ pair exadecim bool xD false
1189             | xC ⇒ pair exadecim bool xE false
1190             | xD ⇒ pair exadecim bool xF false
1191             | xE ⇒ pair exadecim bool x0 true
1192             | xF ⇒ pair exadecim bool x1 true ]
1193        | x3 ⇒
1194            match e2 with
1195             [ x0 ⇒ pair exadecim bool x3 false
1196             | x1 ⇒ pair exadecim bool x4 false
1197             | x2 ⇒ pair exadecim bool x5 false
1198             | x3 ⇒ pair exadecim bool x6 false
1199             | x4 ⇒ pair exadecim bool x7 false
1200             | x5 ⇒ pair exadecim bool x8 false
1201             | x6 ⇒ pair exadecim bool x9 false
1202             | x7 ⇒ pair exadecim bool xA false
1203             | x8 ⇒ pair exadecim bool xB false
1204             | x9 ⇒ pair exadecim bool xC false
1205             | xA ⇒ pair exadecim bool xD false
1206             | xB ⇒ pair exadecim bool xE false
1207             | xC ⇒ pair exadecim bool xF false
1208             | xD ⇒ pair exadecim bool x0 true
1209             | xE ⇒ pair exadecim bool x1 true
1210             | xF ⇒ pair exadecim bool x2 true ]
1211        | x4 ⇒
1212            match e2 with
1213             [ x0 ⇒ pair exadecim bool x4 false
1214             | x1 ⇒ pair exadecim bool x5 false
1215             | x2 ⇒ pair exadecim bool x6 false
1216             | x3 ⇒ pair exadecim bool x7 false
1217             | x4 ⇒ pair exadecim bool x8 false
1218             | x5 ⇒ pair exadecim bool x9 false
1219             | x6 ⇒ pair exadecim bool xA false
1220             | x7 ⇒ pair exadecim bool xB false
1221             | x8 ⇒ pair exadecim bool xC false
1222             | x9 ⇒ pair exadecim bool xD false
1223             | xA ⇒ pair exadecim bool xE false
1224             | xB ⇒ pair exadecim bool xF false
1225             | xC ⇒ pair exadecim bool x0 true
1226             | xD ⇒ pair exadecim bool x1 true
1227             | xE ⇒ pair exadecim bool x2 true
1228             | xF ⇒ pair exadecim bool x3 true ]
1229        | x5 ⇒
1230            match e2 with
1231             [ x0 ⇒ pair exadecim bool x5 false
1232             | x1 ⇒ pair exadecim bool x6 false
1233             | x2 ⇒ pair exadecim bool x7 false
1234             | x3 ⇒ pair exadecim bool x8 false
1235             | x4 ⇒ pair exadecim bool x9 false
1236             | x5 ⇒ pair exadecim bool xA false
1237             | x6 ⇒ pair exadecim bool xB false
1238             | x7 ⇒ pair exadecim bool xC false
1239             | x8 ⇒ pair exadecim bool xD false
1240             | x9 ⇒ pair exadecim bool xE false
1241             | xA ⇒ pair exadecim bool xF false
1242             | xB ⇒ pair exadecim bool x0 true
1243             | xC ⇒ pair exadecim bool x1 true
1244             | xD ⇒ pair exadecim bool x2 true
1245             | xE ⇒ pair exadecim bool x3 true
1246             | xF ⇒ pair exadecim bool x4 true ]
1247        | x6 ⇒
1248            match e2 with
1249             [ x0 ⇒ pair exadecim bool x6 false
1250             | x1 ⇒ pair exadecim bool x7 false
1251             | x2 ⇒ pair exadecim bool x8 false
1252             | x3 ⇒ pair exadecim bool x9 false
1253             | x4 ⇒ pair exadecim bool xA false
1254             | x5 ⇒ pair exadecim bool xB false
1255             | x6 ⇒ pair exadecim bool xC false
1256             | x7 ⇒ pair exadecim bool xD false
1257             | x8 ⇒ pair exadecim bool xE false
1258             | x9 ⇒ pair exadecim bool xF false
1259             | xA ⇒ pair exadecim bool x0 true
1260             | xB ⇒ pair exadecim bool x1 true
1261             | xC ⇒ pair exadecim bool x2 true
1262             | xD ⇒ pair exadecim bool x3 true
1263             | xE ⇒ pair exadecim bool x4 true
1264             | xF ⇒ pair exadecim bool x5 true ]
1265        | x7 ⇒
1266            match e2 with
1267             [ x0 ⇒ pair exadecim bool x7 false
1268             | x1 ⇒ pair exadecim bool x8 false
1269             | x2 ⇒ pair exadecim bool x9 false
1270             | x3 ⇒ pair exadecim bool xA false
1271             | x4 ⇒ pair exadecim bool xB false
1272             | x5 ⇒ pair exadecim bool xC false
1273             | x6 ⇒ pair exadecim bool xD false
1274             | x7 ⇒ pair exadecim bool xE false
1275             | x8 ⇒ pair exadecim bool xF false
1276             | x9 ⇒ pair exadecim bool x0 true
1277             | xA ⇒ pair exadecim bool x1 true
1278             | xB ⇒ pair exadecim bool x2 true
1279             | xC ⇒ pair exadecim bool x3 true
1280             | xD ⇒ pair exadecim bool x4 true
1281             | xE ⇒ pair exadecim bool x5 true
1282             | xF ⇒ pair exadecim bool x6 true ]
1283        | x8 ⇒
1284            match e2 with
1285             [ x0 ⇒ pair exadecim bool x8 false
1286             | x1 ⇒ pair exadecim bool x9 false
1287             | x2 ⇒ pair exadecim bool xA false
1288             | x3 ⇒ pair exadecim bool xB false
1289             | x4 ⇒ pair exadecim bool xC false
1290             | x5 ⇒ pair exadecim bool xD false
1291             | x6 ⇒ pair exadecim bool xE false
1292             | x7 ⇒ pair exadecim bool xF false
1293             | x8 ⇒ pair exadecim bool x0 true
1294             | x9 ⇒ pair exadecim bool x1 true
1295             | xA ⇒ pair exadecim bool x2 true
1296             | xB ⇒ pair exadecim bool x3 true
1297             | xC ⇒ pair exadecim bool x4 true
1298             | xD ⇒ pair exadecim bool x5 true
1299             | xE ⇒ pair exadecim bool x6 true
1300             | xF ⇒ pair exadecim bool x7 true ]
1301        | x9 ⇒
1302            match e2 with
1303             [ x0 ⇒ pair exadecim bool x9 false
1304             | x1 ⇒ pair exadecim bool xA false
1305             | x2 ⇒ pair exadecim bool xB false
1306             | x3 ⇒ pair exadecim bool xC false
1307             | x4 ⇒ pair exadecim bool xD false
1308             | x5 ⇒ pair exadecim bool xE false
1309             | x6 ⇒ pair exadecim bool xF false
1310             | x7 ⇒ pair exadecim bool x0 true
1311             | x8 ⇒ pair exadecim bool x1 true
1312             | x9 ⇒ pair exadecim bool x2 true
1313             | xA ⇒ pair exadecim bool x3 true
1314             | xB ⇒ pair exadecim bool x4 true
1315             | xC ⇒ pair exadecim bool x5 true
1316             | xD ⇒ pair exadecim bool x6 true
1317             | xE ⇒ pair exadecim bool x7 true
1318             | xF ⇒ pair exadecim bool x8 true ]
1319        | xA ⇒
1320            match e2 with
1321             [ x0 ⇒ pair exadecim bool xA false
1322             | x1 ⇒ pair exadecim bool xB false
1323             | x2 ⇒ pair exadecim bool xC false
1324             | x3 ⇒ pair exadecim bool xD false
1325             | x4 ⇒ pair exadecim bool xE false
1326             | x5 ⇒ pair exadecim bool xF false
1327             | x6 ⇒ pair exadecim bool x0 true
1328             | x7 ⇒ pair exadecim bool x1 true
1329             | x8 ⇒ pair exadecim bool x2 true
1330             | x9 ⇒ pair exadecim bool x3 true
1331             | xA ⇒ pair exadecim bool x4 true
1332             | xB ⇒ pair exadecim bool x5 true
1333             | xC ⇒ pair exadecim bool x6 true
1334             | xD ⇒ pair exadecim bool x7 true
1335             | xE ⇒ pair exadecim bool x8 true
1336             | xF ⇒ pair exadecim bool x9 true ]
1337        | xB ⇒
1338            match e2 with
1339             [ x0 ⇒ pair exadecim bool xB false
1340             | x1 ⇒ pair exadecim bool xC false
1341             | x2 ⇒ pair exadecim bool xD false
1342             | x3 ⇒ pair exadecim bool xE false
1343             | x4 ⇒ pair exadecim bool xF false
1344             | x5 ⇒ pair exadecim bool x0 true
1345             | x6 ⇒ pair exadecim bool x1 true
1346             | x7 ⇒ pair exadecim bool x2 true
1347             | x8 ⇒ pair exadecim bool x3 true
1348             | x9 ⇒ pair exadecim bool x4 true
1349             | xA ⇒ pair exadecim bool x5 true
1350             | xB ⇒ pair exadecim bool x6 true
1351             | xC ⇒ pair exadecim bool x7 true
1352             | xD ⇒ pair exadecim bool x8 true
1353             | xE ⇒ pair exadecim bool x9 true
1354             | xF ⇒ pair exadecim bool xA true ]
1355        | xC ⇒
1356            match e2 with
1357             [ x0 ⇒ pair exadecim bool xC false
1358             | x1 ⇒ pair exadecim bool xD false
1359             | x2 ⇒ pair exadecim bool xE false
1360             | x3 ⇒ pair exadecim bool xF false
1361             | x4 ⇒ pair exadecim bool x0 true
1362             | x5 ⇒ pair exadecim bool x1 true
1363             | x6 ⇒ pair exadecim bool x2 true
1364             | x7 ⇒ pair exadecim bool x3 true
1365             | x8 ⇒ pair exadecim bool x4 true
1366             | x9 ⇒ pair exadecim bool x5 true
1367             | xA ⇒ pair exadecim bool x6 true
1368             | xB ⇒ pair exadecim bool x7 true
1369             | xC ⇒ pair exadecim bool x8 true
1370             | xD ⇒ pair exadecim bool x9 true
1371             | xE ⇒ pair exadecim bool xA true
1372             | xF ⇒ pair exadecim bool xB true ]
1373        | xD ⇒
1374            match e2 with
1375             [ x0 ⇒ pair exadecim bool xD false
1376             | x1 ⇒ pair exadecim bool xE false
1377             | x2 ⇒ pair exadecim bool xF false
1378             | x3 ⇒ pair exadecim bool x0 true
1379             | x4 ⇒ pair exadecim bool x1 true
1380             | x5 ⇒ pair exadecim bool x2 true
1381             | x6 ⇒ pair exadecim bool x3 true
1382             | x7 ⇒ pair exadecim bool x4 true
1383             | x8 ⇒ pair exadecim bool x5 true
1384             | x9 ⇒ pair exadecim bool x6 true
1385             | xA ⇒ pair exadecim bool x7 true
1386             | xB ⇒ pair exadecim bool x8 true
1387             | xC ⇒ pair exadecim bool x9 true
1388             | xD ⇒ pair exadecim bool xA true
1389             | xE ⇒ pair exadecim bool xB true
1390             | xF ⇒ pair exadecim bool xC true ]
1391        | xE ⇒
1392            match e2 with
1393             [ x0 ⇒ pair exadecim bool xE false
1394             | x1 ⇒ pair exadecim bool xF false
1395             | x2 ⇒ pair exadecim bool x0 true
1396             | x3 ⇒ pair exadecim bool x1 true
1397             | x4 ⇒ pair exadecim bool x2 true
1398             | x5 ⇒ pair exadecim bool x3 true
1399             | x6 ⇒ pair exadecim bool x4 true
1400             | x7 ⇒ pair exadecim bool x5 true
1401             | x8 ⇒ pair exadecim bool x6 true
1402             | x9 ⇒ pair exadecim bool x7 true
1403             | xA ⇒ pair exadecim bool x8 true
1404             | xB ⇒ pair exadecim bool x9 true
1405             | xC ⇒ pair exadecim bool xA true
1406             | xD ⇒ pair exadecim bool xB true
1407             | xE ⇒ pair exadecim bool xC true
1408             | xF ⇒ pair exadecim bool xD true ]
1409        | xF ⇒
1410            match e2 with
1411             [ x0 ⇒ pair exadecim bool xF false
1412             | x1 ⇒ pair exadecim bool x0 true
1413             | x2 ⇒ pair exadecim bool x1 true
1414             | x3 ⇒ pair exadecim bool x2 true
1415             | x4 ⇒ pair exadecim bool x3 true
1416             | x5 ⇒ pair exadecim bool x4 true
1417             | x6 ⇒ pair exadecim bool x5 true
1418             | x7 ⇒ pair exadecim bool x6 true
1419             | x8 ⇒ pair exadecim bool x7 true
1420             | x9 ⇒ pair exadecim bool x8 true
1421             | xA ⇒ pair exadecim bool x9 true
1422             | xB ⇒ pair exadecim bool xA true
1423             | xC ⇒ pair exadecim bool xB true
1424             | xD ⇒ pair exadecim bool xC true
1425             | xE ⇒ pair exadecim bool xD true
1426             | xF ⇒ pair exadecim bool xE true ]
1427        ]
1428    ].
1429
1430 (* operatore somma senza carry *)
1431 definition plus_exnc ≝
1432 λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
1433
1434 (* operatore carry della somma *)
1435 definition plus_exc ≝
1436 λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
1437
1438 (* operatore Most Significant Bit *)
1439 definition MSB_ex ≝
1440 λe:exadecim.match e with
1441  [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1442  | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1443  | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
1444  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ].
1445
1446 (* esadecimali → naturali *)
1447 definition nat_of_exadecim ≝
1448 λe:exadecim.
1449  match e with
1450   [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2  | x3 ⇒ 3  | x4 ⇒ 4  | x5 ⇒ 5  | x6 ⇒ 6  | x7 ⇒ 7
1451   | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
1452
1453 coercion cic:/matita/freescale/exadecim/nat_of_exadecim.con.
1454
1455 (* naturali → esadecimali *)
1456 let rec exadecim_of_nat n ≝
1457  match n with [ O ⇒ x0 | S n ⇒
1458   match n with [ O ⇒ x1 | S n ⇒
1459    match n with [ O ⇒ x2 | S n ⇒
1460     match n with [ O ⇒ x3 | S n ⇒
1461      match n with [ O ⇒ x4 | S n ⇒
1462       match n with [ O ⇒ x5 | S n ⇒
1463        match n with [ O ⇒ x6 | S n ⇒
1464         match n with [ O ⇒ x7 | S n ⇒
1465          match n with [ O ⇒ x8 | S n ⇒
1466           match n with [ O ⇒ x9 | S n ⇒
1467            match n with [ O ⇒ xA | S n ⇒
1468             match n with [ O ⇒ xB | S n ⇒
1469              match n with [ O ⇒ xC | S n ⇒
1470               match n with [ O ⇒ xD | S n ⇒
1471                match n with [ O ⇒ xE | S n ⇒
1472                 match n with [ O ⇒ xF | S n ⇒ exadecim_of_nat n ]]]]]]]]]]]]]]]].
1473
1474 (* operatore predecessore *)
1475 definition pred_ex ≝
1476 λe:exadecim.
1477  match e with
1478   [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1479   | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1480
1481 (* operatore successore *)
1482 definition succ_ex ≝
1483 λe:exadecim.
1484  match e with
1485   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1486   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1487
1488 (* operatore neg/complemento a 2 *)
1489 definition compl_ex ≝
1490 λe:exadecim.match e with
1491  [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1492  | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1493  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1494  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1495
1496 (* iteratore sugli esadecimali *)
1497 definition forall_exadecim ≝ λP.
1498  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1499  P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
1500
1501 (* ********************** *)
1502 (* TEOREMI/LEMMMI/ASSIOMI *)
1503 (* ********************** *)
1504
1505 (* ESPERIMENTO UTILIZZO DELL'ITERATORE *)
1506
1507 (*
1508 lemma forall_exadecim_eqProp_left_aux :
1509  ∀P.(∀e:exadecim.P e = true) →
1510  ((P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1511    P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF) = true).
1512  intros;
1513  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1514  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1515  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1516  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1517  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1518  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1519  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1520  elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1521  reflexivity.
1522 qed.
1523
1524 lemma forall_exadecim_eqProp_left :
1525  ∀P.(∀e:exadecim. P e = true) → (forall_exadecim (λe.P e) = true).
1526  intro;
1527  elim P 0;
1528  [ simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
1529    simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
1530    autobatch; ].
1531 qed.
1532
1533 lemma forall_exadecim_eqProp_right_aux :
1534  ∀P.((P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1535       P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF) = true) →
1536     (∀e:exadecim.P e = true).
1537  elim daemon.
1538 qed.
1539
1540 lemma forall_exadecim_eqProp_right :
1541  ∀P.(forall_exadecim (λe.P e) = true) → (∀e:exadecim.P e = true).
1542  intro;
1543  elim P 0;
1544  [ simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
1545    simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
1546    autobatch; ].
1547 qed.
1548
1549 lemma lt_nat_of_exadecim_16_forall: ∀e.ltb (nat_of_exadecim e) 16 = true.
1550  apply forall_exadecim_eqProp_right;
1551  reflexivity;
1552 qed.
1553 *)
1554
1555 (* FINE DELL'ESPERIMENTO *)
1556
1557 lemma lt_nat_of_exadecim_16: ∀e.nat_of_exadecim e < 16.
1558  intro;
1559  elim e;
1560  simplify;
1561  autobatch depth=17.
1562 qed.
1563
1564 lemma exadecim_of_nat_mod:
1565  ∀n.exadecim_of_nat n = exadecim_of_nat (n \mod 16).
1566  intros;
1567  apply (nat_elim1 n); intro;
1568  cases m; [ intro; reflexivity | ];
1569  cases n1; [ intro; reflexivity | ];
1570  cases n2; [ intro; reflexivity | ];
1571  cases n3; [ intro; reflexivity | ];
1572  cases n4; [ intro; reflexivity | ];
1573  cases n5; [ intro; reflexivity | ];
1574  cases n6; [ intro; reflexivity | ];
1575  cases n7; [ intro; reflexivity | ];
1576  cases n8; [ intro; reflexivity | ];
1577  cases n9; [ intro; reflexivity | ];
1578  cases n10; [ intro; reflexivity | ];
1579  cases n11; [ intro; reflexivity | ];
1580  cases n12; [ intro; reflexivity | ];
1581  cases n13; [ intro; reflexivity | ];
1582  cases n14; [ intro; reflexivity | ];
1583  cases n15; [ intro; reflexivity | ];
1584  intros;
1585  change in ⊢ (? ? % ?) with (exadecim_of_nat n16);
1586  change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
1587  rewrite > mod_plus;
1588  change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
1589  rewrite < mod_mod;
1590   [ apply H;
1591     unfold lt;
1592     autobatch.
1593   | autobatch
1594   ]
1595 qed.
1596
1597 lemma nat_of_exadecim_exadecim_of_nat:
1598  ∀n. nat_of_exadecim (exadecim_of_nat n) = n \mod 16.
1599  intro;
1600  rewrite > exadecim_of_nat_mod;
1601  generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
1602  generalize in match (n \mod 16); intro;
1603  cases n1; [ intro; reflexivity | ];
1604  cases n2; [ intro; reflexivity | ];
1605  cases n3; [ intro; reflexivity | ];
1606  cases n4; [ intro; reflexivity | ];
1607  cases n5; [ intro; reflexivity | ];
1608  cases n6; [ intro; reflexivity | ];
1609  cases n7; [ intro; reflexivity | ];
1610  cases n8; [ intro; reflexivity | ];
1611  cases n9; [ intro; reflexivity | ];
1612  cases n10; [ intro; reflexivity | ];
1613  cases n11 [ intro; reflexivity | ];
1614  cases n12; [ intro; reflexivity | ];
1615  cases n13; [ intro; reflexivity | ];
1616  cases n14; [ intro; reflexivity | ];
1617  cases n15; [ intro; reflexivity | ];
1618  cases n16; [ intro; reflexivity | ];
1619  intro;
1620  unfold lt in H;
1621  cut False;
1622   [ elim Hcut
1623   | autobatch
1624   ]
1625 qed.
1626
1627 lemma exadecim_of_nat_nat_of_exadecim:
1628  ∀e.exadecim_of_nat (nat_of_exadecim e) = e.
1629  intro;
1630  elim e;
1631  reflexivity.
1632 qed.
1633
1634 lemma plusex_ok:
1635  ∀b1,b2,c.
1636   match plus_ex b1 b2 c with
1637    [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
1638  intros;
1639  elim b1; (elim b2; (elim c; normalize; reflexivity)).
1640 qed.
1641
1642 lemma eq_eqex_S_x0_false:
1643  ∀n. n < 15 → eq_ex x0 (exadecim_of_nat (S n)) = false.
1644  intro;
1645  cases n 0; [ intro; simplify; reflexivity | clear n];
1646  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1647  cases n 0; [ intro; simplify; reflexivity | clear n];
1648  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1649  cases n 0; [ intro; simplify; reflexivity | clear n];
1650  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1651  cases n 0; [ intro; simplify; reflexivity | clear n];
1652  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1653  cases n 0; [ intro; simplify; reflexivity | clear n];
1654  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1655  cases n 0; [ intro; simplify; reflexivity | clear n];
1656  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1657  cases n 0; [ intro; simplify; reflexivity | clear n];
1658  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1659  cases n 0; [ intro; simplify; reflexivity | clear n];
1660  intro;
1661  unfold lt in H;
1662  cut (S n1 ≤ 0);
1663   [ elim (not_le_Sn_O ? Hcut)
1664   | do 15 (apply le_S_S_to_le);
1665     assumption
1666   ]
1667 qed.
1668
1669 lemma eqex_true_to_eq: ∀b,b'. eq_ex b b' = true → b=b'.
1670  intros 2;
1671  elim b 0;
1672  elim b' 0;
1673  simplify;
1674  intro;
1675  first [ reflexivity | destruct H ].
1676 qed.
1677
1678 lemma eqex_false_to_not_eq: ∀b,b'. eq_ex b b' = false → b ≠ b'.
1679  intros 2;
1680  elim b 0;
1681  elim b' 0;
1682  simplify;
1683  intro;
1684  try (destruct H);
1685  intro K;
1686  destruct K.
1687 qed.
1688
1689 (* nuovi *)
1690
1691 lemma ok_lt_ex : ∀e1,e2:exadecim.
1692  lt_ex e1 e2 = ltb e1 e2.
1693  intros;
1694  elim e1;
1695  elim e2;
1696  simplify;
1697  reflexivity.
1698  qed.
1699
1700 lemma ok_le_ex : ∀e1,e2:exadecim.
1701  le_ex e1 e2 = leb e1 e2.
1702  intros;
1703  elim e1;
1704  elim e2;
1705  simplify;
1706  reflexivity.
1707  qed.
1708
1709 lemma ok_gt_ex : ∀e1,e2:exadecim.
1710  gt_ex e1 e2 = notb (leb e1 e2).
1711  intros;
1712  elim e1;
1713  elim e2;
1714  simplify;
1715  reflexivity.
1716  qed.
1717
1718 lemma ok_ge_ex : ∀e1,e2:exadecim.
1719  ge_ex e1 e2 = notb (ltb e1 e2).
1720  intros;
1721  elim e1;
1722  elim e2;
1723  simplify;
1724  reflexivity.
1725  qed.
1726
1727 lemma ok_pred_ex : ∀e:exadecim.
1728  pred_ex e = plus_exnc e xF.
1729  intros;
1730  elim e;
1731  simplify;
1732  reflexivity.
1733  qed.
1734
1735 lemma ok_succ_ex : ∀e:exadecim.
1736  succ_ex e = plus_exnc e x1.
1737  intros;
1738  elim e;
1739  simplify;
1740  reflexivity.
1741  qed.
1742
1743 lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
1744  rcr_ex e b =
1745  pair exadecim bool
1746   (exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
1747   (eqb (mod e 2) 1).
1748  intros;
1749  elim e;
1750  elim b;
1751  simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
1752  simplify in ⊢ (? ? ? (? ? ? ? %));
1753  simplify in ⊢ (? ? ? (? ? ? % ?));
1754  simplify in ⊢ (? ? % ?);
1755  reflexivity;
1756 qed.
1757
1758 lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
1759  rcl_ex e b =
1760  pair exadecim bool
1761   (exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
1762   (notb (ltb e 8)).
1763  intros;
1764  elim e;
1765  elim b;
1766  simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
1767  simplify in ⊢ (? ? ? (? ? ? % ?));
1768  simplify in ⊢ (? ? ? (? ? ? ? (? %)));
1769  simplify in ⊢ (? ? ? (? ? ? ? %));
1770  simplify in ⊢ (? ? % ?);
1771  reflexivity.
1772  qed.
1773
1774 lemma ok_shr_ex : ∀e:exadecim.
1775  shr_ex e =
1776  pair exadecim bool
1777   (exadecim_of_nat (e/2))
1778   (eqb (mod e 2) 1).
1779  intros;
1780  elim e;
1781  simplify in ⊢ (? ? ? (? ? ? % ?));
1782  simplify in ⊢ (? ? ? (? ? ? ? %));
1783  simplify in ⊢ (? ? % ?);
1784  reflexivity.
1785 qed.
1786
1787 lemma ok_shl_ex : ∀e:exadecim.
1788  shl_ex e =
1789  pair exadecim bool
1790   (exadecim_of_nat (mod (e*2) 16))
1791   (notb (ltb e 8)).
1792  intros;
1793  elim e;
1794  simplify in ⊢ (? ? ? (? ? ? % ?));
1795  simplify in ⊢ (? ? ? (? ? ? ? (? %)));
1796  simplify in ⊢ (? ? ? (? ? ? ? %));
1797  simplify in ⊢ (? ? % ?);
1798  reflexivity.
1799 qed.
1800
1801 lemma ok_not_ex : ∀e:exadecim.
1802  e + (not_ex e) = 15.
1803  intros;
1804  elim e;
1805  simplify;
1806  reflexivity.
1807 qed.
1808
1809 lemma ok_compl_ex : ∀e:exadecim.
1810  e + (compl_ex e) = match gt_ex e x0 with [ true ⇒ 16 | false ⇒ 0 ].
1811  intros;
1812  elim e;
1813  simplify;
1814  reflexivity.
1815 qed.
1816
1817 lemma ok_MSB_ex : ∀e:exadecim.
1818  MSB_ex e = notb (ltb e 8).
1819  intros;
1820  elim e;
1821  simplify;
1822  reflexivity.
1823 qed.