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 definition nat_of_bool ≝
 803  λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
 804
 805 (* Way too slow. Handles 2^32 goals!
 806 lemma plusbyte_ok:
 807  ∀b1,b2,c.
 808   match plusbyte b1 b2 c with
 809    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
 810    ].
 811  intros;
 812  elim c;
 813  elim b1;
 814  elim e;
 815  elim e1;
 816  elim b2;
 817  elim e2;
 818  elim e3;
 819  reflexivity.
 820 qed.
 821 *)
 822
 823 notation "14" non associative with precedence 80 for @{ 'x14 }.
 824 interpretation "natural number" 'x14 =
 825 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 826 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 827 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 828 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 829 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 830 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 831 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 832 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 833 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 834 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 835 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 836 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 837 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 838 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 839 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
 840
 841 notation "22" non associative with precedence 80 for @{ 'x22 }.
 842 interpretation "natural number" 'x22 =
 843 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 844 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 845 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 846 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 847 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 848 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 849 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 850 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 851 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 852 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 853 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 854 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 855 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 856 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 857 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 858 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 859 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 860 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 861 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 862 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 863 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 864 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 865 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
 866
 867 notation "256" non associative with precedence 80 for @{ 'x256 }.
 868 interpretation "natural number" 'x256 =
 869 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 870 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 871 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 872 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 873 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 874 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 875 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 876 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 877 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 878 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 879 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 880 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 881 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 882 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 883 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 884 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 885 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 886 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 887 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 888 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 889 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 890 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 891 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 892 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 893 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 894 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 895 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 896 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 897 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 898 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 899 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 900 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 901 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 902 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 903 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 904 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 905 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 906 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 907 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 908 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 909 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 910 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 911 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 912 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 913 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 914 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 915 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 916 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 917 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 918 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 919 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 920 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 921 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 922 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 923 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 924 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 925 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 926 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 927 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 928 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 929 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 930 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 931 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 932 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 933 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 934 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 935 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 936 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 937 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 938 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 939 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 940 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 941 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 942 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 943 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 944 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 945 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 946 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 947 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 948 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 949 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 950 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 951 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 952 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 953 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 954 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 955 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 956 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 957 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 958 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 959 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 960 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 961 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 962 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 963 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 964 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 965 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 966 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 967 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 968 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 969 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 970 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 971 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 972 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 973 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 974 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 975 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 976 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 977 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 978 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 979 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 980 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 981 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 982 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 983 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 984 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 985 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 986 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 987 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 988 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 989 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 990 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 991 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 992 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 993 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 994 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 995 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 996 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 997 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 998 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 999 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1000 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1001 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1002 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1003 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1004 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1005 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1006 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1007 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1008 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1009 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1010 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1011 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1012 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1013 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1014 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1015 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1016 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1017 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1018 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1019 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1020 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1021 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1022 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1023 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1024 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1025 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1026 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1027 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1028 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1029 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1030 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1031 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1032 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1033 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1034 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1035 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1036 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1037 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1038 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1039 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1040 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1041 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1042 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1043 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1044 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1045 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1046 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1047 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1048 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1049 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1050 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1051 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1052 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1053 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1054 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1055 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1056 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1057 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1058 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1059 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1060 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1061 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1062 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1063 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1064 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1065 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1066 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1067 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1068 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1069 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1070 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1071 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1072 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1073 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1074 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1075 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1076 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1077 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1078 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1079 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1080 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1081 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1082 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1083 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1084 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1085 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1086 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1087 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1088 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1089 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1090 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1091 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1092 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1093 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1094 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1095 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1096 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1097 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1098 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1099 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1100 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1101 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1102 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1103 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1104 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1105 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1106 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1107 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1108 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1109 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1110 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1111 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1112 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1113 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1114 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1115 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1116 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1117 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1118 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1119 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1120 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1121 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
1122 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
1123 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1124 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1125 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1126 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
1127
1128 (*
1129 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1130  intros; elim n; [ reflexivity | unfold byte_of_nat.
1131 qed.
1132 *)
1133
1134 definition addr ≝ nat.
1135
1136 definition xpred ≝
1137  λb.
1138   match b with
1139    [ x0 ⇒ xF
1140    | x1 ⇒ x0
1141    | x2 ⇒ x1
1142    | x3 ⇒ x2
1143    | x4 ⇒ x3
1144    | x5 ⇒ x4
1145    | x6 ⇒ x5
1146    | x7 ⇒ x6
1147    | x8 ⇒ x7
1148    | x9 ⇒ x8
1149    | xA ⇒ x9
1150    | xB ⇒ xA
1151    | xC ⇒ xB
1152    | xD ⇒ xC
1153    | xE ⇒ xD
1154    | xF ⇒ xE ].
1155
1156 definition bpred ≝
1157  λb.
1158   match eqex (bl b) x0 with
1159    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1160    | false ⇒ mk_byte (bh b) (xpred (bl b))
1161    ].
1162
1163 (* Way too slow and subsumed by previous theorem
1164 lemma bpred_pred:
1165  ∀b.
1166   match eqbyte b (mk_byte x0 x0) with
1167    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1168    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1169  intros;
1170  elim b;
1171  elim e;
1172  elim e1;
1173  reflexivity.
1174 qed.
1175 *)
1176
1177 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1178
1179 coercion cic:/matita/assembly/addr_of_byte.con.
1180
1181 inductive opcode: Type ≝
1182    ADDd: opcode  (* 3 clock, 171 *)
1183  | BEQ: opcode   (* 3, 55 *)
1184  | BRA: opcode   (* 3, 48 *)
1185  | DECd: opcode  (* 5, 58 *)
1186  | LDAi: opcode  (* 2, 166 *)
1187  | LDAd: opcode  (* 3, 182 *)
1188  | STAd: opcode. (* 3, 183 *)
1189
1190 let rec cycles_of_opcode op : nat ≝
1191  match op with
1192   [ ADDd ⇒ 3
1193   | BEQ ⇒ 3
1194   | BRA ⇒ 3
1195   | DECd ⇒ 5
1196   | LDAi ⇒ 2
1197   | LDAd ⇒ 3
1198   | STAd ⇒ 3
1199   ].
1200
1201 definition opcodemap ≝
1202  [ couple ? ? ADDd (mk_byte xA xB);
1203    couple ? ? BEQ (mk_byte x3 x7);
1204    couple ? ? BRA (mk_byte x3 x0);
1205    couple ? ? DECd (mk_byte x3 xA);
1206    couple ? ? LDAi (mk_byte xA x6);
1207    couple ? ? LDAd (mk_byte xB x6);
1208    couple ? ? STAd (mk_byte xB x7) ].
1209
1210 definition opcode_of_byte ≝
1211  λb.
1212   let rec aux l ≝
1213    match l with
1214     [ nil ⇒ ADDd
1215     | cons c tl ⇒
1216        match c with
1217         [ couple op n ⇒
1218            match eqbyte n b with
1219             [ true ⇒ op
1220             | false ⇒ aux tl
1221             ]]]
1222   in
1223    aux opcodemap.
1224
1225 definition magic_of_opcode ≝
1226  λop1.
1227   match op1 with
1228    [ ADDd ⇒ 0
1229    | BEQ ⇒  1
1230    | BRA ⇒  2
1231    | DECd ⇒ 3
1232    | LDAi ⇒ 4
1233    | LDAd ⇒ 5
1234    | STAd ⇒ 6 ].
1235
1236 definition opcodeeqb ≝
1237  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1238
1239 definition byte_of_opcode : opcode → byte ≝
1240  λop.
1241   let rec aux l ≝
1242    match l with
1243     [ nil ⇒ mk_byte x0 x0
1244     | cons c tl ⇒
1245        match c with
1246         [ couple op' n ⇒
1247            match opcodeeqb op op' with
1248             [ true ⇒ n
1249             | false ⇒ aux tl
1250             ]]]
1251   in
1252    aux opcodemap.
1253
1254 record status : Type ≝ {
1255   acc : byte;
1256   pc  : addr;
1257   spc : addr;
1258   zf  : bool;
1259   cf  : bool;
1260   mem : addr → byte;
1261   clk : nat
1262 }.
1263
1264 definition update ≝
1265  λf: addr → byte.λa.λv.λx.
1266   match eqb x a with
1267    [ true ⇒ v
1268    | false ⇒ f x ].
1269
1270 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1271
1272 definition tick ≝
1273  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1274   let opc ≝ opcode_of_byte (mem pc) in
1275   let op1 ≝ mem (S pc) in
1276   let clk' ≝ cycles_of_opcode opc in
1277   match eqb (S clk) clk' with
1278    [ true ⇒
1279       match opc with
1280        [ ADDd ⇒
1281           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1282           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1283           let c' ≝ match res with [ couple _ c' ⇒ c'] in
1284            mk_status acc' (2 + pc) spc
1285             (eqb O (nat_of_byte acc')) c' mem 0 (* verify carrier! *)
1286        | BEQ ⇒
1287           mk_status
1288            acc
1289            (match zf with
1290              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
1291              | false ⇒ 2 + pc
1292              ])
1293            spc
1294            zf
1295            cf
1296            mem
1297            0
1298        | BRA ⇒
1299           mk_status
1300            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1301            spc
1302            zf
1303            cf
1304            mem
1305            0
1306        | DECd ⇒
1307           let x ≝ bpred (mem op1) in (* signed!!! *)
1308           let mem' ≝ update mem op1 x in
1309            mk_status acc (2 + pc) spc
1310             (eqb O x) cf mem' 0 (* check zb!!! *)
1311        | LDAi ⇒
1312           mk_status op1 (2 + pc) spc (eqb O op1) cf mem 0
1313        | LDAd ⇒
1314           let x ≝ mem op1 in
1315            mk_status x (2 + pc) spc (eqb O x) cf mem 0
1316        | STAd ⇒
1317           mk_status acc (2 + pc) spc zf cf
1318            (update mem op1 acc) 0
1319        ]
1320    | false ⇒
1321        mk_status
1322         acc pc spc zf cf mem (S clk)
1323    ]].
1324
1325 let rec execute s n on n ≝
1326  match n with
1327   [ O ⇒ s
1328   | S n' ⇒ execute (tick s) n'
1329   ].
1330
1331 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
1332  intros; reflexivity.
1333 qed.
1334
1335 notation "hvbox(# break a)"
1336   non associative with precedence 80
1337 for @{ 'byte_of_opcode $a }.
1338 interpretation "byte_of_opcode" 'byte_of_opcode a =
1339  (cic:/matita/assembly/byte_of_opcode.con a).
1340
1341 definition mult_source : list byte ≝
1342   [#LDAi; mk_byte x0 x0; (* A := 0 *)
1343    #STAd; mk_byte x2 x0; (* Z := A *)
1344    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1345    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
1346    #LDAd; mk_byte x2 x0; (* A := Z *)
1347    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1348    #ADDd; mk_byte x1 xE; (* A += X *)
1349    #STAd; mk_byte x2 x0; (* Z := A *)
1350    #BRA;  mk_byte xF x2; (* goto l1 *)
1351    #LDAd; mk_byte x2 x0].(* (l2) *)
1352
1353 definition mult_status ≝
1354  λx,y.
1355   mk_status (mk_byte x0 x0) 0 0 false false
1356    (λa:addr.
1357      match leb a 29 with
1358       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1359       | false ⇒
1360          match eqb a 30 with
1361           [ true ⇒ x
1362           | false ⇒ y
1363           ]
1364       ]) 0.
1365
1366 lemma plusbyte_O_x:
1367  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1368  intros;
1369  elim b;
1370  elim e;
1371  elim e1;
1372  reflexivity.
1373 qed.
1374
1375 definition plusbytenc ≝
1376  λx,y.
1377   match plusbyte x y false with
1378    [couple res _ ⇒ res].
1379
1380 lemma plusbytenc_O_x:
1381  ∀x. plusbytenc (mk_byte x0 x0) x = x.
1382  intros;
1383  unfold plusbytenc;
1384  rewrite > plusbyte_O_x;
1385  reflexivity.
1386 qed.
1387
1388 lemma test_O_O:
1389   let i ≝ 14 in
1390   let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1391    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1392  normalize;
1393  split;
1394  reflexivity.
1395 qed.
1396
1397
1398 lemma test_0_2:
1399   let x ≝ mk_byte x0 x0 in
1400   let y ≝ mk_byte x0 x2 in
1401   let i ≝ 14 + 23 * nat_of_byte y in
1402   let s ≝ execute (mult_status x y) i in
1403    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1404  intros;
1405  split;
1406  reflexivity.
1407 qed.
1408
1409 lemma test_x_1:
1410  ∀x.
1411   let y ≝ mk_byte x0 x1 in
1412   let i ≝ 14 + 23 * nat_of_byte y in
1413   let s ≝ execute (mult_status x y) i in
1414    pc s = 20 ∧ mem s 32 = x.
1415  intros;
1416  split;
1417   [ reflexivity
1418   | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1419     rewrite > plusbytenc_O_x;
1420     reflexivity
1421   ].
1422 qed.
1423
1424 lemma test_x_2:
1425  ∀x.
1426   let y ≝ mk_byte x0 x2 in
1427   let i ≝ 14 + 23 * nat_of_byte y in
1428   let s ≝ execute (mult_status x y) i in
1429    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1430  intros;
1431  split;
1432   [ reflexivity
1433   | change in ⊢ (? ? % ?) with
1434      (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1435     rewrite > plusbytenc_O_x;
1436     reflexivity
1437   ].
1438 qed.
1439
1440 (*
1441 lemma test_x_y:
1442  ∀x,y.
1443   let i ≝ 14 + 23 * nat_of_byte y in
1444   let s ≝ execute (mult_status x y) i in
1445    pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
1446  intros;
1447
1448 qed.
1449 *)
1450
1451 (*
1452  letin w ≝ 22;
1453  letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc;
1454  letin acc' ≝ (acc (execute (mult_status x y) w));
1455  normalize in acc';
1456  change in acc' with x;
1457  letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z;
1458  letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x;
1459  (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*)
1460  split;
1461   [ normalize; reflexivity
1462   | change with (byte_of_nat x = x);
1463  normalize;
1464  split;
1465   [ reflexivity
1466   | change with (byte_of_nat (x + 0));
1467  letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www;
1468  letin xxx ≝ (260 \mod 256); reduce in xxx;
1469  letin xxx ≝ ((18 + 242) \mod 256);
1470  whd in xxx;
1471  letin pc' ≝ (pc s);
1472  normalize in pc';
1473  letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s)));
1474  normalize in opcode;
1475  csc.
1476  split;
1477  reduce in s;
1478  reflexivity.
1479 qed.
1480
1481 lemma goo1:
1482  ∀x,y.
1483   let i ≝ 14 + 23 * nat_of_byte y in
1484   let s ≝ execute (mult_status x y) i in
1485    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
1486  intros;
1487 qed.
1488
1489 lemma goo: True.
1490  letin s0 ≝ mult_status;
1491  letin pc0 ≝ (pc s0);
1492  reduce in pc0;
1493  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
1494  reduce in i0;
1495
1496  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
1497  letin pc1 ≝ (pc s1);
1498  reduce in pc1;
1499  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
1500  reduce in i1;
1501
1502  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
1503  letin pc2 ≝ (pc s2);
1504  reduce in pc2;
1505  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
1506  reduce in i2;
1507
1508  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
1509  letin pc3 ≝ (pc s3);
1510  reduce in pc3;
1511  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
1512  reduce in i3;
1513  letin zf3 ≝ (zf s3);
1514  reduce in zf3;
1515
1516  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
1517  letin pc4 ≝ (pc s4);
1518  reduce in pc4;
1519  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
1520  reduce in i4;
1521
1522  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
1523  letin pc5 ≝ (pc s5);
1524  reduce in pc5;
1525  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
1526  reduce in i5;
1527
1528  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
1529  letin pc6 ≝ (pc s6);
1530  reduce in pc6;
1531  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
1532  reduce in i6;
1533
1534  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
1535  letin pc7 ≝ (pc s7);
1536  reduce in pc7;
1537  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
1538  reduce in i7;
1539
1540  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
1541  letin pc8 ≝ (pc s8);
1542  reduce in pc8;
1543  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
1544  reduce in i8;
1545
1546  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
1547  letin pc9 ≝ (pc s9);
1548  reduce in pc9;
1549  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
1550  reduce in i9;
1551
1552  exact I.
1553 qed.
1554 *)