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