helm/software/matita/library/assembly/assembly.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 set "baseuri" "cic:/matita/assembly/".
  16
  17 include "nat/div_and_mod.ma".
  18 include "list/list.ma".
  19
  20 inductive exadecimal : Type ≝
  21    x0: exadecimal
  22  | x1: exadecimal
  23  | x2: exadecimal
  24  | x3: exadecimal
  25  | x4: exadecimal
  26  | x5: exadecimal
  27  | x6: exadecimal
  28  | x7: exadecimal
  29  | x8: exadecimal
  30  | x9: exadecimal
  31  | xA: exadecimal
  32  | xB: exadecimal
  33  | xC: exadecimal
  34  | xD: exadecimal
  35  | xE: exadecimal
  36  | xF: exadecimal.
  37
  38 record byte : Type ≝ {
  39  bh: exadecimal;
  40  bl: exadecimal
  41 }.
  42
  43 definition eqex ≝
  44  λb1,b2.
  45   match b1 with
  46    [ x0 ⇒
  47        match b2 with
  48         [ x0 ⇒ true  | x1 ⇒ false | 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    | x1 ⇒
  53        match b2 with
  54         [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | 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    | x2 ⇒
  59        match b2 with
  60         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
  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    | x3 ⇒
  65        match b2 with
  66         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
  67         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  68         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  69         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  70    | x4 ⇒
  71        match b2 with
  72         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  73         | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  74         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  75         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  76    | x5 ⇒
  77        match b2 with
  78         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  79         | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
  80         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  81         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  82    | x6 ⇒
  83        match b2 with
  84         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  85         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
  86         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  87         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  88    | x7 ⇒
  89        match b2 with
  90         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  91         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
  92         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  93         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  94    | x8 ⇒
  95        match b2 with
  96         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  97         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  98         | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  99         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 100    | x9 ⇒
 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 ⇒ true  | xA ⇒ false | xB ⇒ false
 105         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 106    | xA ⇒
 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 ⇒ true  | xB ⇒ false
 111         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 112    | xB ⇒
 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 ⇒ true
 117         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 118    | xC ⇒
 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 ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 124    | xD ⇒
 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 ⇒ true  | xE ⇒ false | xF ⇒ false ]
 130    | xE ⇒
 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 ⇒ true  | xF ⇒ false ]
 136    | xF ⇒
 137        match b2 with
 138         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 139         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 140         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 141         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]].
 142
 143
 144 definition eqbyte ≝
 145  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 146
 147 inductive cartesian_product (A,B: Type) : Type ≝
 148  couple: ∀a:A.∀b:B. cartesian_product A B.
 149
 150 definition plusex ≝
 151  λb1,b2,c.
 152   match c with
 153    [ true ⇒
 154       match b1 with
 155        [ x0 ⇒
 156            match b2 with
 157             [ x0 ⇒ couple exadecimal bool x1 false
 158             | x1 ⇒ couple exadecimal bool x2 false
 159             | x2 ⇒ couple exadecimal bool x3 false
 160             | x3 ⇒ couple exadecimal bool x4 false
 161             | x4 ⇒ couple exadecimal bool x5 false
 162             | x5 ⇒ couple exadecimal bool x6 false
 163             | x6 ⇒ couple exadecimal bool x7 false
 164             | x7 ⇒ couple exadecimal bool x8 false
 165             | x8 ⇒ couple exadecimal bool x9 false
 166             | x9 ⇒ couple exadecimal bool xA false
 167             | xA ⇒ couple exadecimal bool xB false
 168             | xB ⇒ couple exadecimal bool xC false
 169             | xC ⇒ couple exadecimal bool xD false
 170             | xD ⇒ couple exadecimal bool xE false
 171             | xE ⇒ couple exadecimal bool xF false
 172             | xF ⇒ couple exadecimal bool x0 true ]
 173        | x1 ⇒
 174            match b2 with
 175             [ x0 ⇒ couple exadecimal bool x2 false
 176             | x1 ⇒ couple exadecimal bool x3 false
 177             | x2 ⇒ couple exadecimal bool x4 false
 178             | x3 ⇒ couple exadecimal bool x5 false
 179             | x4 ⇒ couple exadecimal bool x6 false
 180             | x5 ⇒ couple exadecimal bool x7 false
 181             | x6 ⇒ couple exadecimal bool x8 false
 182             | x7 ⇒ couple exadecimal bool x9 false
 183             | x8 ⇒ couple exadecimal bool xA false
 184             | x9 ⇒ couple exadecimal bool xB false
 185             | xA ⇒ couple exadecimal bool xC false
 186             | xB ⇒ couple exadecimal bool xD false
 187             | xC ⇒ couple exadecimal bool xE false
 188             | xD ⇒ couple exadecimal bool xF false
 189             | xE ⇒ couple exadecimal bool x0 true
 190             | xF ⇒ couple exadecimal bool x1 true ]
 191        | x2 ⇒
 192            match b2 with
 193             [ x0 ⇒ couple exadecimal bool x3 false
 194             | x1 ⇒ couple exadecimal bool x4 false
 195             | x2 ⇒ couple exadecimal bool x5 false
 196             | x3 ⇒ couple exadecimal bool x6 false
 197             | x4 ⇒ couple exadecimal bool x7 false
 198             | x5 ⇒ couple exadecimal bool x8 false
 199             | x6 ⇒ couple exadecimal bool x9 false
 200             | x7 ⇒ couple exadecimal bool xA false
 201             | x8 ⇒ couple exadecimal bool xB false
 202             | x9 ⇒ couple exadecimal bool xC false
 203             | xA ⇒ couple exadecimal bool xD false
 204             | xB ⇒ couple exadecimal bool xE false
 205             | xC ⇒ couple exadecimal bool xF false
 206             | xD ⇒ couple exadecimal bool x0 true
 207             | xE ⇒ couple exadecimal bool x1 true
 208             | xF ⇒ couple exadecimal bool x2 true ]
 209        | x3 ⇒
 210            match b2 with
 211             [ x0 ⇒ couple exadecimal bool x4 false
 212             | x1 ⇒ couple exadecimal bool x5 false
 213             | x2 ⇒ couple exadecimal bool x6 false
 214             | x3 ⇒ couple exadecimal bool x7 false
 215             | x4 ⇒ couple exadecimal bool x8 false
 216             | x5 ⇒ couple exadecimal bool x9 false
 217             | x6 ⇒ couple exadecimal bool xA false
 218             | x7 ⇒ couple exadecimal bool xB false
 219             | x8 ⇒ couple exadecimal bool xC false
 220             | x9 ⇒ couple exadecimal bool xD false
 221             | xA ⇒ couple exadecimal bool xE false
 222             | xB ⇒ couple exadecimal bool xF false
 223             | xC ⇒ couple exadecimal bool x0 true
 224             | xD ⇒ couple exadecimal bool x1 true
 225             | xE ⇒ couple exadecimal bool x2 true
 226             | xF ⇒ couple exadecimal bool x3 true ]
 227        | x4 ⇒
 228            match b2 with
 229             [ x0 ⇒ couple exadecimal bool x5 false
 230             | x1 ⇒ couple exadecimal bool x6 false
 231             | x2 ⇒ couple exadecimal bool x7 false
 232             | x3 ⇒ couple exadecimal bool x8 false
 233             | x4 ⇒ couple exadecimal bool x9 false
 234             | x5 ⇒ couple exadecimal bool xA false
 235             | x6 ⇒ couple exadecimal bool xB false
 236             | x7 ⇒ couple exadecimal bool xC false
 237             | x8 ⇒ couple exadecimal bool xD false
 238             | x9 ⇒ couple exadecimal bool xE false
 239             | xA ⇒ couple exadecimal bool xF false
 240             | xB ⇒ couple exadecimal bool x0 true
 241             | xC ⇒ couple exadecimal bool x1 true
 242             | xD ⇒ couple exadecimal bool x2 true
 243             | xE ⇒ couple exadecimal bool x3 true
 244             | xF ⇒ couple exadecimal bool x4 true ]
 245        | x5 ⇒
 246            match b2 with
 247             [ x0 ⇒ couple exadecimal bool x6 false
 248             | x1 ⇒ couple exadecimal bool x7 false
 249             | x2 ⇒ couple exadecimal bool x8 false
 250             | x3 ⇒ couple exadecimal bool x9 false
 251             | x4 ⇒ couple exadecimal bool xA false
 252             | x5 ⇒ couple exadecimal bool xB false
 253             | x6 ⇒ couple exadecimal bool xC false
 254             | x7 ⇒ couple exadecimal bool xD false
 255             | x8 ⇒ couple exadecimal bool xE false
 256             | x9 ⇒ couple exadecimal bool xF false
 257             | xA ⇒ couple exadecimal bool x0 true
 258             | xB ⇒ couple exadecimal bool x1 true
 259             | xC ⇒ couple exadecimal bool x2 true
 260             | xD ⇒ couple exadecimal bool x3 true
 261             | xE ⇒ couple exadecimal bool x4 true
 262             | xF ⇒ couple exadecimal bool x5 true ]
 263        | x6 ⇒
 264            match b2 with
 265             [ x0 ⇒ couple exadecimal bool x7 false
 266             | x1 ⇒ couple exadecimal bool x8 false
 267             | x2 ⇒ couple exadecimal bool x9 false
 268             | x3 ⇒ couple exadecimal bool xA false
 269             | x4 ⇒ couple exadecimal bool xB false
 270             | x5 ⇒ couple exadecimal bool xC false
 271             | x6 ⇒ couple exadecimal bool xD false
 272             | x7 ⇒ couple exadecimal bool xE false
 273             | x8 ⇒ couple exadecimal bool xF false
 274             | x9 ⇒ couple exadecimal bool x0 true
 275             | xA ⇒ couple exadecimal bool x1 true
 276             | xB ⇒ couple exadecimal bool x2 true
 277             | xC ⇒ couple exadecimal bool x3 true
 278             | xD ⇒ couple exadecimal bool x4 true
 279             | xE ⇒ couple exadecimal bool x5 true
 280             | xF ⇒ couple exadecimal bool x6 true ]
 281        | x7 ⇒
 282            match b2 with
 283             [ x0 ⇒ couple exadecimal bool x8 false
 284             | x1 ⇒ couple exadecimal bool x9 false
 285             | x2 ⇒ couple exadecimal bool xA false
 286             | x3 ⇒ couple exadecimal bool xB false
 287             | x4 ⇒ couple exadecimal bool xC false
 288             | x5 ⇒ couple exadecimal bool xD false
 289             | x6 ⇒ couple exadecimal bool xE false
 290             | x7 ⇒ couple exadecimal bool xF false
 291             | x8 ⇒ couple exadecimal bool x0 true
 292             | x9 ⇒ couple exadecimal bool x1 true
 293             | xA ⇒ couple exadecimal bool x2 true
 294             | xB ⇒ couple exadecimal bool x3 true
 295             | xC ⇒ couple exadecimal bool x4 true
 296             | xD ⇒ couple exadecimal bool x5 true
 297             | xE ⇒ couple exadecimal bool x6 true
 298             | xF ⇒ couple exadecimal bool x7 true ]
 299        | x8 ⇒
 300            match b2 with
 301             [ x0 ⇒ couple exadecimal bool x9 false
 302             | x1 ⇒ couple exadecimal bool xA false
 303             | x2 ⇒ couple exadecimal bool xB false
 304             | x3 ⇒ couple exadecimal bool xC false
 305             | x4 ⇒ couple exadecimal bool xD false
 306             | x5 ⇒ couple exadecimal bool xE false
 307             | x6 ⇒ couple exadecimal bool xF false
 308             | x7 ⇒ couple exadecimal bool x0 true
 309             | x8 ⇒ couple exadecimal bool x1 true
 310             | x9 ⇒ couple exadecimal bool x2 true
 311             | xA ⇒ couple exadecimal bool x3 true
 312             | xB ⇒ couple exadecimal bool x4 true
 313             | xC ⇒ couple exadecimal bool x5 true
 314             | xD ⇒ couple exadecimal bool x6 true
 315             | xE ⇒ couple exadecimal bool x7 true
 316             | xF ⇒ couple exadecimal bool x8 true ]
 317        | x9 ⇒
 318            match b2 with
 319             [ x0 ⇒ couple exadecimal bool xA false
 320             | x1 ⇒ couple exadecimal bool xB false
 321             | x2 ⇒ couple exadecimal bool xC false
 322             | x3 ⇒ couple exadecimal bool xD false
 323             | x4 ⇒ couple exadecimal bool xE false
 324             | x5 ⇒ couple exadecimal bool xF false
 325             | x6 ⇒ couple exadecimal bool x0 true
 326             | x7 ⇒ couple exadecimal bool x1 true
 327             | x8 ⇒ couple exadecimal bool x2 true
 328             | x9 ⇒ couple exadecimal bool x3 true
 329             | xA ⇒ couple exadecimal bool x4 true
 330             | xB ⇒ couple exadecimal bool x5 true
 331             | xC ⇒ couple exadecimal bool x6 true
 332             | xD ⇒ couple exadecimal bool x7 true
 333             | xE ⇒ couple exadecimal bool x8 true
 334             | xF ⇒ couple exadecimal bool x9 true ]
 335        | xA ⇒
 336            match b2 with
 337             [ x0 ⇒ couple exadecimal bool xB false
 338             | x1 ⇒ couple exadecimal bool xC false
 339             | x2 ⇒ couple exadecimal bool xD false
 340             | x3 ⇒ couple exadecimal bool xE false
 341             | x4 ⇒ couple exadecimal bool xF false
 342             | x5 ⇒ couple exadecimal bool x0 true
 343             | x6 ⇒ couple exadecimal bool x1 true
 344             | x7 ⇒ couple exadecimal bool x2 true
 345             | x8 ⇒ couple exadecimal bool x3 true
 346             | x9 ⇒ couple exadecimal bool x4 true
 347             | xA ⇒ couple exadecimal bool x5 true
 348             | xB ⇒ couple exadecimal bool x6 true
 349             | xC ⇒ couple exadecimal bool x7 true
 350             | xD ⇒ couple exadecimal bool x8 true
 351             | xE ⇒ couple exadecimal bool x9 true
 352             | xF ⇒ couple exadecimal bool xA true ]
 353        | xB ⇒
 354            match b2 with
 355             [ x0 ⇒ couple exadecimal bool xC false
 356             | x1 ⇒ couple exadecimal bool xD false
 357             | x2 ⇒ couple exadecimal bool xE false
 358             | x3 ⇒ couple exadecimal bool xF false
 359             | x4 ⇒ couple exadecimal bool x0 true
 360             | x5 ⇒ couple exadecimal bool x1 true
 361             | x6 ⇒ couple exadecimal bool x2 true
 362             | x7 ⇒ couple exadecimal bool x3 true
 363             | x8 ⇒ couple exadecimal bool x4 true
 364             | x9 ⇒ couple exadecimal bool x5 true
 365             | xA ⇒ couple exadecimal bool x6 true
 366             | xB ⇒ couple exadecimal bool x7 true
 367             | xC ⇒ couple exadecimal bool x8 true
 368             | xD ⇒ couple exadecimal bool x9 true
 369             | xE ⇒ couple exadecimal bool xA true
 370             | xF ⇒ couple exadecimal bool xB true ]
 371        | xC ⇒
 372            match b2 with
 373             [ x0 ⇒ couple exadecimal bool xD false
 374             | x1 ⇒ couple exadecimal bool xE false
 375             | x2 ⇒ couple exadecimal bool xF false
 376             | x3 ⇒ couple exadecimal bool x0 true
 377             | x4 ⇒ couple exadecimal bool x1 true
 378             | x5 ⇒ couple exadecimal bool x2 true
 379             | x6 ⇒ couple exadecimal bool x3 true
 380             | x7 ⇒ couple exadecimal bool x4 true
 381             | x8 ⇒ couple exadecimal bool x5 true
 382             | x9 ⇒ couple exadecimal bool x6 true
 383             | xA ⇒ couple exadecimal bool x7 true
 384             | xB ⇒ couple exadecimal bool x8 true
 385             | xC ⇒ couple exadecimal bool x9 true
 386             | xD ⇒ couple exadecimal bool xA true
 387             | xE ⇒ couple exadecimal bool xB true
 388             | xF ⇒ couple exadecimal bool xC true ]
 389        | xD ⇒
 390            match b2 with
 391             [ x0 ⇒ couple exadecimal bool xE false
 392             | x1 ⇒ couple exadecimal bool xF false
 393             | x2 ⇒ couple exadecimal bool x0 true
 394             | x3 ⇒ couple exadecimal bool x1 true
 395             | x4 ⇒ couple exadecimal bool x2 true
 396             | x5 ⇒ couple exadecimal bool x3 true
 397             | x6 ⇒ couple exadecimal bool x4 true
 398             | x7 ⇒ couple exadecimal bool x5 true
 399             | x8 ⇒ couple exadecimal bool x6 true
 400             | x9 ⇒ couple exadecimal bool x7 true
 401             | xA ⇒ couple exadecimal bool x8 true
 402             | xB ⇒ couple exadecimal bool x9 true
 403             | xC ⇒ couple exadecimal bool xA true
 404             | xD ⇒ couple exadecimal bool xB true
 405             | xE ⇒ couple exadecimal bool xC true
 406             | xF ⇒ couple exadecimal bool xD true ]
 407        | xE ⇒
 408            match b2 with
 409             [ x0 ⇒ couple exadecimal bool xF false
 410             | x1 ⇒ couple exadecimal bool x0 true
 411             | x2 ⇒ couple exadecimal bool x1 true
 412             | x3 ⇒ couple exadecimal bool x2 true
 413             | x4 ⇒ couple exadecimal bool x3 true
 414             | x5 ⇒ couple exadecimal bool x4 true
 415             | x6 ⇒ couple exadecimal bool x5 true
 416             | x7 ⇒ couple exadecimal bool x6 true
 417             | x8 ⇒ couple exadecimal bool x7 true
 418             | x9 ⇒ couple exadecimal bool x8 true
 419             | xA ⇒ couple exadecimal bool x9 true
 420             | xB ⇒ couple exadecimal bool xA true
 421             | xC ⇒ couple exadecimal bool xB true
 422             | xD ⇒ couple exadecimal bool xC true
 423             | xE ⇒ couple exadecimal bool xD true
 424             | xF ⇒ couple exadecimal bool xE true ]
 425        | xF ⇒
 426            match b2 with
 427             [ x0 ⇒ couple exadecimal bool x0 true
 428             | x1 ⇒ couple exadecimal bool x1 true
 429             | x2 ⇒ couple exadecimal bool x2 true
 430             | x3 ⇒ couple exadecimal bool x3 true
 431             | x4 ⇒ couple exadecimal bool x4 true
 432             | x5 ⇒ couple exadecimal bool x5 true
 433             | x6 ⇒ couple exadecimal bool x6 true
 434             | x7 ⇒ couple exadecimal bool x7 true
 435             | x8 ⇒ couple exadecimal bool x8 true
 436             | x9 ⇒ couple exadecimal bool x9 true
 437             | xA ⇒ couple exadecimal bool xA true
 438             | xB ⇒ couple exadecimal bool xB true
 439             | xC ⇒ couple exadecimal bool xC true
 440             | xD ⇒ couple exadecimal bool xD true
 441             | xE ⇒ couple exadecimal bool xE true
 442             | xF ⇒ couple exadecimal bool xF true ]
 443        ]
 444    | false ⇒
 445       match b1 with
 446        [ x0 ⇒
 447            match b2 with
 448             [ x0 ⇒ couple exadecimal bool x0 false
 449             | x1 ⇒ couple exadecimal bool x1 false
 450             | x2 ⇒ couple exadecimal bool x2 false
 451             | x3 ⇒ couple exadecimal bool x3 false
 452             | x4 ⇒ couple exadecimal bool x4 false
 453             | x5 ⇒ couple exadecimal bool x5 false
 454             | x6 ⇒ couple exadecimal bool x6 false
 455             | x7 ⇒ couple exadecimal bool x7 false
 456             | x8 ⇒ couple exadecimal bool x8 false
 457             | x9 ⇒ couple exadecimal bool x9 false
 458             | xA ⇒ couple exadecimal bool xA false
 459             | xB ⇒ couple exadecimal bool xB false
 460             | xC ⇒ couple exadecimal bool xC false
 461             | xD ⇒ couple exadecimal bool xD false
 462             | xE ⇒ couple exadecimal bool xE false
 463             | xF ⇒ couple exadecimal bool xF false ]
 464        | x1 ⇒
 465            match b2 with
 466             [ x0 ⇒ couple exadecimal bool x1 false
 467             | x1 ⇒ couple exadecimal bool x2 false
 468             | x2 ⇒ couple exadecimal bool x3 false
 469             | x3 ⇒ couple exadecimal bool x4 false
 470             | x4 ⇒ couple exadecimal bool x5 false
 471             | x5 ⇒ couple exadecimal bool x6 false
 472             | x6 ⇒ couple exadecimal bool x7 false
 473             | x7 ⇒ couple exadecimal bool x8 false
 474             | x8 ⇒ couple exadecimal bool x9 false
 475             | x9 ⇒ couple exadecimal bool xA false
 476             | xA ⇒ couple exadecimal bool xB false
 477             | xB ⇒ couple exadecimal bool xC false
 478             | xC ⇒ couple exadecimal bool xD false
 479             | xD ⇒ couple exadecimal bool xE false
 480             | xE ⇒ couple exadecimal bool xF false
 481             | xF ⇒ couple exadecimal bool x0 true ]
 482        | x2 ⇒
 483            match b2 with
 484             [ x0 ⇒ couple exadecimal bool x2 false
 485             | x1 ⇒ couple exadecimal bool x3 false
 486             | x2 ⇒ couple exadecimal bool x4 false
 487             | x3 ⇒ couple exadecimal bool x5 false
 488             | x4 ⇒ couple exadecimal bool x6 false
 489             | x5 ⇒ couple exadecimal bool x7 false
 490             | x6 ⇒ couple exadecimal bool x8 false
 491             | x7 ⇒ couple exadecimal bool x9 false
 492             | x8 ⇒ couple exadecimal bool xA false
 493             | x9 ⇒ couple exadecimal bool xB false
 494             | xA ⇒ couple exadecimal bool xC false
 495             | xB ⇒ couple exadecimal bool xD false
 496             | xC ⇒ couple exadecimal bool xE false
 497             | xD ⇒ couple exadecimal bool xF false
 498             | xE ⇒ couple exadecimal bool x0 true
 499             | xF ⇒ couple exadecimal bool x1 true ]
 500        | x3 ⇒
 501            match b2 with
 502             [ x0 ⇒ couple exadecimal bool x3 false
 503             | x1 ⇒ couple exadecimal bool x4 false
 504             | x2 ⇒ couple exadecimal bool x5 false
 505             | x3 ⇒ couple exadecimal bool x6 false
 506             | x4 ⇒ couple exadecimal bool x7 false
 507             | x5 ⇒ couple exadecimal bool x8 false
 508             | x6 ⇒ couple exadecimal bool x9 false
 509             | x7 ⇒ couple exadecimal bool xA false
 510             | x8 ⇒ couple exadecimal bool xB false
 511             | x9 ⇒ couple exadecimal bool xC false
 512             | xA ⇒ couple exadecimal bool xD false
 513             | xB ⇒ couple exadecimal bool xE false
 514             | xC ⇒ couple exadecimal bool xF false
 515             | xD ⇒ couple exadecimal bool x0 true
 516             | xE ⇒ couple exadecimal bool x1 true
 517             | xF ⇒ couple exadecimal bool x2 true ]
 518        | x4 ⇒
 519            match b2 with
 520             [ x0 ⇒ couple exadecimal bool x4 false
 521             | x1 ⇒ couple exadecimal bool x5 false
 522             | x2 ⇒ couple exadecimal bool x6 false
 523             | x3 ⇒ couple exadecimal bool x7 false
 524             | x4 ⇒ couple exadecimal bool x8 false
 525             | x5 ⇒ couple exadecimal bool x9 false
 526             | x6 ⇒ couple exadecimal bool xA false
 527             | x7 ⇒ couple exadecimal bool xB false
 528             | x8 ⇒ couple exadecimal bool xC false
 529             | x9 ⇒ couple exadecimal bool xD false
 530             | xA ⇒ couple exadecimal bool xE false
 531             | xB ⇒ couple exadecimal bool xF false
 532             | xC ⇒ couple exadecimal bool x0 true
 533             | xD ⇒ couple exadecimal bool x1 true
 534             | xE ⇒ couple exadecimal bool x2 true
 535             | xF ⇒ couple exadecimal bool x3 true ]
 536        | x5 ⇒
 537            match b2 with
 538             [ x0 ⇒ couple exadecimal bool x5 false
 539             | x1 ⇒ couple exadecimal bool x6 false
 540             | x2 ⇒ couple exadecimal bool x7 false
 541             | x3 ⇒ couple exadecimal bool x8 false
 542             | x4 ⇒ couple exadecimal bool x9 false
 543             | x5 ⇒ couple exadecimal bool xA false
 544             | x6 ⇒ couple exadecimal bool xB false
 545             | x7 ⇒ couple exadecimal bool xC false
 546             | x8 ⇒ couple exadecimal bool xD false
 547             | x9 ⇒ couple exadecimal bool xE false
 548             | xA ⇒ couple exadecimal bool xF false
 549             | xB ⇒ couple exadecimal bool x0 true
 550             | xC ⇒ couple exadecimal bool x1 true
 551             | xD ⇒ couple exadecimal bool x2 true
 552             | xE ⇒ couple exadecimal bool x3 true
 553             | xF ⇒ couple exadecimal bool x4 true ]
 554        | x6 ⇒
 555            match b2 with
 556             [ x0 ⇒ couple exadecimal bool x6 false
 557             | x1 ⇒ couple exadecimal bool x7 false
 558             | x2 ⇒ couple exadecimal bool x8 false
 559             | x3 ⇒ couple exadecimal bool x9 false
 560             | x4 ⇒ couple exadecimal bool xA false
 561             | x5 ⇒ couple exadecimal bool xB false
 562             | x6 ⇒ couple exadecimal bool xC false
 563             | x7 ⇒ couple exadecimal bool xD false
 564             | x8 ⇒ couple exadecimal bool xE false
 565             | x9 ⇒ couple exadecimal bool xF false
 566             | xA ⇒ couple exadecimal bool x0 true
 567             | xB ⇒ couple exadecimal bool x1 true
 568             | xC ⇒ couple exadecimal bool x2 true
 569             | xD ⇒ couple exadecimal bool x3 true
 570             | xE ⇒ couple exadecimal bool x4 true
 571             | xF ⇒ couple exadecimal bool x5 true ]
 572        | x7 ⇒
 573            match b2 with
 574             [ x0 ⇒ couple exadecimal bool x7 false
 575             | x1 ⇒ couple exadecimal bool x8 false
 576             | x2 ⇒ couple exadecimal bool x9 false
 577             | x3 ⇒ couple exadecimal bool xA false
 578             | x4 ⇒ couple exadecimal bool xB false
 579             | x5 ⇒ couple exadecimal bool xC false
 580             | x6 ⇒ couple exadecimal bool xD false
 581             | x7 ⇒ couple exadecimal bool xE false
 582             | x8 ⇒ couple exadecimal bool xF false
 583             | x9 ⇒ couple exadecimal bool x0 true
 584             | xA ⇒ couple exadecimal bool x1 true
 585             | xB ⇒ couple exadecimal bool x2 true
 586             | xC ⇒ couple exadecimal bool x3 true
 587             | xD ⇒ couple exadecimal bool x4 true
 588             | xE ⇒ couple exadecimal bool x5 true
 589             | xF ⇒ couple exadecimal bool x6 true ]
 590        | x8 ⇒
 591            match b2 with
 592             [ x0 ⇒ couple exadecimal bool x8 false
 593             | x1 ⇒ couple exadecimal bool x9 false
 594             | x2 ⇒ couple exadecimal bool xA false
 595             | x3 ⇒ couple exadecimal bool xB false
 596             | x4 ⇒ couple exadecimal bool xC false
 597             | x5 ⇒ couple exadecimal bool xD false
 598             | x6 ⇒ couple exadecimal bool xE false
 599             | x7 ⇒ couple exadecimal bool xF false
 600             | x8 ⇒ couple exadecimal bool x0 true
 601             | x9 ⇒ couple exadecimal bool x1 true
 602             | xA ⇒ couple exadecimal bool x2 true
 603             | xB ⇒ couple exadecimal bool x3 true
 604             | xC ⇒ couple exadecimal bool x4 true
 605             | xD ⇒ couple exadecimal bool x5 true
 606             | xE ⇒ couple exadecimal bool x6 true
 607             | xF ⇒ couple exadecimal bool x7 true ]
 608        | x9 ⇒
 609            match b2 with
 610             [ x0 ⇒ couple exadecimal bool x9 false
 611             | x1 ⇒ couple exadecimal bool xA false
 612             | x2 ⇒ couple exadecimal bool xB false
 613             | x3 ⇒ couple exadecimal bool xC false
 614             | x4 ⇒ couple exadecimal bool xD false
 615             | x5 ⇒ couple exadecimal bool xE false
 616             | x6 ⇒ couple exadecimal bool xF false
 617             | x7 ⇒ couple exadecimal bool x0 true
 618             | x8 ⇒ couple exadecimal bool x1 true
 619             | x9 ⇒ couple exadecimal bool x2 true
 620             | xA ⇒ couple exadecimal bool x3 true
 621             | xB ⇒ couple exadecimal bool x4 true
 622             | xC ⇒ couple exadecimal bool x5 true
 623             | xD ⇒ couple exadecimal bool x6 true
 624             | xE ⇒ couple exadecimal bool x7 true
 625             | xF ⇒ couple exadecimal bool x8 true ]
 626        | xA ⇒
 627            match b2 with
 628             [ x0 ⇒ couple exadecimal bool xA false
 629             | x1 ⇒ couple exadecimal bool xB false
 630             | x2 ⇒ couple exadecimal bool xC false
 631             | x3 ⇒ couple exadecimal bool xD false
 632             | x4 ⇒ couple exadecimal bool xE false
 633             | x5 ⇒ couple exadecimal bool xF false
 634             | x6 ⇒ couple exadecimal bool x0 true
 635             | x7 ⇒ couple exadecimal bool x1 true
 636             | x8 ⇒ couple exadecimal bool x2 true
 637             | x9 ⇒ couple exadecimal bool x3 true
 638             | xA ⇒ couple exadecimal bool x4 true
 639             | xB ⇒ couple exadecimal bool x5 true
 640             | xC ⇒ couple exadecimal bool x6 true
 641             | xD ⇒ couple exadecimal bool x7 true
 642             | xE ⇒ couple exadecimal bool x8 true
 643             | xF ⇒ couple exadecimal bool x9 true ]
 644        | xB ⇒
 645            match b2 with
 646             [ x0 ⇒ couple exadecimal bool xB false
 647             | x1 ⇒ couple exadecimal bool xC false
 648             | x2 ⇒ couple exadecimal bool xD false
 649             | x3 ⇒ couple exadecimal bool xE false
 650             | x4 ⇒ couple exadecimal bool xF false
 651             | x5 ⇒ couple exadecimal bool x0 true
 652             | x6 ⇒ couple exadecimal bool x1 true
 653             | x7 ⇒ couple exadecimal bool x2 true
 654             | x8 ⇒ couple exadecimal bool x3 true
 655             | x9 ⇒ couple exadecimal bool x4 true
 656             | xA ⇒ couple exadecimal bool x5 true
 657             | xB ⇒ couple exadecimal bool x6 true
 658             | xC ⇒ couple exadecimal bool x7 true
 659             | xD ⇒ couple exadecimal bool x8 true
 660             | xE ⇒ couple exadecimal bool x9 true
 661             | xF ⇒ couple exadecimal bool xA true ]
 662        | xC ⇒
 663            match b2 with
 664             [ x0 ⇒ couple exadecimal bool xC false
 665             | x1 ⇒ couple exadecimal bool xD false
 666             | x2 ⇒ couple exadecimal bool xE false
 667             | x3 ⇒ couple exadecimal bool xF false
 668             | x4 ⇒ couple exadecimal bool x0 true
 669             | x5 ⇒ couple exadecimal bool x1 true
 670             | x6 ⇒ couple exadecimal bool x2 true
 671             | x7 ⇒ couple exadecimal bool x3 true
 672             | x8 ⇒ couple exadecimal bool x4 true
 673             | x9 ⇒ couple exadecimal bool x5 true
 674             | xA ⇒ couple exadecimal bool x6 true
 675             | xB ⇒ couple exadecimal bool x7 true
 676             | xC ⇒ couple exadecimal bool x8 true
 677             | xD ⇒ couple exadecimal bool x9 true
 678             | xE ⇒ couple exadecimal bool xA true
 679             | xF ⇒ couple exadecimal bool xB true ]
 680        | xD ⇒
 681            match b2 with
 682             [ x0 ⇒ couple exadecimal bool xD false
 683             | x1 ⇒ couple exadecimal bool xE false
 684             | x2 ⇒ couple exadecimal bool xF false
 685             | x3 ⇒ couple exadecimal bool x0 true
 686             | x4 ⇒ couple exadecimal bool x1 true
 687             | x5 ⇒ couple exadecimal bool x2 true
 688             | x6 ⇒ couple exadecimal bool x3 true
 689             | x7 ⇒ couple exadecimal bool x4 true
 690             | x8 ⇒ couple exadecimal bool x5 true
 691             | x9 ⇒ couple exadecimal bool x6 true
 692             | xA ⇒ couple exadecimal bool x7 true
 693             | xB ⇒ couple exadecimal bool x8 true
 694             | xC ⇒ couple exadecimal bool x9 true
 695             | xD ⇒ couple exadecimal bool xA true
 696             | xE ⇒ couple exadecimal bool xB true
 697             | xF ⇒ couple exadecimal bool xC true ]
 698        | xE ⇒
 699            match b2 with
 700             [ x0 ⇒ couple exadecimal bool xE false
 701             | x1 ⇒ couple exadecimal bool xF false
 702             | x2 ⇒ couple exadecimal bool x0 true
 703             | x3 ⇒ couple exadecimal bool x1 true
 704             | x4 ⇒ couple exadecimal bool x2 true
 705             | x5 ⇒ couple exadecimal bool x3 true
 706             | x6 ⇒ couple exadecimal bool x4 true
 707             | x7 ⇒ couple exadecimal bool x5 true
 708             | x8 ⇒ couple exadecimal bool x6 true
 709             | x9 ⇒ couple exadecimal bool x7 true
 710             | xA ⇒ couple exadecimal bool x8 true
 711             | xB ⇒ couple exadecimal bool x9 true
 712             | xC ⇒ couple exadecimal bool xA true
 713             | xD ⇒ couple exadecimal bool xB true
 714             | xE ⇒ couple exadecimal bool xC true
 715             | xF ⇒ couple exadecimal bool xD true ]
 716        | xF ⇒
 717            match b2 with
 718             [ x0 ⇒ couple exadecimal bool xF false
 719             | x1 ⇒ couple exadecimal bool x0 true
 720             | x2 ⇒ couple exadecimal bool x1 true
 721             | x3 ⇒ couple exadecimal bool x2 true
 722             | x4 ⇒ couple exadecimal bool x3 true
 723             | x5 ⇒ couple exadecimal bool x4 true
 724             | x6 ⇒ couple exadecimal bool x5 true
 725             | x7 ⇒ couple exadecimal bool x6 true
 726             | x8 ⇒ couple exadecimal bool x7 true
 727             | x9 ⇒ couple exadecimal bool x8 true
 728             | xA ⇒ couple exadecimal bool x9 true
 729             | xB ⇒ couple exadecimal bool xA true
 730             | xC ⇒ couple exadecimal bool xB true
 731             | xD ⇒ couple exadecimal bool xC true
 732             | xE ⇒ couple exadecimal bool xD true
 733             | xF ⇒ couple exadecimal bool xE true ]
 734        ]
 735    ]
 736 .
 737
 738 definition plusbyte ≝
 739  λb1,b2,c.
 740   match plusex (bl b1) (bl b2) c with
 741    [ couple l c' ⇒
 742       match plusex (bh b1) (bh b2) c' with
 743        [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
 744
 745 alias num (instance 0) = "natural number".
 746 definition nat_of_exadecimal ≝
 747  λb.
 748   match b with
 749    [ x0 ⇒ 0
 750    | x1 ⇒ 1
 751    | x2 ⇒ 2
 752    | x3 ⇒ 3
 753    | x4 ⇒ 4
 754    | x5 ⇒ 5
 755    | x6 ⇒ 6
 756    | x7 ⇒ 7
 757    | x8 ⇒ 8
 758    | x9 ⇒ 9
 759    | xA ⇒ 10
 760    | xB ⇒ 11
 761    | xC ⇒ 12
 762    | xD ⇒ 13
 763    | xE ⇒ 14
 764    | xF ⇒ 15
 765    ].
 766
 767 coercion cic:/matita/assembly/nat_of_exadecimal.con.
 768
 769 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
 770
 771 coercion cic:/matita/assembly/nat_of_byte.con.
 772
 773 let rec exadecimal_of_nat b ≝
 774   match b with [ O ⇒ x0 | S b ⇒
 775   match b with [ O ⇒ x1 | S b ⇒
 776   match b with [ O ⇒ x2 | S b ⇒
 777   match b with [ O ⇒ x3 | S b ⇒
 778   match b with [ O ⇒ x4 | S b ⇒
 779   match b with [ O ⇒ x5 | S b ⇒
 780   match b with [ O ⇒ x6 | S b ⇒
 781   match b with [ O ⇒ x7 | S b ⇒
 782   match b with [ O ⇒ x8 | S b ⇒
 783   match b with [ O ⇒ x9 | S b ⇒
 784   match b with [ O ⇒ xA | S b ⇒
 785   match b with [ O ⇒ xB | S b ⇒
 786   match b with [ O ⇒ xC | S b ⇒
 787   match b with [ O ⇒ xD | S b ⇒
 788   match b with [ O ⇒ xE | S b ⇒
 789   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
 790
 791 definition byte_of_nat ≝
 792  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
 793
 794 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
 795  intros;
 796  elim b;
 797  elim e;
 798  elim e1;
 799  reflexivity.
 800 qed.
 801
 802 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
 803  intro;
 804  elim b;
 805  simplify;
 806  autobatch.
 807 qed.
 808
 809 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
 810  intro;
 811  unfold nat_of_byte;
 812  letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
 813  letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
 814  unfold lt in H K ⊢ %;
 815  letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
 816  letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
 817  apply le_S_S;
 818  cut (16*bh b ≤ 16*15);
 819   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
 820     simplify in Hf:(? ? %);
 821     assumption
 822   | autobatch
 823   ]
 824 qed.
 825
 826 lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
 827  intros;
 828  autobatch.
 829 qed.
 830
 831 axiom daemon: False.
 832
 833 lemma exadecimal_of_nat_mod:
 834  ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
 835  elim daemon.
 836 (*
 837  intros;
 838  cases n; [ reflexivity | ];
 839  cases n1; [ reflexivity | ];
 840  cases n2; [ reflexivity | ];
 841  cases n3; [ reflexivity | ];
 842  cases n4; [ reflexivity | ];
 843  cases n5; [ reflexivity | ];
 844  cases n6; [ reflexivity | ];
 845  cases n7; [ reflexivity | ];
 846  cases n8; [ reflexivity | ];
 847  cases n9; [ reflexivity | ];
 848  cases n10; [ reflexivity | ];
 849  cases n11; [ reflexivity | ];
 850  cases n12; [ reflexivity | ];
 851  cases n13; [ reflexivity | ];
 852  cases n14; [ reflexivity | ];
 853  cases n15; [ reflexivity | ];
 854  change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
 855  cut ((16 + n16) \mod 16 = n16 \mod 16);
 856   [ rewrite > Hcut;
 857     simplify in ⊢ (? ? % ?);
 858
 859   | unfold mod;
 860     change with (mod_aux (16+n16) (16+n16) 15 = n16);
 861     unfold mod_aux;
 862     change with
 863      (match leb (16+n16) 15 with
 864        [true ⇒ 16+n16
 865        | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
 866        ] = n16);
 867     cut (leb (16+n16) 15 = false);
 868      [ rewrite > Hcut;
 869        change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
 870        cut (16+n16-16 = n16);
 871         [ rewrite > Hcut1; clear Hcut1;
 872
 873         |
 874         ]
 875      |
 876      ]
 877   ]*)
 878 qed.
 879
 880 (*lemma exadecimal_of_nat_elim:
 881  ∀P:exadecimal → Prop.
 882   (∀m. m < 16 → P (exadecimal_of_nat m)) →
 883     ∀n. P (exadecimal_of_nat n).
 884  intros;
 885  cases n; [ apply H; autobatch | ]; clear n;
 886  cases n1; [ apply H; autobatch | ]; clear n1;
 887  cases n; [ apply H; autobatch | ]; clear n;
 888  cases n1; [ apply H; autobatch | ]; clear n1;
 889  cases n; [ apply H; autobatch | ]; clear n;
 890  cases n1; [ apply H; autobatch | ]; clear n1;
 891  cases n; [ apply H; autobatch | ]; clear n;
 892  cases n1; [ apply H; autobatch | ]; clear n1;
 893  cases n; [ apply H; autobatch | ]; clear n;
 894  cases n1; [ apply H; autobatch | ]; clear n1;
 895  cases n; [ apply H; autobatch | ]; clear n;
 896  cases n1; [ apply H; autobatch | ]; clear n1;
 897  cases n; [ apply H; autobatch | ]; clear n;
 898  cases n1; [ apply H; autobatch | ]; clear n1;
 899  cases n; [ apply H; autobatch | ]; clear n;
 900  cases n1; [ apply H; autobatch | ]; clear n1;
 901  simplify;
 902  elim daemon.
 903 qed.
 904 *)
 905
 906 axiom nat_of_exadecimal_exadecimal_of_nat:
 907  ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
 908 (*
 909  intro;
 910  apply (exadecimal_of_nat_elim (λn.;
 911
 912
 913
 914  elim n 0; [ reflexivity | intro ];
 915  elim n1 0; [ intros; reflexivity | intros 2 ];
 916  elim n2 0; [ intros; reflexivity | intros 2 ];
 917  elim n3 0; [ intros; reflexivity | intros 2 ];
 918  elim n4 0; [ intros; reflexivity | intros 2 ];
 919  elim n5 0; [ intros; reflexivity | intros 2 ];
 920  elim n6 0; [ intros; reflexivity | intros 2 ];
 921  elim n7 0; [ intros; reflexivity | intros 2 ];
 922  elim n8 0; [ intros; reflexivity | intros 2 ];
 923  elim n9 0; [ intros; reflexivity | intros 2 ];
 924  elim n10 0; [ intros; reflexivity | intros 2 ];
 925  elim n11 0; [ intros; reflexivity | intros 2 ];
 926  elim n12 0; [ intros; reflexivity | intros 2 ];
 927  elim n13 0; [ intros; reflexivity | intros 2 ];
 928  elim n14 0; [ intros; reflexivity | intros 2 ];
 929  elim n15 0; [ intros; reflexivity | intros 2 ];
 930  intro;
 931  simplify;
 932  rewrite < H15;
 933  change in ⊢ (? ? % ?) with (nat_of_exadecimal (exadecimal_of_nat n16));
 934 qed.
 935 *)
 936
 937 lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
 938  intro;
 939  unfold byte_of_nat;
 940  unfold nat_of_byte;
 941  change with (16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n = n \mod 256);
 942  rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
 943  rewrite > nat_of_exadecimal_exadecimal_of_nat;
 944  elim daemon.
 945 qed.
 946
 947 definition nat_of_bool ≝
 948  λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
 949
 950 lemma plusex_ok:
 951  ∀b1,b2,c.
 952   match plusex b1 b2 c with
 953    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
 954  intros;
 955  elim c;
 956  elim b1;
 957  elim b2;
 958  normalize;
 959  reflexivity.
 960 qed.
 961
 962 lemma plusbyte_ok:
 963  ∀b1,b2,c.
 964   match plusbyte b1 b2 c with
 965    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
 966    ].
 967  intros;
 968  unfold plusbyte;
 969  generalize in match (plusex_ok (bl b1) (bl b2) c);
 970  elim (plusex (bl b1) (bl b2) c);
 971  simplify in H ⊢ %;
 972  generalize in match (plusex_ok (bh b1) (bh b2) t1);
 973  elim (plusex (bh b1) (bh b2) t1);
 974  simplify in H1 ⊢ %;
 975  change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
 976  unfold nat_of_byte;
 977  letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
 978  rewrite > distr_times_plus in K:(? ? ? %);
 979  rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
 980  rewrite < associative_times in K:(? ? ? (? ? %));
 981  normalize in K:(? ? ? (? ? (? % ?)));
 982  rewrite > symmetric_times in K:(? ? ? (? ? %));
 983  rewrite > sym_plus in ⊢ (? ? ? (? % ?));
 984  rewrite > associative_plus in ⊢ (? ? ? %);
 985  letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
 986   apply transitive_eq; [3: apply K' | skip | ];
 987  clear K';
 988  rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
 989  rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
 990  rewrite > associative_plus in ⊢ (? ? % ?);
 991  rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
 992  rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
 993  rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
 994  rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
 995  rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
 996  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
 997  rewrite > H; clear H;
 998  autobatch paramodulation.
 999 qed.
1000
1001 (*
1002 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1003  intros; elim n; [ reflexivity | unfold byte_of_nat.
1004 qed.
1005 *)
1006
1007 definition addr ≝ nat.
1008
1009 definition xpred ≝
1010  λb.
1011   match b with
1012    [ x0 ⇒ xF
1013    | x1 ⇒ x0
1014    | x2 ⇒ x1
1015    | x3 ⇒ x2
1016    | x4 ⇒ x3
1017    | x5 ⇒ x4
1018    | x6 ⇒ x5
1019    | x7 ⇒ x6
1020    | x8 ⇒ x7
1021    | x9 ⇒ x8
1022    | xA ⇒ x9
1023    | xB ⇒ xA
1024    | xC ⇒ xB
1025    | xD ⇒ xC
1026    | xE ⇒ xD
1027    | xF ⇒ xE ].
1028
1029 definition bpred ≝
1030  λb.
1031   match eqex (bl b) x0 with
1032    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1033    | false ⇒ mk_byte (bh b) (xpred (bl b))
1034    ].
1035
1036 (* Way too slow and subsumed by previous theorem
1037 lemma bpred_pred:
1038  ∀b.
1039   match eqbyte b (mk_byte x0 x0) with
1040    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1041    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1042  intros;
1043  elim b;
1044  elim e;
1045  elim e1;
1046  reflexivity.
1047 qed.
1048 *)
1049
1050 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1051
1052 coercion cic:/matita/assembly/addr_of_byte.con.
1053
1054 inductive opcode: Type ≝
1055    ADDd: opcode  (* 3 clock, 171 *)
1056  | BEQ: opcode   (* 3, 55 *)
1057  | BRA: opcode   (* 3, 48 *)
1058  | DECd: opcode  (* 5, 58 *)
1059  | LDAi: opcode  (* 2, 166 *)
1060  | LDAd: opcode  (* 3, 182 *)
1061  | STAd: opcode. (* 3, 183 *)
1062
1063 let rec cycles_of_opcode op : nat ≝
1064  match op with
1065   [ ADDd ⇒ 3
1066   | BEQ ⇒ 3
1067   | BRA ⇒ 3
1068   | DECd ⇒ 5
1069   | LDAi ⇒ 2
1070   | LDAd ⇒ 3
1071   | STAd ⇒ 3
1072   ].
1073
1074 definition opcodemap ≝
1075  [ couple ? ? ADDd (mk_byte xA xB);
1076    couple ? ? BEQ (mk_byte x3 x7);
1077    couple ? ? BRA (mk_byte x3 x0);
1078    couple ? ? DECd (mk_byte x3 xA);
1079    couple ? ? LDAi (mk_byte xA x6);
1080    couple ? ? LDAd (mk_byte xB x6);
1081    couple ? ? STAd (mk_byte xB x7) ].
1082
1083 definition opcode_of_byte ≝
1084  λb.
1085   let rec aux l ≝
1086    match l with
1087     [ nil ⇒ ADDd
1088     | cons c tl ⇒
1089        match c with
1090         [ couple op n ⇒
1091            match eqbyte n b with
1092             [ true ⇒ op
1093             | false ⇒ aux tl
1094             ]]]
1095   in
1096    aux opcodemap.
1097
1098 definition magic_of_opcode ≝
1099  λop1.
1100   match op1 with
1101    [ ADDd ⇒ 0
1102    | BEQ ⇒  1
1103    | BRA ⇒  2
1104    | DECd ⇒ 3
1105    | LDAi ⇒ 4
1106    | LDAd ⇒ 5
1107    | STAd ⇒ 6 ].
1108
1109 definition opcodeeqb ≝
1110  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1111
1112 definition byte_of_opcode : opcode → byte ≝
1113  λop.
1114   let rec aux l ≝
1115    match l with
1116     [ nil ⇒ mk_byte x0 x0
1117     | cons c tl ⇒
1118        match c with
1119         [ couple op' n ⇒
1120            match opcodeeqb op op' with
1121             [ true ⇒ n
1122             | false ⇒ aux tl
1123             ]]]
1124   in
1125    aux opcodemap.
1126
1127 record status : Type ≝ {
1128   acc : byte;
1129   pc  : addr;
1130   spc : addr;
1131   zf  : bool;
1132   cf  : bool;
1133   mem : addr → byte;
1134   clk : nat
1135 }.
1136
1137 definition update ≝
1138  λf: addr → byte.λa.λv.λx.
1139   match eqb x a with
1140    [ true ⇒ v
1141    | false ⇒ f x ].
1142
1143 lemma update_update_a_a:
1144  ∀s,a,v1,v2,b.
1145   update (update s a v1) a v2 b = update s a v2 b.
1146  intros;
1147  unfold update;
1148  unfold update;
1149  elim (eqb b a);
1150  reflexivity.
1151 qed.
1152
1153 lemma update_update_a_b:
1154  ∀s,a1,v1,a2,v2,b.
1155   a1 ≠ a2 →
1156    update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
1157  intros;
1158  unfold update;
1159  unfold update;
1160  apply (bool_elim ? (eqb b a1)); intros;
1161  apply (bool_elim ? (eqb b a2)); intros;
1162  simplify;
1163  [ elim H;
1164    rewrite < (eqb_true_to_eq ? ? H1);
1165    apply eqb_true_to_eq;
1166    assumption
1167  |*: reflexivity
1168  ].
1169 qed.
1170
1171 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1172
1173 definition tick ≝
1174  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1175   let opc ≝ opcode_of_byte (mem pc) in
1176   let op1 ≝ mem (S pc) in
1177   let clk' ≝ cycles_of_opcode opc in
1178   match eqb (S clk) clk' with
1179    [ true ⇒
1180       match opc with
1181        [ ADDd ⇒
1182           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1183           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1184           let c' ≝ match res with [ couple _ c' ⇒ c'] in
1185            mk_status acc' (2 + pc) spc
1186             (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
1187        | BEQ ⇒
1188           mk_status
1189            acc
1190            (match zf with
1191              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
1192                       (* FIXME: can't work - address truncated to 8 bits *)
1193              | false ⇒ 2 + pc
1194              ])
1195            spc
1196            zf
1197            cf
1198            mem
1199            0
1200        | BRA ⇒
1201           mk_status
1202            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1203                                       (* FIXME: same as above *)
1204            spc
1205            zf
1206            cf
1207            mem
1208            0
1209        | DECd ⇒
1210           let x ≝ bpred (mem op1) in (* signed!!! *)
1211           let mem' ≝ update mem op1 x in
1212            mk_status acc (2 + pc) spc
1213             (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
1214        | LDAi ⇒
1215           mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
1216        | LDAd ⇒
1217           let x ≝ mem op1 in
1218            mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
1219        | STAd ⇒
1220           mk_status acc (2 + pc) spc zf cf
1221            (update mem op1 acc) 0
1222        ]
1223    | false ⇒
1224        mk_status
1225         acc pc spc zf cf mem (S clk)
1226    ]].
1227
1228 let rec execute s n on n ≝
1229  match n with
1230   [ O ⇒ s
1231   | S n' ⇒ execute (tick s) n'
1232   ].
1233
1234 lemma breakpoint:
1235  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
1236  intros;
1237  generalize in match s; clear s;
1238  elim n1;
1239   [ reflexivity
1240   | simplify;
1241     apply H;
1242   ]
1243 qed.
1244
1245 notation "hvbox(# break a)"
1246   non associative with precedence 80
1247 for @{ 'byte_of_opcode $a }.
1248 interpretation "byte_of_opcode" 'byte_of_opcode a =
1249  (cic:/matita/assembly/byte_of_opcode.con a).
1250
1251 definition mult_source : list byte ≝
1252   [#LDAi; mk_byte x0 x0; (* A := 0 *)
1253    #STAd; mk_byte x2 x0; (* Z := A *)
1254    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1255    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
1256    #LDAd; mk_byte x2 x0; (* A := Z *)
1257    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1258    #ADDd; mk_byte x1 xE; (* A += X *)
1259    #STAd; mk_byte x2 x0; (* Z := A *)
1260    #BRA;  mk_byte xF x2; (* goto l1 *)
1261    #LDAd; mk_byte x2 x0].(* (l2) *)
1262
1263 definition mult_memory ≝
1264  λx,y.λa:addr.
1265      match leb a 29 with
1266       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1267       | false ⇒
1268          match eqb a 30 with
1269           [ true ⇒ x
1270           | false ⇒ y
1271           ]
1272       ].
1273
1274 definition mult_status ≝
1275  λx,y.
1276   mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
1277
1278 lemma plusbyte_O_x:
1279  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1280  intros;
1281  elim b;
1282  elim e;
1283  elim e1;
1284  reflexivity.
1285 qed.
1286
1287 definition plusbytenc ≝
1288  λx,y.
1289   match plusbyte x y false with
1290    [couple res _ ⇒ res].
1291
1292 definition plusbytec ≝
1293  λx,y.
1294   match plusbyte x y false with
1295    [couple _ c ⇒ c].
1296
1297 lemma plusbytenc_O_x:
1298  ∀x. plusbytenc (mk_byte x0 x0) x = x.
1299  intros;
1300  unfold plusbytenc;
1301  rewrite > plusbyte_O_x;
1302  reflexivity.
1303 qed.
1304
1305 (*axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.*)
1306 axiom mod_plus: \forall a1,a2,b1,b2,m.
1307               a1 \mod m = b1 \mod m \to
1308               a2 \mod m = b2 \mod m \to
1309               (a1 + a2) \mod m = (b1 + b2) \mod m.
1310
1311 axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
1312
1313 axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
1314
1315 theorem plusbytenc_ok:
1316  ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
1317  intros;
1318  unfold plusbytenc;
1319  generalize in match (plusbyte_ok b1 b2 false);
1320  elim (plusbyte b1 b2 false);
1321  simplify in H ⊢ %;
1322  change with (nat_of_byte t = (b1 + b2) \mod 256);
1323  rewrite < plus_n_O in H;
1324  rewrite > H; clear H;
1325  letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
1326  rewrite > K in ⊢ (? ? % ?);
1327  letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
1328     [ autobatch
1329     | cut (O =  O \mod 256);
1330        [ rewrite > Hcut in K':(? ? ? %);
1331          rewrite > K in K:(? ? % ?);
1332          rewrite > (mod_plus ? ? ? ? ? K K') in ⊢ (? ? ? %);
1333          rewrite < plus_n_O;reflexivity
1334        |simplify;reflexivity]]
1335 qed.
1336
1337 lemma test_O_O:
1338   let i ≝ 14 in
1339   let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1340    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1341  normalize;
1342  split;
1343  reflexivity.
1344 qed.
1345
1346
1347 lemma test_0_2:
1348   let x ≝ mk_byte x0 x0 in
1349   let y ≝ mk_byte x0 x2 in
1350   let i ≝ 14 + 23 * nat_of_byte y in
1351   let s ≝ execute (mult_status x y) i in
1352    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1353  intros;
1354  split;
1355  reflexivity.
1356 qed.
1357
1358 lemma test_x_1:
1359  ∀x.
1360   let y ≝ mk_byte x0 x1 in
1361   let i ≝ 14 + 23 * nat_of_byte y in
1362   let s ≝ execute (mult_status x y) i in
1363    pc s = 20 ∧ mem s 32 = x.
1364  intros;
1365  split;
1366   [ reflexivity
1367   | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1368     rewrite > plusbytenc_O_x;
1369     reflexivity
1370   ].
1371 qed.
1372
1373 lemma test_x_2:
1374  ∀x.
1375   let y ≝ mk_byte x0 x2 in
1376   let i ≝ 14 + 23 * nat_of_byte y in
1377   let s ≝ execute (mult_status x y) i in
1378    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1379  intros;
1380  split;
1381   [ reflexivity
1382   | change in ⊢ (? ? % ?) with
1383      (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1384     rewrite > plusbytenc_O_x;
1385     reflexivity
1386   ].
1387 qed.
1388
1389 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
1390  unfold lt;
1391  intros;
1392  autobatch.
1393 qed.
1394
1395 axiom status_eq:
1396  ∀s,s'.
1397   acc s = acc s' →
1398   pc s = pc s' →
1399   spc s = spc s' →
1400   zf s = zf s' →
1401   cf s = cf s' →
1402   (∀a. mem s a = mem s' a) →
1403   clk s = clk s' →
1404    s=s'.
1405
1406 lemma eq_eqex_S_x0_false:
1407  ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
1408  intro;
1409  cases n 0; [ intro; simplify; reflexivity | clear n];
1410  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1411  cases n 0; [ intro; simplify; reflexivity | clear n];
1412  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1413  cases n 0; [ intro; simplify; reflexivity | clear n];
1414  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1415  cases n 0; [ intro; simplify; reflexivity | clear n];
1416  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1417  cases n 0; [ intro; simplify; reflexivity | clear n];
1418  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1419  cases n 0; [ intro; simplify; reflexivity | clear n];
1420  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1421  cases n 0; [ intro; simplify; reflexivity | clear n];
1422  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1423  cases n 0; [ intro; simplify; reflexivity | clear n];
1424  intro;
1425  unfold lt in H;
1426  cut (S n1 ≤ 0);
1427   [ elim (not_le_Sn_O ? Hcut)
1428   | do 15 (apply le_S_S_to_le);
1429     assumption
1430   ]
1431 qed.
1432
1433 lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
1434  intros;
1435  unfold div;
1436  apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
1437  cut (∃w.m = S w);
1438   [ elim Hcut;
1439     rewrite > H2;
1440     rewrite > H2 in H1;
1441     clear Hcut; clear H2; clear H; (*clear m;*)
1442     simplify;
1443     unfold in ⊢ (? ? % ?);
1444     cut (∃z.n = S z);
1445      [ elim Hcut; clear Hcut;
1446        rewrite > H in H1;
1447        rewrite > H; clear m;
1448        change in ⊢ (? ? % ?)  with
1449         (match leb (S a1) a with
1450          [ true ⇒ O
1451          | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
1452        cut (S a1 ≰ a);
1453         [ apply (leb_elim (S a1) a);
1454            [ intro;
1455              elim (Hcut H2)
1456            | intro;
1457              simplify;
1458              reflexivity
1459            ]
1460         | intro;
1461           autobatch
1462         ]
1463      | elim H1; autobatch
1464      ]
1465   | autobatch
1466   ].
1467 qed.
1468
1469 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
1470  ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
1471  intros;
1472  unfold byte_of_nat;
1473  cut (b < 15 ∨ b ≥ 15);
1474   [ elim Hcut;
1475     [ unfold eqbyte;
1476       change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
1477       rewrite > eq_eqex_S_x0_false;
1478        [ elim (eqex (bh (mk_byte x0 x0))
1479 (bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
1480 (*
1481  alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
1482          rewrite > andb_sym;
1483 *)
1484          reflexivity
1485        | assumption
1486        ]
1487     | unfold eqbyte;
1488       change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
1489       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
1490        [ autobatch
1491        | unfold in H1;
1492          apply le_S_S;
1493          assumption
1494        | clearbody K;
1495          elim K; clear K;
1496          rewrite > H2;
1497          rewrite > eq_eqex_S_x0_false;
1498           [ reflexivity
1499           | unfold lt;
1500             unfold lt in H;
1501             rewrite < H2;
1502             clear H2; clear a; clear H1; clear Hcut;
1503             elim daemon (* trivial arithmetic property over <= and div *)
1504           ]
1505        ]
1506     ]
1507   | elim daemon
1508   ].
1509 qed.
1510
1511 lemma eq_bpred_S_a_a:
1512  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
1513 elim daemon. (*
1514  intros;
1515  unfold byte_of_nat;
1516  cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
1517   [ elim Hcut;
1518      [
1519      |
1520      ]
1521   | autobatch
1522   ].*)
1523 qed.
1524
1525 lemma plusbyteenc_S:
1526  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
1527  intros;
1528  rewrite < byte_of_nat_nat_of_byte;
1529  rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
1530  rewrite > na
1531
1532 (*CSC*)
1533  intros;
1534  unfold byte_of_nat;
1535  unfold plusbytenc;
1536  unfold plusbyte;
1537
1538  elim daemon.
1539 qed.
1540
1541 lemma eq_plusbytec_x0_x0_x_false:
1542  ∀x.plusbytec (mk_byte x0 x0) x = false.
1543  intro;
1544  elim x;
1545  elim e;
1546  elim e1;
1547  reflexivity.
1548 qed.
1549
1550 lemma loop_invariant':
1551  ∀x,y:byte.∀j:nat. j ≤ y →
1552   execute (mult_status x y) (5 + 23*j)
1553    =
1554     mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
1555      (plusbytec (byte_of_nat (x*pred j)) x)
1556      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
1557       (byte_of_nat (x * j)))
1558      0.
1559  intros 3;
1560  elim j;
1561   [ do 2 (rewrite < times_n_O);
1562     apply status_eq;
1563     [1,2,3,4,7: normalize; reflexivity
1564     | rewrite > eq_plusbytec_x0_x0_x_false;
1565       normalize;
1566       reflexivity
1567     | intro;
1568       elim daemon
1569     ]
1570   | cut (5 + 23 * S n = 5 + 23 * n + 23);
1571     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
1572       letin H' ≝ (H ?); clearbody H'; clear H;
1573       [ autobatch
1574       | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
1575         clear Hcut;
1576         rewrite > xxx;
1577         clear xxx;
1578         apply (transitive_eq ? ? ? ? K);
1579         clear K;
1580         rewrite > H';
1581         clear H';
1582         cut (∃z.y-n=S z ∧ z < 255);
1583          [ elim Hcut; clear Hcut;
1584            elim H; clear H;
1585            rewrite > H2;
1586            (* instruction LDAd *)
1587            letin K ≝
1588             (breakpoint
1589               (mk_status (byte_of_nat (x*n)) 4 O
1590                (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
1591                (plusbytec (byte_of_nat (x*pred n)) x)
1592                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1593                (byte_of_nat (x*n))) O)
1594               3 20); clearbody K;
1595            normalize in K:(? ? (? ? %) ?);
1596            apply transitive_eq; [2: apply K | skip | ]; clear K;
1597            whd in ⊢ (? ? (? % ?) ?);
1598            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1599            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
1600             with (byte_of_nat (S a));
1601            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
1602             (byte_of_nat (S a));
1603            (* instruction BEQ *)
1604            letin K ≝
1605             (breakpoint
1606               (mk_status (byte_of_nat (S a)) 6 O
1607                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
1608                (plusbytec (byte_of_nat (x*pred n)) x)
1609                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1610                  (byte_of_nat (x*n))) O)
1611               3 17); clearbody K;
1612            normalize in K:(? ? (? ? %) ?);
1613            apply transitive_eq; [2: apply K | skip | ]; clear K;
1614            whd in ⊢ (? ? (? % ?) ?);
1615            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
1616            rewrite > K; clear K;
1617            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1618            (* instruction LDAd *)
1619            letin K ≝
1620             (breakpoint
1621               (mk_status (byte_of_nat (S a)) 8 O
1622                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
1623                (plusbytec (byte_of_nat (x*pred n)) x)
1624                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1625                  (byte_of_nat (x*n))) O)
1626               3 14); clearbody K;
1627            normalize in K:(? ? (? ? %) ?);
1628            apply transitive_eq; [2: apply K | skip | ]; clear K;
1629            whd in ⊢ (? ? (? % ?) ?);
1630            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
1631            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1632            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
1633            (* instruction DECd *)
1634            letin K ≝
1635             (breakpoint
1636              (mk_status (byte_of_nat (x*n)) 10 O
1637               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
1638               (plusbytec (byte_of_nat (x*pred n)) x)
1639                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1640                 (byte_of_nat (x*n))) O)
1641              5 9); clearbody K;
1642            normalize in K:(? ? (? ? %) ?);
1643            apply transitive_eq; [2: apply K | skip | ]; clear K;
1644            whd in ⊢ (? ? (? % ?) ?);
1645            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
1646            rewrite > (eq_bpred_S_a_a ? H3);
1647            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1648            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
1649            cut (y - S n = a);
1650             [2: elim daemon | ];
1651            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
1652            (* instruction ADDd *)
1653            letin K ≝
1654             (breakpoint
1655              (mk_status (byte_of_nat (x*n)) 12
1656               O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
1657               (plusbytec (byte_of_nat (x*pred n)) x)
1658               (update
1659                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
1660                32 (byte_of_nat (x*n))) 31
1661                (byte_of_nat (y-S n))) O)
1662              3 6); clearbody K;
1663            normalize in K:(? ? (? ? %) ?);
1664            apply transitive_eq; [2: apply K | skip | ]; clear K;
1665            whd in ⊢ (? ? (? % ?) ?);
1666            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
1667             (plusbytenc (byte_of_nat (x*n)) x);
1668            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
1669             (plusbytenc (byte_of_nat (x*n)) x);
1670            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1671            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
1672             with (plusbytec (byte_of_nat (x*n)) x);
1673            rewrite > plusbyteenc_S;
1674            (* instruction STAd *)
1675            letin K ≝
1676             (breakpoint
1677              (mk_status (byte_of_nat (x*S n)) 14 O
1678               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
1679               (plusbytec (byte_of_nat (x*n)) x)
1680                (update
1681                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
1682                 32 (byte_of_nat (x*n))) 31
1683                 (byte_of_nat (y-S n))) O)
1684             3 3); clearbody K;
1685            normalize in K:(? ? (? ? %) ?);
1686            apply transitive_eq; [2: apply K | skip | ]; clear K;
1687            whd in ⊢ (? ? (? % ?) ?);
1688            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1689            (* instruction BRA *)
1690            whd in ⊢ (? ? % ?);
1691            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
1692            rewrite < pred_Sn;
1693            apply status_eq;
1694             [1,2,3,4,7: normalize; reflexivity
1695             | change with (plusbytec (byte_of_nat (x*n)) x =
1696                              plusbytec (byte_of_nat (x*n)) x);
1697               reflexivity
1698             |6: intro;
1699               elim daemon
1700             ]
1701          | exists;
1702             [ apply (y - S n)
1703             | split;
1704                [ rewrite < (minus_S_S y n);
1705                  autobatch
1706                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
1707                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
1708                  autobatch
1709                ]
1710             ]
1711          ]
1712       ]
1713     | rewrite > associative_plus;
1714       autobatch paramodulation
1715     ]
1716   ]
1717 qed.
1718
1719 theorem test_x_y:
1720  ∀x,y:byte.
1721   let i ≝ 14 + 23 * y in
1722    execute (mult_status x y) i =
1723     mk_status (byte_of_nat (x*y)) 20 0
1724      (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
1725      (plusbytec (byte_of_nat (x*pred y)) x)
1726      (update
1727        (update (mult_memory x y) 31 (mk_byte x0 x0))
1728        32 (byte_of_nat (x*y)))
1729      0.
1730  intros;
1731  cut (14 + 23 * y = 5 + 23*y + 9);
1732   [2: autobatch paramodulation;
1733   | rewrite > Hcut; (* clear Hcut; *)
1734     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
1735     rewrite > loop_invariant';
1736      [2: apply le_n
1737      | rewrite < minus_n_n;
1738        apply status_eq;
1739         [1,2,3,4,5,7: normalize; reflexivity
1740         | elim daemon
1741         ]
1742      ]
1743   ].
1744 qed.