matita/library/assembly/exadecimal.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
  17 include "assembly/extra.ma".
  18
  19 inductive exadecimal : Type ≝
  20    x0: exadecimal
  21  | x1: exadecimal
  22  | x2: exadecimal
  23  | x3: exadecimal
  24  | x4: exadecimal
  25  | x5: exadecimal
  26  | x6: exadecimal
  27  | x7: exadecimal
  28  | x8: exadecimal
  29  | x9: exadecimal
  30  | xA: exadecimal
  31  | xB: exadecimal
  32  | xC: exadecimal
  33  | xD: exadecimal
  34  | xE: exadecimal
  35  | xF: exadecimal.
  36
  37 definition eqex ≝
  38  λb1,b2.
  39   match b1 with
  40    [ x0 ⇒
  41        match b2 with
  42         [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  43         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  44         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  45         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  46    | x1 ⇒
  47        match b2 with
  48         [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
  49         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  50         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  51         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  52    | x2 ⇒
  53        match b2 with
  54         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
  55         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  56         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  57         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  58    | x3 ⇒
  59        match b2 with
  60         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
  61         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  62         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  63         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  64    | x4 ⇒
  65        match b2 with
  66         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  67         | x4 ⇒ true  | 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    | x5 ⇒
  71        match b2 with
  72         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  73         | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
  74         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  75         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  76    | x6 ⇒
  77        match b2 with
  78         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  79         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
  80         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  81         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  82    | x7 ⇒
  83        match b2 with
  84         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  85         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
  86         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  87         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  88    | x8 ⇒
  89        match b2 with
  90         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  91         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  92         | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  93         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  94    | x9 ⇒
  95        match b2 with
  96         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  97         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  98         | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
  99         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 100    | xA ⇒
 101        match b2 with
 102         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 103         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 104         | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 105         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 106    | xB ⇒
 107        match b2 with
 108         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 109         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 110         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 111         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 112    | xC ⇒
 113        match b2 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 ⇒ false
 117         | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 118    | xD ⇒
 119        match b2 with
 120         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 121         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 122         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 123         | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 124    | xE ⇒
 125        match b2 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 ⇒
 131        match b2 with
 132         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 133         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 134         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 135         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]].
 136
 137 definition plusex ≝
 138  λb1,b2,c.
 139   match c with
 140    [ true ⇒
 141       match b1 with
 142        [ x0 ⇒
 143            match b2 with
 144             [ x0 ⇒ couple exadecimal bool x1 false
 145             | x1 ⇒ couple exadecimal bool x2 false
 146             | x2 ⇒ couple exadecimal bool x3 false
 147             | x3 ⇒ couple exadecimal bool x4 false
 148             | x4 ⇒ couple exadecimal bool x5 false
 149             | x5 ⇒ couple exadecimal bool x6 false
 150             | x6 ⇒ couple exadecimal bool x7 false
 151             | x7 ⇒ couple exadecimal bool x8 false
 152             | x8 ⇒ couple exadecimal bool x9 false
 153             | x9 ⇒ couple exadecimal bool xA false
 154             | xA ⇒ couple exadecimal bool xB false
 155             | xB ⇒ couple exadecimal bool xC false
 156             | xC ⇒ couple exadecimal bool xD false
 157             | xD ⇒ couple exadecimal bool xE false
 158             | xE ⇒ couple exadecimal bool xF false
 159             | xF ⇒ couple exadecimal bool x0 true ]
 160        | x1 ⇒
 161            match b2 with
 162             [ x0 ⇒ couple exadecimal bool x2 false
 163             | x1 ⇒ couple exadecimal bool x3 false
 164             | x2 ⇒ couple exadecimal bool x4 false
 165             | x3 ⇒ couple exadecimal bool x5 false
 166             | x4 ⇒ couple exadecimal bool x6 false
 167             | x5 ⇒ couple exadecimal bool x7 false
 168             | x6 ⇒ couple exadecimal bool x8 false
 169             | x7 ⇒ couple exadecimal bool x9 false
 170             | x8 ⇒ couple exadecimal bool xA false
 171             | x9 ⇒ couple exadecimal bool xB false
 172             | xA ⇒ couple exadecimal bool xC false
 173             | xB ⇒ couple exadecimal bool xD false
 174             | xC ⇒ couple exadecimal bool xE false
 175             | xD ⇒ couple exadecimal bool xF false
 176             | xE ⇒ couple exadecimal bool x0 true
 177             | xF ⇒ couple exadecimal bool x1 true ]
 178        | x2 ⇒
 179            match b2 with
 180             [ x0 ⇒ couple exadecimal bool x3 false
 181             | x1 ⇒ couple exadecimal bool x4 false
 182             | x2 ⇒ couple exadecimal bool x5 false
 183             | x3 ⇒ couple exadecimal bool x6 false
 184             | x4 ⇒ couple exadecimal bool x7 false
 185             | x5 ⇒ couple exadecimal bool x8 false
 186             | x6 ⇒ couple exadecimal bool x9 false
 187             | x7 ⇒ couple exadecimal bool xA false
 188             | x8 ⇒ couple exadecimal bool xB false
 189             | x9 ⇒ couple exadecimal bool xC false
 190             | xA ⇒ couple exadecimal bool xD false
 191             | xB ⇒ couple exadecimal bool xE false
 192             | xC ⇒ couple exadecimal bool xF false
 193             | xD ⇒ couple exadecimal bool x0 true
 194             | xE ⇒ couple exadecimal bool x1 true
 195             | xF ⇒ couple exadecimal bool x2 true ]
 196        | x3 ⇒
 197            match b2 with
 198             [ x0 ⇒ couple exadecimal bool x4 false
 199             | x1 ⇒ couple exadecimal bool x5 false
 200             | x2 ⇒ couple exadecimal bool x6 false
 201             | x3 ⇒ couple exadecimal bool x7 false
 202             | x4 ⇒ couple exadecimal bool x8 false
 203             | x5 ⇒ couple exadecimal bool x9 false
 204             | x6 ⇒ couple exadecimal bool xA false
 205             | x7 ⇒ couple exadecimal bool xB false
 206             | x8 ⇒ couple exadecimal bool xC false
 207             | x9 ⇒ couple exadecimal bool xD false
 208             | xA ⇒ couple exadecimal bool xE false
 209             | xB ⇒ couple exadecimal bool xF false
 210             | xC ⇒ couple exadecimal bool x0 true
 211             | xD ⇒ couple exadecimal bool x1 true
 212             | xE ⇒ couple exadecimal bool x2 true
 213             | xF ⇒ couple exadecimal bool x3 true ]
 214        | x4 ⇒
 215            match b2 with
 216             [ x0 ⇒ couple exadecimal bool x5 false
 217             | x1 ⇒ couple exadecimal bool x6 false
 218             | x2 ⇒ couple exadecimal bool x7 false
 219             | x3 ⇒ couple exadecimal bool x8 false
 220             | x4 ⇒ couple exadecimal bool x9 false
 221             | x5 ⇒ couple exadecimal bool xA false
 222             | x6 ⇒ couple exadecimal bool xB false
 223             | x7 ⇒ couple exadecimal bool xC false
 224             | x8 ⇒ couple exadecimal bool xD false
 225             | x9 ⇒ couple exadecimal bool xE false
 226             | xA ⇒ couple exadecimal bool xF false
 227             | xB ⇒ couple exadecimal bool x0 true
 228             | xC ⇒ couple exadecimal bool x1 true
 229             | xD ⇒ couple exadecimal bool x2 true
 230             | xE ⇒ couple exadecimal bool x3 true
 231             | xF ⇒ couple exadecimal bool x4 true ]
 232        | x5 ⇒
 233            match b2 with
 234             [ x0 ⇒ couple exadecimal bool x6 false
 235             | x1 ⇒ couple exadecimal bool x7 false
 236             | x2 ⇒ couple exadecimal bool x8 false
 237             | x3 ⇒ couple exadecimal bool x9 false
 238             | x4 ⇒ couple exadecimal bool xA false
 239             | x5 ⇒ couple exadecimal bool xB false
 240             | x6 ⇒ couple exadecimal bool xC false
 241             | x7 ⇒ couple exadecimal bool xD false
 242             | x8 ⇒ couple exadecimal bool xE false
 243             | x9 ⇒ couple exadecimal bool xF false
 244             | xA ⇒ couple exadecimal bool x0 true
 245             | xB ⇒ couple exadecimal bool x1 true
 246             | xC ⇒ couple exadecimal bool x2 true
 247             | xD ⇒ couple exadecimal bool x3 true
 248             | xE ⇒ couple exadecimal bool x4 true
 249             | xF ⇒ couple exadecimal bool x5 true ]
 250        | x6 ⇒
 251            match b2 with
 252             [ x0 ⇒ couple exadecimal bool x7 false
 253             | x1 ⇒ couple exadecimal bool x8 false
 254             | x2 ⇒ couple exadecimal bool x9 false
 255             | x3 ⇒ couple exadecimal bool xA false
 256             | x4 ⇒ couple exadecimal bool xB false
 257             | x5 ⇒ couple exadecimal bool xC false
 258             | x6 ⇒ couple exadecimal bool xD false
 259             | x7 ⇒ couple exadecimal bool xE false
 260             | x8 ⇒ couple exadecimal bool xF false
 261             | x9 ⇒ couple exadecimal bool x0 true
 262             | xA ⇒ couple exadecimal bool x1 true
 263             | xB ⇒ couple exadecimal bool x2 true
 264             | xC ⇒ couple exadecimal bool x3 true
 265             | xD ⇒ couple exadecimal bool x4 true
 266             | xE ⇒ couple exadecimal bool x5 true
 267             | xF ⇒ couple exadecimal bool x6 true ]
 268        | x7 ⇒
 269            match b2 with
 270             [ x0 ⇒ couple exadecimal bool x8 false
 271             | x1 ⇒ couple exadecimal bool x9 false
 272             | x2 ⇒ couple exadecimal bool xA false
 273             | x3 ⇒ couple exadecimal bool xB false
 274             | x4 ⇒ couple exadecimal bool xC false
 275             | x5 ⇒ couple exadecimal bool xD false
 276             | x6 ⇒ couple exadecimal bool xE false
 277             | x7 ⇒ couple exadecimal bool xF false
 278             | x8 ⇒ couple exadecimal bool x0 true
 279             | x9 ⇒ couple exadecimal bool x1 true
 280             | xA ⇒ couple exadecimal bool x2 true
 281             | xB ⇒ couple exadecimal bool x3 true
 282             | xC ⇒ couple exadecimal bool x4 true
 283             | xD ⇒ couple exadecimal bool x5 true
 284             | xE ⇒ couple exadecimal bool x6 true
 285             | xF ⇒ couple exadecimal bool x7 true ]
 286        | x8 ⇒
 287            match b2 with
 288             [ x0 ⇒ couple exadecimal bool x9 false
 289             | x1 ⇒ couple exadecimal bool xA false
 290             | x2 ⇒ couple exadecimal bool xB false
 291             | x3 ⇒ couple exadecimal bool xC false
 292             | x4 ⇒ couple exadecimal bool xD false
 293             | x5 ⇒ couple exadecimal bool xE false
 294             | x6 ⇒ couple exadecimal bool xF false
 295             | x7 ⇒ couple exadecimal bool x0 true
 296             | x8 ⇒ couple exadecimal bool x1 true
 297             | x9 ⇒ couple exadecimal bool x2 true
 298             | xA ⇒ couple exadecimal bool x3 true
 299             | xB ⇒ couple exadecimal bool x4 true
 300             | xC ⇒ couple exadecimal bool x5 true
 301             | xD ⇒ couple exadecimal bool x6 true
 302             | xE ⇒ couple exadecimal bool x7 true
 303             | xF ⇒ couple exadecimal bool x8 true ]
 304        | x9 ⇒
 305            match b2 with
 306             [ x0 ⇒ couple exadecimal bool xA false
 307             | x1 ⇒ couple exadecimal bool xB false
 308             | x2 ⇒ couple exadecimal bool xC false
 309             | x3 ⇒ couple exadecimal bool xD false
 310             | x4 ⇒ couple exadecimal bool xE false
 311             | x5 ⇒ couple exadecimal bool xF false
 312             | x6 ⇒ couple exadecimal bool x0 true
 313             | x7 ⇒ couple exadecimal bool x1 true
 314             | x8 ⇒ couple exadecimal bool x2 true
 315             | x9 ⇒ couple exadecimal bool x3 true
 316             | xA ⇒ couple exadecimal bool x4 true
 317             | xB ⇒ couple exadecimal bool x5 true
 318             | xC ⇒ couple exadecimal bool x6 true
 319             | xD ⇒ couple exadecimal bool x7 true
 320             | xE ⇒ couple exadecimal bool x8 true
 321             | xF ⇒ couple exadecimal bool x9 true ]
 322        | xA ⇒
 323            match b2 with
 324             [ x0 ⇒ couple exadecimal bool xB false
 325             | x1 ⇒ couple exadecimal bool xC false
 326             | x2 ⇒ couple exadecimal bool xD false
 327             | x3 ⇒ couple exadecimal bool xE false
 328             | x4 ⇒ couple exadecimal bool xF false
 329             | x5 ⇒ couple exadecimal bool x0 true
 330             | x6 ⇒ couple exadecimal bool x1 true
 331             | x7 ⇒ couple exadecimal bool x2 true
 332             | x8 ⇒ couple exadecimal bool x3 true
 333             | x9 ⇒ couple exadecimal bool x4 true
 334             | xA ⇒ couple exadecimal bool x5 true
 335             | xB ⇒ couple exadecimal bool x6 true
 336             | xC ⇒ couple exadecimal bool x7 true
 337             | xD ⇒ couple exadecimal bool x8 true
 338             | xE ⇒ couple exadecimal bool x9 true
 339             | xF ⇒ couple exadecimal bool xA true ]
 340        | xB ⇒
 341            match b2 with
 342             [ x0 ⇒ couple exadecimal bool xC false
 343             | x1 ⇒ couple exadecimal bool xD false
 344             | x2 ⇒ couple exadecimal bool xE false
 345             | x3 ⇒ couple exadecimal bool xF false
 346             | x4 ⇒ couple exadecimal bool x0 true
 347             | x5 ⇒ couple exadecimal bool x1 true
 348             | x6 ⇒ couple exadecimal bool x2 true
 349             | x7 ⇒ couple exadecimal bool x3 true
 350             | x8 ⇒ couple exadecimal bool x4 true
 351             | x9 ⇒ couple exadecimal bool x5 true
 352             | xA ⇒ couple exadecimal bool x6 true
 353             | xB ⇒ couple exadecimal bool x7 true
 354             | xC ⇒ couple exadecimal bool x8 true
 355             | xD ⇒ couple exadecimal bool x9 true
 356             | xE ⇒ couple exadecimal bool xA true
 357             | xF ⇒ couple exadecimal bool xB true ]
 358        | xC ⇒
 359            match b2 with
 360             [ x0 ⇒ couple exadecimal bool xD false
 361             | x1 ⇒ couple exadecimal bool xE false
 362             | x2 ⇒ couple exadecimal bool xF false
 363             | x3 ⇒ couple exadecimal bool x0 true
 364             | x4 ⇒ couple exadecimal bool x1 true
 365             | x5 ⇒ couple exadecimal bool x2 true
 366             | x6 ⇒ couple exadecimal bool x3 true
 367             | x7 ⇒ couple exadecimal bool x4 true
 368             | x8 ⇒ couple exadecimal bool x5 true
 369             | x9 ⇒ couple exadecimal bool x6 true
 370             | xA ⇒ couple exadecimal bool x7 true
 371             | xB ⇒ couple exadecimal bool x8 true
 372             | xC ⇒ couple exadecimal bool x9 true
 373             | xD ⇒ couple exadecimal bool xA true
 374             | xE ⇒ couple exadecimal bool xB true
 375             | xF ⇒ couple exadecimal bool xC true ]
 376        | xD ⇒
 377            match b2 with
 378             [ x0 ⇒ couple exadecimal bool xE false
 379             | x1 ⇒ couple exadecimal bool xF false
 380             | x2 ⇒ couple exadecimal bool x0 true
 381             | x3 ⇒ couple exadecimal bool x1 true
 382             | x4 ⇒ couple exadecimal bool x2 true
 383             | x5 ⇒ couple exadecimal bool x3 true
 384             | x6 ⇒ couple exadecimal bool x4 true
 385             | x7 ⇒ couple exadecimal bool x5 true
 386             | x8 ⇒ couple exadecimal bool x6 true
 387             | x9 ⇒ couple exadecimal bool x7 true
 388             | xA ⇒ couple exadecimal bool x8 true
 389             | xB ⇒ couple exadecimal bool x9 true
 390             | xC ⇒ couple exadecimal bool xA true
 391             | xD ⇒ couple exadecimal bool xB true
 392             | xE ⇒ couple exadecimal bool xC true
 393             | xF ⇒ couple exadecimal bool xD true ]
 394        | xE ⇒
 395            match b2 with
 396             [ x0 ⇒ couple exadecimal bool xF false
 397             | x1 ⇒ couple exadecimal bool x0 true
 398             | x2 ⇒ couple exadecimal bool x1 true
 399             | x3 ⇒ couple exadecimal bool x2 true
 400             | x4 ⇒ couple exadecimal bool x3 true
 401             | x5 ⇒ couple exadecimal bool x4 true
 402             | x6 ⇒ couple exadecimal bool x5 true
 403             | x7 ⇒ couple exadecimal bool x6 true
 404             | x8 ⇒ couple exadecimal bool x7 true
 405             | x9 ⇒ couple exadecimal bool x8 true
 406             | xA ⇒ couple exadecimal bool x9 true
 407             | xB ⇒ couple exadecimal bool xA true
 408             | xC ⇒ couple exadecimal bool xB true
 409             | xD ⇒ couple exadecimal bool xC true
 410             | xE ⇒ couple exadecimal bool xD true
 411             | xF ⇒ couple exadecimal bool xE true ]
 412        | xF ⇒
 413            match b2 with
 414             [ x0 ⇒ couple exadecimal bool x0 true
 415             | x1 ⇒ couple exadecimal bool x1 true
 416             | x2 ⇒ couple exadecimal bool x2 true
 417             | x3 ⇒ couple exadecimal bool x3 true
 418             | x4 ⇒ couple exadecimal bool x4 true
 419             | x5 ⇒ couple exadecimal bool x5 true
 420             | x6 ⇒ couple exadecimal bool x6 true
 421             | x7 ⇒ couple exadecimal bool x7 true
 422             | x8 ⇒ couple exadecimal bool x8 true
 423             | x9 ⇒ couple exadecimal bool x9 true
 424             | xA ⇒ couple exadecimal bool xA true
 425             | xB ⇒ couple exadecimal bool xB true
 426             | xC ⇒ couple exadecimal bool xC true
 427             | xD ⇒ couple exadecimal bool xD true
 428             | xE ⇒ couple exadecimal bool xE true
 429             | xF ⇒ couple exadecimal bool xF true ]
 430        ]
 431    | false ⇒
 432       match b1 with
 433        [ x0 ⇒
 434            match b2 with
 435             [ x0 ⇒ couple exadecimal bool x0 false
 436             | x1 ⇒ couple exadecimal bool x1 false
 437             | x2 ⇒ couple exadecimal bool x2 false
 438             | x3 ⇒ couple exadecimal bool x3 false
 439             | x4 ⇒ couple exadecimal bool x4 false
 440             | x5 ⇒ couple exadecimal bool x5 false
 441             | x6 ⇒ couple exadecimal bool x6 false
 442             | x7 ⇒ couple exadecimal bool x7 false
 443             | x8 ⇒ couple exadecimal bool x8 false
 444             | x9 ⇒ couple exadecimal bool x9 false
 445             | xA ⇒ couple exadecimal bool xA false
 446             | xB ⇒ couple exadecimal bool xB false
 447             | xC ⇒ couple exadecimal bool xC false
 448             | xD ⇒ couple exadecimal bool xD false
 449             | xE ⇒ couple exadecimal bool xE false
 450             | xF ⇒ couple exadecimal bool xF false ]
 451        | x1 ⇒
 452            match b2 with
 453             [ x0 ⇒ couple exadecimal bool x1 false
 454             | x1 ⇒ couple exadecimal bool x2 false
 455             | x2 ⇒ couple exadecimal bool x3 false
 456             | x3 ⇒ couple exadecimal bool x4 false
 457             | x4 ⇒ couple exadecimal bool x5 false
 458             | x5 ⇒ couple exadecimal bool x6 false
 459             | x6 ⇒ couple exadecimal bool x7 false
 460             | x7 ⇒ couple exadecimal bool x8 false
 461             | x8 ⇒ couple exadecimal bool x9 false
 462             | x9 ⇒ couple exadecimal bool xA false
 463             | xA ⇒ couple exadecimal bool xB false
 464             | xB ⇒ couple exadecimal bool xC false
 465             | xC ⇒ couple exadecimal bool xD false
 466             | xD ⇒ couple exadecimal bool xE false
 467             | xE ⇒ couple exadecimal bool xF false
 468             | xF ⇒ couple exadecimal bool x0 true ]
 469        | x2 ⇒
 470            match b2 with
 471             [ x0 ⇒ couple exadecimal bool x2 false
 472             | x1 ⇒ couple exadecimal bool x3 false
 473             | x2 ⇒ couple exadecimal bool x4 false
 474             | x3 ⇒ couple exadecimal bool x5 false
 475             | x4 ⇒ couple exadecimal bool x6 false
 476             | x5 ⇒ couple exadecimal bool x7 false
 477             | x6 ⇒ couple exadecimal bool x8 false
 478             | x7 ⇒ couple exadecimal bool x9 false
 479             | x8 ⇒ couple exadecimal bool xA false
 480             | x9 ⇒ couple exadecimal bool xB false
 481             | xA ⇒ couple exadecimal bool xC false
 482             | xB ⇒ couple exadecimal bool xD false
 483             | xC ⇒ couple exadecimal bool xE false
 484             | xD ⇒ couple exadecimal bool xF false
 485             | xE ⇒ couple exadecimal bool x0 true
 486             | xF ⇒ couple exadecimal bool x1 true ]
 487        | x3 ⇒
 488            match b2 with
 489             [ x0 ⇒ couple exadecimal bool x3 false
 490             | x1 ⇒ couple exadecimal bool x4 false
 491             | x2 ⇒ couple exadecimal bool x5 false
 492             | x3 ⇒ couple exadecimal bool x6 false
 493             | x4 ⇒ couple exadecimal bool x7 false
 494             | x5 ⇒ couple exadecimal bool x8 false
 495             | x6 ⇒ couple exadecimal bool x9 false
 496             | x7 ⇒ couple exadecimal bool xA false
 497             | x8 ⇒ couple exadecimal bool xB false
 498             | x9 ⇒ couple exadecimal bool xC false
 499             | xA ⇒ couple exadecimal bool xD false
 500             | xB ⇒ couple exadecimal bool xE false
 501             | xC ⇒ couple exadecimal bool xF false
 502             | xD ⇒ couple exadecimal bool x0 true
 503             | xE ⇒ couple exadecimal bool x1 true
 504             | xF ⇒ couple exadecimal bool x2 true ]
 505        | x4 ⇒
 506            match b2 with
 507             [ x0 ⇒ couple exadecimal bool x4 false
 508             | x1 ⇒ couple exadecimal bool x5 false
 509             | x2 ⇒ couple exadecimal bool x6 false
 510             | x3 ⇒ couple exadecimal bool x7 false
 511             | x4 ⇒ couple exadecimal bool x8 false
 512             | x5 ⇒ couple exadecimal bool x9 false
 513             | x6 ⇒ couple exadecimal bool xA false
 514             | x7 ⇒ couple exadecimal bool xB false
 515             | x8 ⇒ couple exadecimal bool xC false
 516             | x9 ⇒ couple exadecimal bool xD false
 517             | xA ⇒ couple exadecimal bool xE false
 518             | xB ⇒ couple exadecimal bool xF false
 519             | xC ⇒ couple exadecimal bool x0 true
 520             | xD ⇒ couple exadecimal bool x1 true
 521             | xE ⇒ couple exadecimal bool x2 true
 522             | xF ⇒ couple exadecimal bool x3 true ]
 523        | x5 ⇒
 524            match b2 with
 525             [ x0 ⇒ couple exadecimal bool x5 false
 526             | x1 ⇒ couple exadecimal bool x6 false
 527             | x2 ⇒ couple exadecimal bool x7 false
 528             | x3 ⇒ couple exadecimal bool x8 false
 529             | x4 ⇒ couple exadecimal bool x9 false
 530             | x5 ⇒ couple exadecimal bool xA false
 531             | x6 ⇒ couple exadecimal bool xB false
 532             | x7 ⇒ couple exadecimal bool xC false
 533             | x8 ⇒ couple exadecimal bool xD false
 534             | x9 ⇒ couple exadecimal bool xE false
 535             | xA ⇒ couple exadecimal bool xF false
 536             | xB ⇒ couple exadecimal bool x0 true
 537             | xC ⇒ couple exadecimal bool x1 true
 538             | xD ⇒ couple exadecimal bool x2 true
 539             | xE ⇒ couple exadecimal bool x3 true
 540             | xF ⇒ couple exadecimal bool x4 true ]
 541        | x6 ⇒
 542            match b2 with
 543             [ x0 ⇒ couple exadecimal bool x6 false
 544             | x1 ⇒ couple exadecimal bool x7 false
 545             | x2 ⇒ couple exadecimal bool x8 false
 546             | x3 ⇒ couple exadecimal bool x9 false
 547             | x4 ⇒ couple exadecimal bool xA false
 548             | x5 ⇒ couple exadecimal bool xB false
 549             | x6 ⇒ couple exadecimal bool xC false
 550             | x7 ⇒ couple exadecimal bool xD false
 551             | x8 ⇒ couple exadecimal bool xE false
 552             | x9 ⇒ couple exadecimal bool xF false
 553             | xA ⇒ couple exadecimal bool x0 true
 554             | xB ⇒ couple exadecimal bool x1 true
 555             | xC ⇒ couple exadecimal bool x2 true
 556             | xD ⇒ couple exadecimal bool x3 true
 557             | xE ⇒ couple exadecimal bool x4 true
 558             | xF ⇒ couple exadecimal bool x5 true ]
 559        | x7 ⇒
 560            match b2 with
 561             [ x0 ⇒ couple exadecimal bool x7 false
 562             | x1 ⇒ couple exadecimal bool x8 false
 563             | x2 ⇒ couple exadecimal bool x9 false
 564             | x3 ⇒ couple exadecimal bool xA false
 565             | x4 ⇒ couple exadecimal bool xB false
 566             | x5 ⇒ couple exadecimal bool xC false
 567             | x6 ⇒ couple exadecimal bool xD false
 568             | x7 ⇒ couple exadecimal bool xE false
 569             | x8 ⇒ couple exadecimal bool xF false
 570             | x9 ⇒ couple exadecimal bool x0 true
 571             | xA ⇒ couple exadecimal bool x1 true
 572             | xB ⇒ couple exadecimal bool x2 true
 573             | xC ⇒ couple exadecimal bool x3 true
 574             | xD ⇒ couple exadecimal bool x4 true
 575             | xE ⇒ couple exadecimal bool x5 true
 576             | xF ⇒ couple exadecimal bool x6 true ]
 577        | x8 ⇒
 578            match b2 with
 579             [ x0 ⇒ couple exadecimal bool x8 false
 580             | x1 ⇒ couple exadecimal bool x9 false
 581             | x2 ⇒ couple exadecimal bool xA false
 582             | x3 ⇒ couple exadecimal bool xB false
 583             | x4 ⇒ couple exadecimal bool xC false
 584             | x5 ⇒ couple exadecimal bool xD false
 585             | x6 ⇒ couple exadecimal bool xE false
 586             | x7 ⇒ couple exadecimal bool xF false
 587             | x8 ⇒ couple exadecimal bool x0 true
 588             | x9 ⇒ couple exadecimal bool x1 true
 589             | xA ⇒ couple exadecimal bool x2 true
 590             | xB ⇒ couple exadecimal bool x3 true
 591             | xC ⇒ couple exadecimal bool x4 true
 592             | xD ⇒ couple exadecimal bool x5 true
 593             | xE ⇒ couple exadecimal bool x6 true
 594             | xF ⇒ couple exadecimal bool x7 true ]
 595        | x9 ⇒
 596            match b2 with
 597             [ x0 ⇒ couple exadecimal bool x9 false
 598             | x1 ⇒ couple exadecimal bool xA false
 599             | x2 ⇒ couple exadecimal bool xB false
 600             | x3 ⇒ couple exadecimal bool xC false
 601             | x4 ⇒ couple exadecimal bool xD false
 602             | x5 ⇒ couple exadecimal bool xE false
 603             | x6 ⇒ couple exadecimal bool xF false
 604             | x7 ⇒ couple exadecimal bool x0 true
 605             | x8 ⇒ couple exadecimal bool x1 true
 606             | x9 ⇒ couple exadecimal bool x2 true
 607             | xA ⇒ couple exadecimal bool x3 true
 608             | xB ⇒ couple exadecimal bool x4 true
 609             | xC ⇒ couple exadecimal bool x5 true
 610             | xD ⇒ couple exadecimal bool x6 true
 611             | xE ⇒ couple exadecimal bool x7 true
 612             | xF ⇒ couple exadecimal bool x8 true ]
 613        | xA ⇒
 614            match b2 with
 615             [ x0 ⇒ couple exadecimal bool xA false
 616             | x1 ⇒ couple exadecimal bool xB false
 617             | x2 ⇒ couple exadecimal bool xC false
 618             | x3 ⇒ couple exadecimal bool xD false
 619             | x4 ⇒ couple exadecimal bool xE false
 620             | x5 ⇒ couple exadecimal bool xF false
 621             | x6 ⇒ couple exadecimal bool x0 true
 622             | x7 ⇒ couple exadecimal bool x1 true
 623             | x8 ⇒ couple exadecimal bool x2 true
 624             | x9 ⇒ couple exadecimal bool x3 true
 625             | xA ⇒ couple exadecimal bool x4 true
 626             | xB ⇒ couple exadecimal bool x5 true
 627             | xC ⇒ couple exadecimal bool x6 true
 628             | xD ⇒ couple exadecimal bool x7 true
 629             | xE ⇒ couple exadecimal bool x8 true
 630             | xF ⇒ couple exadecimal bool x9 true ]
 631        | xB ⇒
 632            match b2 with
 633             [ x0 ⇒ couple exadecimal bool xB false
 634             | x1 ⇒ couple exadecimal bool xC false
 635             | x2 ⇒ couple exadecimal bool xD false
 636             | x3 ⇒ couple exadecimal bool xE false
 637             | x4 ⇒ couple exadecimal bool xF false
 638             | x5 ⇒ couple exadecimal bool x0 true
 639             | x6 ⇒ couple exadecimal bool x1 true
 640             | x7 ⇒ couple exadecimal bool x2 true
 641             | x8 ⇒ couple exadecimal bool x3 true
 642             | x9 ⇒ couple exadecimal bool x4 true
 643             | xA ⇒ couple exadecimal bool x5 true
 644             | xB ⇒ couple exadecimal bool x6 true
 645             | xC ⇒ couple exadecimal bool x7 true
 646             | xD ⇒ couple exadecimal bool x8 true
 647             | xE ⇒ couple exadecimal bool x9 true
 648             | xF ⇒ couple exadecimal bool xA true ]
 649        | xC ⇒
 650            match b2 with
 651             [ x0 ⇒ couple exadecimal bool xC false
 652             | x1 ⇒ couple exadecimal bool xD false
 653             | x2 ⇒ couple exadecimal bool xE false
 654             | x3 ⇒ couple exadecimal bool xF false
 655             | x4 ⇒ couple exadecimal bool x0 true
 656             | x5 ⇒ couple exadecimal bool x1 true
 657             | x6 ⇒ couple exadecimal bool x2 true
 658             | x7 ⇒ couple exadecimal bool x3 true
 659             | x8 ⇒ couple exadecimal bool x4 true
 660             | x9 ⇒ couple exadecimal bool x5 true
 661             | xA ⇒ couple exadecimal bool x6 true
 662             | xB ⇒ couple exadecimal bool x7 true
 663             | xC ⇒ couple exadecimal bool x8 true
 664             | xD ⇒ couple exadecimal bool x9 true
 665             | xE ⇒ couple exadecimal bool xA true
 666             | xF ⇒ couple exadecimal bool xB true ]
 667        | xD ⇒
 668            match b2 with
 669             [ x0 ⇒ couple exadecimal bool xD false
 670             | x1 ⇒ couple exadecimal bool xE false
 671             | x2 ⇒ couple exadecimal bool xF false
 672             | x3 ⇒ couple exadecimal bool x0 true
 673             | x4 ⇒ couple exadecimal bool x1 true
 674             | x5 ⇒ couple exadecimal bool x2 true
 675             | x6 ⇒ couple exadecimal bool x3 true
 676             | x7 ⇒ couple exadecimal bool x4 true
 677             | x8 ⇒ couple exadecimal bool x5 true
 678             | x9 ⇒ couple exadecimal bool x6 true
 679             | xA ⇒ couple exadecimal bool x7 true
 680             | xB ⇒ couple exadecimal bool x8 true
 681             | xC ⇒ couple exadecimal bool x9 true
 682             | xD ⇒ couple exadecimal bool xA true
 683             | xE ⇒ couple exadecimal bool xB true
 684             | xF ⇒ couple exadecimal bool xC true ]
 685        | xE ⇒
 686            match b2 with
 687             [ x0 ⇒ couple exadecimal bool xE false
 688             | x1 ⇒ couple exadecimal bool xF false
 689             | x2 ⇒ couple exadecimal bool x0 true
 690             | x3 ⇒ couple exadecimal bool x1 true
 691             | x4 ⇒ couple exadecimal bool x2 true
 692             | x5 ⇒ couple exadecimal bool x3 true
 693             | x6 ⇒ couple exadecimal bool x4 true
 694             | x7 ⇒ couple exadecimal bool x5 true
 695             | x8 ⇒ couple exadecimal bool x6 true
 696             | x9 ⇒ couple exadecimal bool x7 true
 697             | xA ⇒ couple exadecimal bool x8 true
 698             | xB ⇒ couple exadecimal bool x9 true
 699             | xC ⇒ couple exadecimal bool xA true
 700             | xD ⇒ couple exadecimal bool xB true
 701             | xE ⇒ couple exadecimal bool xC true
 702             | xF ⇒ couple exadecimal bool xD true ]
 703        | xF ⇒
 704            match b2 with
 705             [ x0 ⇒ couple exadecimal bool xF false
 706             | x1 ⇒ couple exadecimal bool x0 true
 707             | x2 ⇒ couple exadecimal bool x1 true
 708             | x3 ⇒ couple exadecimal bool x2 true
 709             | x4 ⇒ couple exadecimal bool x3 true
 710             | x5 ⇒ couple exadecimal bool x4 true
 711             | x6 ⇒ couple exadecimal bool x5 true
 712             | x7 ⇒ couple exadecimal bool x6 true
 713             | x8 ⇒ couple exadecimal bool x7 true
 714             | x9 ⇒ couple exadecimal bool x8 true
 715             | xA ⇒ couple exadecimal bool x9 true
 716             | xB ⇒ couple exadecimal bool xA true
 717             | xC ⇒ couple exadecimal bool xB true
 718             | xD ⇒ couple exadecimal bool xC true
 719             | xE ⇒ couple exadecimal bool xD true
 720             | xF ⇒ couple exadecimal bool xE true ]
 721        ]
 722    ]
 723 .
 724
 725 definition nat_of_exadecimal ≝
 726  λb.
 727   match b with
 728    [ x0 ⇒ 0
 729    | x1 ⇒ 1
 730    | x2 ⇒ 2
 731    | x3 ⇒ 3
 732    | x4 ⇒ 4
 733    | x5 ⇒ 5
 734    | x6 ⇒ 6
 735    | x7 ⇒ 7
 736    | x8 ⇒ 8
 737    | x9 ⇒ 9
 738    | xA ⇒ 10
 739    | xB ⇒ 11
 740    | xC ⇒ 12
 741    | xD ⇒ 13
 742    | xE ⇒ 14
 743    | xF ⇒ 15
 744    ].
 745
 746 coercion cic:/matita/assembly/exadecimal/nat_of_exadecimal.con.
 747
 748 let rec exadecimal_of_nat b ≝
 749   match b with [ O ⇒ x0 | S b ⇒
 750   match b with [ O ⇒ x1 | S b ⇒
 751   match b with [ O ⇒ x2 | S b ⇒
 752   match b with [ O ⇒ x3 | S b ⇒
 753   match b with [ O ⇒ x4 | S b ⇒
 754   match b with [ O ⇒ x5 | S b ⇒
 755   match b with [ O ⇒ x6 | S b ⇒
 756   match b with [ O ⇒ x7 | S b ⇒
 757   match b with [ O ⇒ x8 | S b ⇒
 758   match b with [ O ⇒ x9 | S b ⇒
 759   match b with [ O ⇒ xA | S b ⇒
 760   match b with [ O ⇒ xB | S b ⇒
 761   match b with [ O ⇒ xC | S b ⇒
 762   match b with [ O ⇒ xD | S b ⇒
 763   match b with [ O ⇒ xE | S b ⇒
 764   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
 765
 766 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
 767  intro;
 768  elim b;
 769  simplify;
 770  [
 771  |*: repeat (apply lt_to_lt_S_S)
 772  ];
 773  autobatch.
 774 qed.
 775
 776 lemma exadecimal_of_nat_mod:
 777  ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
 778  intros;
 779  apply (nat_elim1 n); intro;
 780  cases m; [ intro; reflexivity | ];
 781  cases n1; [ intro; reflexivity | ];
 782  cases n2; [ intro; reflexivity | ];
 783  cases n3; [ intro; reflexivity | ];
 784  cases n4; [ intro; reflexivity | ];
 785  cases n5; [ intro; reflexivity | ];
 786  cases n6; [ intro; reflexivity | ];
 787  cases n7; [ intro; reflexivity | ];
 788  cases n8; [ intro; reflexivity | ];
 789  cases n9; [ intro; reflexivity | ];
 790  cases n10; [ intro; reflexivity | ];
 791  cases n11; [ intro; reflexivity | ];
 792  cases n12; [ intro; reflexivity | ];
 793  cases n13; [ intro; reflexivity | ];
 794  cases n14; [ intro; reflexivity | ];
 795  cases n15; [ intro; reflexivity | ];
 796  intros;
 797  change in ⊢ (? ? % ?) with (exadecimal_of_nat n16);
 798  change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
 799  rewrite > mod_plus;
 800  change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
 801  rewrite < mod_mod;
 802   [ apply H;
 803     unfold lt;
 804     autobatch.
 805   | autobatch
 806   ]
 807 qed.
 808
 809 lemma nat_of_exadecimal_exadecimal_of_nat:
 810  ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
 811  intro;
 812  rewrite > exadecimal_of_nat_mod;
 813  generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
 814  generalize in match (n \mod 16); intro;
 815  cases n1; [ intro; reflexivity | ];
 816  cases n2; [ intro; reflexivity | ];
 817  cases n3; [ intro; reflexivity | ];
 818  cases n4; [ intro; reflexivity | ];
 819  cases n5; [ intro; reflexivity | ];
 820  cases n6; [ intro; reflexivity | ];
 821  cases n7; [ intro; reflexivity | ];
 822  cases n8; [ intro; reflexivity | ];
 823  cases n9; [ intro; reflexivity | ];
 824  cases n10; [ intro; reflexivity | ];
 825  cases n11 [ intro; reflexivity | ];
 826  cases n12; [ intro; reflexivity | ];
 827  cases n13; [ intro; reflexivity | ];
 828  cases n14; [ intro; reflexivity | ];
 829  cases n15; [ intro; reflexivity | ];
 830  cases n16; [ intro; reflexivity | ];
 831  intro;
 832  unfold lt in H;
 833  cut False;
 834   [ elim Hcut
 835   | autobatch
 836   ]
 837 qed.
 838
 839 lemma exadecimal_of_nat_nat_of_exadecimal:
 840  ∀b.exadecimal_of_nat (nat_of_exadecimal b) = b.
 841  intro;
 842  elim b;
 843  reflexivity.
 844 qed.
 845
 846 lemma plusex_ok:
 847  ∀b1,b2,c.
 848   match plusex b1 b2 c with
 849    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
 850  intros;
 851  elim b1; (elim b2; (elim c; normalize; reflexivity)).
 852 qed.
 853
 854 definition xpred ≝
 855  λb.
 856   match b with
 857    [ x0 ⇒ xF
 858    | x1 ⇒ x0
 859    | x2 ⇒ x1
 860    | x3 ⇒ x2
 861    | x4 ⇒ x3
 862    | x5 ⇒ x4
 863    | x6 ⇒ x5
 864    | x7 ⇒ x6
 865    | x8 ⇒ x7
 866    | x9 ⇒ x8
 867    | xA ⇒ x9
 868    | xB ⇒ xA
 869    | xC ⇒ xB
 870    | xD ⇒ xC
 871    | xE ⇒ xD
 872    | xF ⇒ xE ].
 873
 874 lemma eq_eqex_S_x0_false:
 875  ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
 876  intro;
 877  cases n 0; [ intro; simplify; reflexivity | clear n];
 878  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 879  cases n 0; [ intro; simplify; reflexivity | clear n];
 880  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 881  cases n 0; [ intro; simplify; reflexivity | clear n];
 882  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 883  cases n 0; [ intro; simplify; reflexivity | clear n];
 884  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 885  cases n 0; [ intro; simplify; reflexivity | clear n];
 886  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 887  cases n 0; [ intro; simplify; reflexivity | clear n];
 888  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 889  cases n 0; [ intro; simplify; reflexivity | clear n];
 890  cases n1 0; [ intro; simplify; reflexivity | clear n1];
 891  cases n 0; [ intro; simplify; reflexivity | clear n];
 892  intro;
 893  unfold lt in H;
 894  cut (S n1 ≤ 0);
 895   [ elim (not_le_Sn_O ? Hcut)
 896   | do 15 (apply le_S_S_to_le);
 897     assumption
 898   ]
 899 qed.
 900
 901 lemma eqex_true_to_eq: ∀b,b'. eqex b b' = true → b=b'.
 902  intros 2;
 903  elim b 0;
 904  elim b' 0;
 905  simplify;
 906  intro;
 907  first [ reflexivity | destruct H ].
 908 qed.
 909
 910 lemma eqex_false_to_not_eq: ∀b,b'. eqex b b' = false → b ≠ b'.
 911  intros 2;
 912  elim b 0;
 913  elim b' 0;
 914  simplify;
 915  intro;
 916  try (destruct H);
 917  intro K;
 918  destruct K.
 919 qed.
 920
 921 (*
 922 lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
 923  intros;
 924  rewrite > exadecimal_of_nat_mod;
 925  rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
 926 *)