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 axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
 803 (* intros;
 804  unfold byte_of_nat;
 805 *)
 806
 807 definition nat_of_bool ≝
 808  λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
 809
 810 lemma plusex_ok:
 811  ∀b1,b2,c.
 812   match plusex b1 b2 c with
 813    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
 814  intros;
 815  elim c;
 816  elim b1;
 817  elim b2;
 818  normalize;
 819  reflexivity.
 820 qed.
 821
 822 lemma plusbyte_ok:
 823  ∀b1,b2,c.
 824   match plusbyte b1 b2 c with
 825    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
 826    ].
 827  intros;
 828  unfold plusbyte;
 829  generalize in match (plusex_ok (bl b1) (bl b2) c);
 830  elim (plusex (bl b1) (bl b2) c);
 831  simplify in H ⊢ %;
 832  generalize in match (plusex_ok (bh b1) (bh b2) t1);
 833  elim (plusex (bh b1) (bh b2) t1);
 834  simplify in H1 ⊢ %;
 835  change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
 836  unfold nat_of_byte;
 837  letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
 838  rewrite > distr_times_plus in K:(? ? ? %);
 839  rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
 840  rewrite < associative_times in K:(? ? ? (? ? %));
 841  normalize in K:(? ? ? (? ? (? % ?)));
 842  rewrite > symmetric_times in K:(? ? ? (? ? %));
 843  rewrite > sym_plus in ⊢ (? ? ? (? % ?));
 844  rewrite > associative_plus in ⊢ (? ? ? %);
 845  letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
 846   apply transitive_eq; [3: apply K' | skip | ];
 847  clear K';
 848  rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
 849  rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
 850  rewrite > associative_plus in ⊢ (? ? % ?);
 851  rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
 852  rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
 853  rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
 854  rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
 855  rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
 856  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
 857  rewrite > H; clear H;
 858  autobatch paramodulation.
 859 qed.
 860
 861 (*
 862 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
 863  intros; elim n; [ reflexivity | unfold byte_of_nat.
 864 qed.
 865 *)
 866
 867 definition addr ≝ nat.
 868
 869 definition xpred ≝
 870  λb.
 871   match b with
 872    [ x0 ⇒ xF
 873    | x1 ⇒ x0
 874    | x2 ⇒ x1
 875    | x3 ⇒ x2
 876    | x4 ⇒ x3
 877    | x5 ⇒ x4
 878    | x6 ⇒ x5
 879    | x7 ⇒ x6
 880    | x8 ⇒ x7
 881    | x9 ⇒ x8
 882    | xA ⇒ x9
 883    | xB ⇒ xA
 884    | xC ⇒ xB
 885    | xD ⇒ xC
 886    | xE ⇒ xD
 887    | xF ⇒ xE ].
 888
 889 definition bpred ≝
 890  λb.
 891   match eqex (bl b) x0 with
 892    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
 893    | false ⇒ mk_byte (bh b) (xpred (bl b))
 894    ].
 895
 896 (* Way too slow and subsumed by previous theorem
 897 lemma bpred_pred:
 898  ∀b.
 899   match eqbyte b (mk_byte x0 x0) with
 900    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
 901    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
 902  intros;
 903  elim b;
 904  elim e;
 905  elim e1;
 906  reflexivity.
 907 qed.
 908 *)
 909
 910 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
 911
 912 coercion cic:/matita/assembly/addr_of_byte.con.
 913
 914 inductive opcode: Type ≝
 915    ADDd: opcode  (* 3 clock, 171 *)
 916  | BEQ: opcode   (* 3, 55 *)
 917  | BRA: opcode   (* 3, 48 *)
 918  | DECd: opcode  (* 5, 58 *)
 919  | LDAi: opcode  (* 2, 166 *)
 920  | LDAd: opcode  (* 3, 182 *)
 921  | STAd: opcode. (* 3, 183 *)
 922
 923 let rec cycles_of_opcode op : nat ≝
 924  match op with
 925   [ ADDd ⇒ 3
 926   | BEQ ⇒ 3
 927   | BRA ⇒ 3
 928   | DECd ⇒ 5
 929   | LDAi ⇒ 2
 930   | LDAd ⇒ 3
 931   | STAd ⇒ 3
 932   ].
 933
 934 definition opcodemap ≝
 935  [ couple ? ? ADDd (mk_byte xA xB);
 936    couple ? ? BEQ (mk_byte x3 x7);
 937    couple ? ? BRA (mk_byte x3 x0);
 938    couple ? ? DECd (mk_byte x3 xA);
 939    couple ? ? LDAi (mk_byte xA x6);
 940    couple ? ? LDAd (mk_byte xB x6);
 941    couple ? ? STAd (mk_byte xB x7) ].
 942
 943 definition opcode_of_byte ≝
 944  λb.
 945   let rec aux l ≝
 946    match l with
 947     [ nil ⇒ ADDd
 948     | cons c tl ⇒
 949        match c with
 950         [ couple op n ⇒
 951            match eqbyte n b with
 952             [ true ⇒ op
 953             | false ⇒ aux tl
 954             ]]]
 955   in
 956    aux opcodemap.
 957
 958 definition magic_of_opcode ≝
 959  λop1.
 960   match op1 with
 961    [ ADDd ⇒ 0
 962    | BEQ ⇒  1
 963    | BRA ⇒  2
 964    | DECd ⇒ 3
 965    | LDAi ⇒ 4
 966    | LDAd ⇒ 5
 967    | STAd ⇒ 6 ].
 968
 969 definition opcodeeqb ≝
 970  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
 971
 972 definition byte_of_opcode : opcode → byte ≝
 973  λop.
 974   let rec aux l ≝
 975    match l with
 976     [ nil ⇒ mk_byte x0 x0
 977     | cons c tl ⇒
 978        match c with
 979         [ couple op' n ⇒
 980            match opcodeeqb op op' with
 981             [ true ⇒ n
 982             | false ⇒ aux tl
 983             ]]]
 984   in
 985    aux opcodemap.
 986
 987 record status : Type ≝ {
 988   acc : byte;
 989   pc  : addr;
 990   spc : addr;
 991   zf  : bool;
 992   cf  : bool;
 993   mem : addr → byte;
 994   clk : nat
 995 }.
 996
 997 definition update ≝
 998  λf: addr → byte.λa.λv.λx.
 999   match eqb x a with
1000    [ true ⇒ v
1001    | false ⇒ f x ].
1002
1003 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1004
1005 definition tick ≝
1006  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1007   let opc ≝ opcode_of_byte (mem pc) in
1008   let op1 ≝ mem (S pc) in
1009   let clk' ≝ cycles_of_opcode opc in
1010   match eqb (S clk) clk' with
1011    [ true ⇒
1012       match opc with
1013        [ ADDd ⇒
1014           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1015           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1016           let c' ≝ match res with [ couple _ c' ⇒ c'] in
1017            mk_status acc' (2 + pc) spc
1018             (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
1019        | BEQ ⇒
1020           mk_status
1021            acc
1022            (match zf with
1023              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
1024              | false ⇒ 2 + pc
1025              ])
1026            spc
1027            zf
1028            cf
1029            mem
1030            0
1031        | BRA ⇒
1032           mk_status
1033            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1034            spc
1035            zf
1036            cf
1037            mem
1038            0
1039        | DECd ⇒
1040           let x ≝ bpred (mem op1) in (* signed!!! *)
1041           let mem' ≝ update mem op1 x in
1042            mk_status acc (2 + pc) spc
1043             (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
1044        | LDAi ⇒
1045           mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
1046        | LDAd ⇒
1047           let x ≝ mem op1 in
1048            mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
1049        | STAd ⇒
1050           mk_status acc (2 + pc) spc zf cf
1051            (update mem op1 acc) 0
1052        ]
1053    | false ⇒
1054        mk_status
1055         acc pc spc zf cf mem (S clk)
1056    ]].
1057
1058 let rec execute s n on n ≝
1059  match n with
1060   [ O ⇒ s
1061   | S n' ⇒ execute (tick s) n'
1062   ].
1063
1064 lemma breakpoint:
1065  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
1066  intros;
1067  generalize in match s; clear s;
1068  elim n1;
1069   [ reflexivity
1070   | simplify;
1071     apply H;
1072   ]
1073 qed.
1074
1075 notation "hvbox(# break a)"
1076   non associative with precedence 80
1077 for @{ 'byte_of_opcode $a }.
1078 interpretation "byte_of_opcode" 'byte_of_opcode a =
1079  (cic:/matita/assembly/byte_of_opcode.con a).
1080
1081 definition mult_source : list byte ≝
1082   [#LDAi; mk_byte x0 x0; (* A := 0 *)
1083    #STAd; mk_byte x2 x0; (* Z := A *)
1084    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1085    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
1086    #LDAd; mk_byte x2 x0; (* A := Z *)
1087    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1088    #ADDd; mk_byte x1 xE; (* A += X *)
1089    #STAd; mk_byte x2 x0; (* Z := A *)
1090    #BRA;  mk_byte xF x2; (* goto l1 *)
1091    #LDAd; mk_byte x2 x0].(* (l2) *)
1092
1093 definition mult_memory ≝
1094  λx,y.λa:addr.
1095      match leb a 29 with
1096       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1097       | false ⇒
1098          match eqb a 30 with
1099           [ true ⇒ x
1100           | false ⇒ y
1101           ]
1102       ].
1103
1104 definition mult_status ≝
1105  λx,y.
1106   mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
1107
1108 lemma plusbyte_O_x:
1109  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1110  intros;
1111  elim b;
1112  elim e;
1113  elim e1;
1114  reflexivity.
1115 qed.
1116
1117 definition plusbytenc ≝
1118  λx,y.
1119   match plusbyte x y false with
1120    [couple res _ ⇒ res].
1121
1122 definition plusbytec ≝
1123  λx,y.
1124   match plusbyte x y false with
1125    [couple _ c ⇒ c].
1126
1127 lemma plusbytenc_O_x:
1128  ∀x. plusbytenc (mk_byte x0 x0) x = x.
1129  intros;
1130  unfold plusbytenc;
1131  rewrite > plusbyte_O_x;
1132  reflexivity.
1133 qed.
1134
1135 axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.
1136 axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
1137
1138 axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
1139
1140 theorem plusbytenc_ok:
1141  ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
1142  intros;
1143  unfold plusbytenc;
1144  generalize in match (plusbyte_ok b1 b2 false);
1145  elim (plusbyte b1 b2 false);
1146  simplify in H ⊢ %;
1147  change with (nat_of_byte t = (b1 + b2) \mod 256);
1148  rewrite < plus_n_O in H;
1149  rewrite > H; clear H;
1150  rewrite > mod_plus;
1151  letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
1152  letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
1153   [ autobatch | ];
1154  autobatch paramodulation.
1155 qed.
1156
1157 lemma test_O_O:
1158   let i ≝ 14 in
1159   let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1160    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1161  normalize;
1162  split;
1163  reflexivity.
1164 qed.
1165
1166
1167 lemma test_0_2:
1168   let x ≝ mk_byte x0 x0 in
1169   let y ≝ mk_byte x0 x2 in
1170   let i ≝ 14 + 23 * nat_of_byte y in
1171   let s ≝ execute (mult_status x y) i in
1172    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1173  intros;
1174  split;
1175  reflexivity.
1176 qed.
1177
1178 lemma test_x_1:
1179  ∀x.
1180   let y ≝ mk_byte x0 x1 in
1181   let i ≝ 14 + 23 * nat_of_byte y in
1182   let s ≝ execute (mult_status x y) i in
1183    pc s = 20 ∧ mem s 32 = x.
1184  intros;
1185  split;
1186   [ reflexivity
1187   | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1188     rewrite > plusbytenc_O_x;
1189     reflexivity
1190   ].
1191 qed.
1192
1193 lemma test_x_2:
1194  ∀x.
1195   let y ≝ mk_byte x0 x2 in
1196   let i ≝ 14 + 23 * nat_of_byte y in
1197   let s ≝ execute (mult_status x y) i in
1198    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1199  intros;
1200  split;
1201   [ reflexivity
1202   | change in ⊢ (? ? % ?) with
1203      (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1204     rewrite > plusbytenc_O_x;
1205     reflexivity
1206   ].
1207 qed.
1208
1209 axiom byte_elim:
1210  ∀P:byte → Prop.
1211   (P (mk_byte x0 x0)) →
1212    (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
1213     ∀b:byte. P b.
1214 (* Tedious proof, easy to automate but not trivial
1215  intros;
1216  elim b;
1217  elim e;
1218   [ elim e1;
1219      [ assumption
1220      | apply (H1 0);
1221         [ apply lt_O_S
1222         | assumption
1223         ]
1224      | apply (H1 1);
1225         [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
1226           apply lt_S_S;
1227           apply lt_O_S
1228         | apply (H1 0);
1229 *)
1230
1231 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
1232  unfold lt;
1233  intros;
1234  autobatch.
1235 qed.
1236
1237 axiom daemon: False.
1238
1239 (*axiom loop_invariant:
1240  ∀x,y:byte.∀j:nat. j ≤ y →
1241   let s ≝ execute (mult_status x y) (5 + 23*j) in
1242    pc s = 4 ∧
1243    mem s 30 = x ∧
1244    mem s 31 = byte_of_nat (y - j) ∧
1245    mem s 32 = byte_of_nat (x * j).
1246
1247  intros 2;
1248  apply (byte_elim ? ? ? y);
1249   [ intros;
1250     simplify in H;
1251     cut (j=O);
1252      [ unfold s; clear s;
1253        rewrite > Hcut;
1254        reflexivity
1255      | (* easy *) elim daemon
1256      ]
1257   | intros;
1258     unfold s;
1259     cut (j < S i ∨ j = S i);
1260     [ elim Hcut;
1261        [ rewrite > nat_of_byte_byte_of_nat in H1;
1262          [2: apply (lt_trans ? 255);
1263              [ assumption
1264              | unfold lt;
1265                (* ???????? *)
1266              ]
1267          | generalize in match (H1 j); clear H1;
1268            intros;
1269            unfold lt in H3;
1270            cut (j ≤ i);
1271             [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro;
1272               apply H1
1273             | letin xxx ≝ H3;
1274               inversion xxx;
1275                [ intro;
1276                  rewrite > (injective_S ? ? H1);
1277                  autobatch
1278                | intros;
1279                  (* facile *) elim daemon
1280                ]
1281             ]
1282          ]
1283        |
1284        ]
1285     | (* easy *)
1286     ]
1287   ].
1288 qed.
1289 *)
1290
1291 axiom status_eq:
1292  ∀s,s'.
1293   acc s = acc s' →
1294   pc s = pc s' →
1295   spc s = spc s' →
1296   zf s = zf s' →
1297   cf s = cf s' →
1298   (∀a. mem s a = mem s' a) →
1299   clk s = clk s' →
1300    s=s'.
1301
1302 lemma eq_eqex_S_x0_false:
1303  ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
1304  intro;
1305  cases n 0; [ intro; simplify; reflexivity | clear n];
1306  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1307  cases n 0; [ intro; simplify; reflexivity | clear n];
1308  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1309  cases n 0; [ intro; simplify; reflexivity | clear n];
1310  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1311  cases n 0; [ intro; simplify; reflexivity | clear n];
1312  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1313  cases n 0; [ intro; simplify; reflexivity | clear n];
1314  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1315  cases n 0; [ intro; simplify; reflexivity | clear n];
1316  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1317  cases n 0; [ intro; simplify; reflexivity | clear n];
1318  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1319  cases n 0; [ intro; simplify; reflexivity | clear n];
1320  intro;
1321  unfold lt in H;
1322  cut (S n1 ≤ 0);
1323   [ elim (not_le_Sn_O ? Hcut)
1324   | do 15 (apply le_S_S_to_le);
1325     assumption
1326   ]
1327 qed.
1328
1329 lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
1330  intros;
1331  unfold div;
1332  apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
1333  cut (∃w.m = S w);
1334   [ elim Hcut;
1335     rewrite > H2;
1336     rewrite > H2 in H1;
1337     clear Hcut; clear H2; clear H; (*clear m;*)
1338     simplify;
1339     unfold in ⊢ (? ? % ?);
1340     cut (∃z.n = S z);
1341      [ elim Hcut; clear Hcut;
1342        rewrite > H in H1;
1343        rewrite > H; clear m;
1344        change in ⊢ (? ? % ?)  with
1345         (match leb (S a1) a with
1346          [ true ⇒ O
1347          | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
1348        cut (S a1 ≰ a);
1349         [ apply (leb_elim (S a1) a);
1350            [ intro;
1351              elim (Hcut H2)
1352            | intro;
1353              simplify;
1354              reflexivity
1355            ]
1356         | intro;
1357           autobatch
1358         ]
1359      | elim H1; autobatch
1360      ]
1361   | autobatch
1362   ].
1363 qed.
1364
1365 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
1366  ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
1367  intros;
1368  unfold byte_of_nat;
1369  cut (b < 15 ∨ b ≥ 15);
1370   [ elim Hcut;
1371     [ unfold eqbyte;
1372       change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
1373       rewrite > eq_eqex_S_x0_false;
1374        [ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
1375          rewrite > andb_sym;
1376          reflexivity
1377        | assumption
1378        ]
1379     | unfold eqbyte;
1380       change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
1381       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
1382        [ autobatch
1383        | unfold in H1;
1384          apply le_S_S;
1385          assumption
1386        | clearbody K;
1387          elim K; clear K;
1388          rewrite > H2;
1389          rewrite > eq_eqex_S_x0_false;
1390           [ reflexivity
1391           | unfold lt;
1392             unfold lt in H;
1393             rewrite < H2;
1394             clear H2; clear a; clear H1; clear Hcut;
1395             elim daemon (* trivial arithmetic property over <= and div *)
1396           ]
1397        ]
1398     ]
1399   | elim daemon
1400   ].
1401 qed.
1402
1403 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
1404  intro;
1405  elim b;
1406  simplify;
1407  autobatch.
1408 qed.
1409
1410 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
1411  intro;
1412  unfold nat_of_byte;
1413  letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
1414  letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
1415  unfold lt in H K ⊢ %;
1416  letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
1417  letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
1418  apply le_S_S;
1419  cut (16*bh b ≤ 16*15);
1420   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
1421     simplify in Hf:(? ? %);
1422     assumption
1423   | autobatch
1424   ]
1425 qed.
1426
1427 lemma exadecimal_of_nat_mod:
1428  ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
1429  elim daemon.
1430 (*
1431  intros;
1432  cases n; [ reflexivity | ];
1433  cases n1; [ reflexivity | ];
1434  cases n2; [ reflexivity | ];
1435  cases n3; [ reflexivity | ];
1436  cases n4; [ reflexivity | ];
1437  cases n5; [ reflexivity | ];
1438  cases n6; [ reflexivity | ];
1439  cases n7; [ reflexivity | ];
1440  cases n8; [ reflexivity | ];
1441  cases n9; [ reflexivity | ];
1442  cases n10; [ reflexivity | ];
1443  cases n11; [ reflexivity | ];
1444  cases n12; [ reflexivity | ];
1445  cases n13; [ reflexivity | ];
1446  cases n14; [ reflexivity | ];
1447  cases n15; [ reflexivity | ];
1448  change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
1449  cut ((16 + n16) \mod 16 = n16 \mod 16);
1450   [ rewrite > Hcut;
1451     simplify in ⊢ (? ? % ?);
1452
1453   | unfold mod;
1454     change with (mod_aux (16+n16) (16+n16) 15 = n16);
1455     unfold mod_aux;
1456     change with
1457      (match leb (16+n16) 15 with
1458        [true ⇒ 16+n16
1459        | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
1460        ] = n16);
1461     cut (leb (16+n16) 15 = false);
1462      [ rewrite > Hcut;
1463        change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
1464        cut (16+n16-16 = n16);
1465         [ rewrite > Hcut1; clear Hcut1;
1466
1467         |
1468         ]
1469      |
1470      ]
1471   ]*)
1472 qed.
1473
1474 lemma eq_bpred_S_a_a:
1475  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
1476 elim daemon. (*
1477  intros;
1478  unfold byte_of_nat;
1479  cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
1480   [ elim Hcut;
1481      [
1482      |
1483      ]
1484   | autobatch
1485   ].*)
1486 qed.
1487
1488 lemma plusbyteenc_S:
1489  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
1490 (*CSC*)
1491  intros;
1492  unfold byte_of_nat;
1493  unfold plusbytenc;
1494  unfold plusbyte;
1495
1496  elim daemon.
1497 qed.
1498
1499 lemma eq_plusbytec_x0_x0_x_false:
1500  ∀x.plusbytec (mk_byte x0 x0) x = false.
1501  intro;
1502  elim x;
1503  elim e;
1504  elim e1;
1505  reflexivity.
1506 qed.
1507
1508 lemma loop_invariant':
1509  ∀x,y:byte.∀j:nat. j ≤ y →
1510   execute (mult_status x y) (5 + 23*j)
1511    =
1512     mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
1513      (plusbytec (byte_of_nat (x*pred j)) x)
1514      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
1515       (byte_of_nat (x * j)))
1516      0.
1517  intros 3;
1518  elim j;
1519   [ do 2 (rewrite < times_n_O);
1520     apply status_eq;
1521     [1,2,3,4,7: normalize; reflexivity
1522     | rewrite > eq_plusbytec_x0_x0_x_false;
1523       normalize;
1524       reflexivity
1525     | intro;
1526       elim daemon
1527     ]
1528   | cut (5 + 23 * S n = 5 + 23 * n + 23);
1529     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
1530       letin H' ≝ (H ?); clearbody H'; clear H;
1531       [ autobatch
1532       | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
1533         clear Hcut;
1534         rewrite > xxx;
1535         clear xxx;
1536         apply (transitive_eq ? ? ? ? K);
1537         clear K;
1538         rewrite > H';
1539         clear H';
1540         cut (∃z.y-n=S z ∧ z < 255);
1541          [ elim Hcut; clear Hcut;
1542            elim H; clear H;
1543            rewrite > H2;
1544            (* instruction LDAd *)
1545            letin K ≝
1546             (breakpoint
1547               (mk_status (byte_of_nat (x*n)) 4 O
1548                (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
1549                (plusbytec (byte_of_nat (x*pred n)) x)
1550                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1551                (byte_of_nat (x*n))) O)
1552               3 20); clearbody K;
1553            normalize in K:(? ? (? ? %) ?);
1554            apply transitive_eq; [2: apply K | skip | ]; clear K;
1555            whd in ⊢ (? ? (? % ?) ?);
1556            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1557            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
1558             with (byte_of_nat (S a));
1559            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
1560             (byte_of_nat (S a));
1561            (* instruction BEQ *)
1562            letin K ≝
1563             (breakpoint
1564               (mk_status (byte_of_nat (S a)) 6 O
1565                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
1566                (plusbytec (byte_of_nat (x*pred n)) x)
1567                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1568                  (byte_of_nat (x*n))) O)
1569               3 17); clearbody K;
1570            normalize in K:(? ? (? ? %) ?);
1571            apply transitive_eq; [2: apply K | skip | ]; clear K;
1572            whd in ⊢ (? ? (? % ?) ?);
1573            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
1574            rewrite > K; clear K;
1575            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1576            (* instruction LDAd *)
1577            letin K ≝
1578             (breakpoint
1579               (mk_status (byte_of_nat (S a)) 8 O
1580                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
1581                (plusbytec (byte_of_nat (x*pred n)) x)
1582                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1583                  (byte_of_nat (x*n))) O)
1584               3 14); clearbody K;
1585            normalize in K:(? ? (? ? %) ?);
1586            apply transitive_eq; [2: apply K | skip | ]; clear K;
1587            whd in ⊢ (? ? (? % ?) ?);
1588            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
1589            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1590            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
1591            (* instruction DECd *)
1592            letin K ≝
1593             (breakpoint
1594              (mk_status (byte_of_nat (x*n)) 10 O
1595               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
1596               (plusbytec (byte_of_nat (x*pred n)) x)
1597                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1598                 (byte_of_nat (x*n))) O)
1599              5 9); clearbody K;
1600            normalize in K:(? ? (? ? %) ?);
1601            apply transitive_eq; [2: apply K | skip | ]; clear K;
1602            whd in ⊢ (? ? (? % ?) ?);
1603            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
1604            rewrite > (eq_bpred_S_a_a ? H3);
1605            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1606            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
1607            cut (y - S n = a);
1608             [2: elim daemon | ];
1609            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
1610            (* instruction ADDd *)
1611            letin K ≝
1612             (breakpoint
1613              (mk_status (byte_of_nat (x*n)) 12
1614               O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
1615               (plusbytec (byte_of_nat (x*pred n)) x)
1616               (update
1617                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
1618                32 (byte_of_nat (x*n))) 31
1619                (byte_of_nat (y-S n))) O)
1620              3 6); clearbody K;
1621            normalize in K:(? ? (? ? %) ?);
1622            apply transitive_eq; [2: apply K | skip | ]; clear K;
1623            whd in ⊢ (? ? (? % ?) ?);
1624            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
1625             (plusbytenc (byte_of_nat (x*n)) x);
1626            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
1627             (plusbytenc (byte_of_nat (x*n)) x);
1628            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1629            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
1630             with (plusbytec (byte_of_nat (x*n)) x);
1631            rewrite > plusbyteenc_S;
1632            (* instruction STAd *)
1633            letin K ≝
1634             (breakpoint
1635              (mk_status (byte_of_nat (x*S n)) 14 O
1636               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
1637               (plusbytec (byte_of_nat (x*n)) x)
1638                (update
1639                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
1640                 32 (byte_of_nat (x*n))) 31
1641                 (byte_of_nat (y-S n))) O)
1642             3 3); clearbody K;
1643            normalize in K:(? ? (? ? %) ?);
1644            apply transitive_eq; [2: apply K | skip | ]; clear K;
1645            whd in ⊢ (? ? (? % ?) ?);
1646            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1647            (* instruction BRA *)
1648            whd in ⊢ (? ? % ?);
1649            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
1650            rewrite < pred_Sn;
1651            apply status_eq;
1652             [1,2,3,4,7: normalize; reflexivity
1653             | change with (plusbytec (byte_of_nat (x*n)) x =
1654                              plusbytec (byte_of_nat (x*n)) x);
1655               reflexivity
1656             |6: intro;
1657               elim daemon
1658             ]
1659          | exists;
1660             [ apply (y - S n)
1661             | split;
1662                [ rewrite < (minus_S_S y n);
1663                  autobatch
1664                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
1665                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
1666                  autobatch
1667                ]
1668             ]
1669          ]
1670       ]
1671     | rewrite > associative_plus;
1672       autobatch paramodulation
1673     ]
1674   ]
1675 qed.
1676
1677 theorem test_x_y:
1678  ∀x,y:byte.
1679   let i ≝ 14 + 23 * y in
1680    execute (mult_status x y) i =
1681     mk_status (byte_of_nat (x*y)) 20 0
1682      (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
1683      (plusbytec (byte_of_nat (x*pred y)) x)
1684      (update
1685        (update (mult_memory x y) 31 (mk_byte x0 x0))
1686        32 (byte_of_nat (x*y)))
1687      0.
1688  intros;
1689  cut (14 + 23 * y = 5 + 23*y + 9);
1690   [2: autobatch paramodulation;
1691   | rewrite > Hcut; (* clear Hcut; *)
1692     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
1693     rewrite > loop_invariant';
1694      [2: apply le_n
1695      | rewrite < minus_n_n;
1696        apply status_eq;
1697         [1,2,3,4,5,7: normalize; reflexivity
1698         | elim daemon
1699         ]
1700      ]
1701   ].
1702 qed.