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 alias num (instance 0) = "natural number".
 148 definition nat_of_exadecimal ≝
 149  λb.
 150   match b with
 151    [ x0 ⇒ 0
 152    | x1 ⇒ 1
 153    | x2 ⇒ 2
 154    | x3 ⇒ 3
 155    | x4 ⇒ 4
 156    | x5 ⇒ 5
 157    | x6 ⇒ 6
 158    | x7 ⇒ 7
 159    | x8 ⇒ 8
 160    | x9 ⇒ 9
 161    | xA ⇒ 10
 162    | xB ⇒ 11
 163    | xC ⇒ 12
 164    | xD ⇒ 13
 165    | xE ⇒ 14
 166    | xF ⇒ 15
 167    ].
 168
 169 coercion cic:/matita/assembly/nat_of_exadecimal.con.
 170
 171 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
 172
 173 coercion cic:/matita/assembly/nat_of_byte.con.
 174
 175 let rec exadecimal_of_nat b ≝
 176   match b with [ O ⇒ x0 | S b ⇒
 177   match b with [ O ⇒ x1 | S b ⇒
 178   match b with [ O ⇒ x2 | S b ⇒
 179   match b with [ O ⇒ x3 | S b ⇒
 180   match b with [ O ⇒ x4 | S b ⇒
 181   match b with [ O ⇒ x5 | S b ⇒
 182   match b with [ O ⇒ x6 | S b ⇒
 183   match b with [ O ⇒ x7 | S b ⇒
 184   match b with [ O ⇒ x8 | S b ⇒
 185   match b with [ O ⇒ x9 | S b ⇒
 186   match b with [ O ⇒ xA | S b ⇒
 187   match b with [ O ⇒ xB | S b ⇒
 188   match b with [ O ⇒ xC | S b ⇒
 189   match b with [ O ⇒ xD | S b ⇒
 190   match b with [ O ⇒ xE | S b ⇒
 191   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
 192
 193 definition byte_of_nat ≝
 194  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
 195
 196 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
 197  intros;
 198  elim b;
 199  elim e;
 200  elim e1;
 201  reflexivity.
 202 qed.
 203
 204 notation "14" non associative with precedence 80 for @{ 'x14 }.
 205 interpretation "natural number" 'x14 =
 206 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 207 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 208 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 209 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 210 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 211 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 212 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 213 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 214 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 215 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 216 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 217 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 218 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 219 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 220 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
 221
 222 notation "22" non associative with precedence 80 for @{ 'x22 }.
 223 interpretation "natural number" 'x22 =
 224 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 225 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 226 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 227 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 228 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 229 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 230 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 231 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 232 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 233 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 234 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 235 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 236 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 237 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 238 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 239 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 240 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 241 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 242 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 243 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 244 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 245 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 246 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
 247
 248 notation "256" non associative with precedence 80 for @{ 'x256 }.
 249 interpretation "natural number" 'x256 =
 250 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 251 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 252 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 253 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 254 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 255 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 256 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 257 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 258 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 259 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 260 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 261 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 262 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 263 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 264 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 265 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 266 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 267 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 268 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 269 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 270 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 271 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 272 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 273 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 274 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 275 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 276 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 277 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 278 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 279 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 280 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 281 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 282 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 283 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 284 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 285 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 286 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 287 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 288 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 289 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 290 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 291 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 292 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 293 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 294 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 295 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 296 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 297 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 298 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 299 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 300 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 301 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 302 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 303 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 304 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 305 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 306 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 307 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 308 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 309 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 310 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 311 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 312 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 313 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 314 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 315 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 316 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 317 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 318 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 319 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 320 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 321 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 322 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 323 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 324 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 325 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 326 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 327 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 328 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 329 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 330 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 331 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 332 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 333 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 334 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 335 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 336 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 337 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 338 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 339 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 340 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 341 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 342 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 343 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 344 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 345 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 346 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 347 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 348 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 349 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 350 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 351 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 352 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 353 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 354 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 355 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 356 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 357 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 358 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 359 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 360 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 361 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 362 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 363 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 364 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 365 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 366 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 367 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 368 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 369 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 370 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 371 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 372 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 373 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 374 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 375 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 376 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 377 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 378 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 379 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 380 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 381 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 382 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 383 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 384 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 385 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 386 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 387 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 388 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 389 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 390 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 391 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 392 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 393 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 394 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 395 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 396 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 397 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 398 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 399 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 400 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 401 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 402 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 403 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 404 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 405 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 406 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 407 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 408 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 409 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 410 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 411 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 412 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 413 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 414 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 415 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 416 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 417 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 418 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 419 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 420 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 421 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 422 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 423 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 424 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 425 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 426 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 427 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 428 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 429 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 430 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 431 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 432 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 433 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 434 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 435 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 436 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 437 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 438 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 439 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 440 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 441 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 442 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 443 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 444 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 445 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 446 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 447 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 448 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 449 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 450 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 451 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 452 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 453 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 454 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 455 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 456 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 457 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 458 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 459 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 460 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 461 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 462 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 463 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 464 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 465 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 466 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 467 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 468 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 469 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 470 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 471 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 472 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 473 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 474 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 475 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 476 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 477 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 478 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 479 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 480 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 481 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 482 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 483 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 484 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 485 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 486 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 487 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 488 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 489 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 490 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 491 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 492 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 493 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 494 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 495 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 496 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 497 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 498 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 499 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 500 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 501 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 502 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 503 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
 504 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 505 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 506 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 507 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
 508
 509 (*
 510 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
 511  intros; elim n; [ reflexivity | unfold byte_of_nat.
 512 qed.
 513 *)
 514
 515 definition addr ≝ nat.
 516
 517 definition xpred ≝
 518  λb.
 519   match b with
 520    [ x0 ⇒ xF
 521    | x1 ⇒ x0
 522    | x2 ⇒ x1
 523    | x3 ⇒ x2
 524    | x4 ⇒ x3
 525    | x5 ⇒ x4
 526    | x6 ⇒ x5
 527    | x7 ⇒ x6
 528    | x8 ⇒ x7
 529    | x9 ⇒ x8
 530    | xA ⇒ x9
 531    | xB ⇒ xA
 532    | xC ⇒ xB
 533    | xD ⇒ xC
 534    | xE ⇒ xD
 535    | xF ⇒ xE ].
 536
 537 definition bpred ≝
 538  λb.
 539   match eqex (bl b) x0 with
 540    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
 541    | false ⇒ mk_byte (bh b) (xpred (bl b))
 542    ].
 543
 544 (* Way too slow and subsumed by previous theorem
 545 lemma bpred_pred:
 546  ∀b.
 547   match eqbyte b (mk_byte x0 x0) with
 548    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
 549    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
 550  intros;
 551  elim b;
 552  elim e;
 553  elim e1;
 554  reflexivity.
 555 qed.
 556 *)
 557
 558 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
 559
 560 coercion cic:/matita/assembly/addr_of_byte.con.
 561
 562 inductive opcode: Type ≝
 563    ADDd: opcode  (* 3 clock, 171 *)
 564  | BEQ: opcode   (* 3, 55 *)
 565  | BRA: opcode   (* 3, 48 *)
 566  | DECd: opcode  (* 5, 58 *)
 567  | LDAi: opcode  (* 2, 166 *)
 568  | LDAd: opcode  (* 3, 182 *)
 569  | STAd: opcode. (* 3, 183 *)
 570
 571 let rec cycles_of_opcode op : nat ≝
 572  match op with
 573   [ ADDd ⇒ 3
 574   | BEQ ⇒ 3
 575   | BRA ⇒ 3
 576   | DECd ⇒ 5
 577   | LDAi ⇒ 2
 578   | LDAd ⇒ 3
 579   | STAd ⇒ 3
 580   ].
 581
 582 inductive cartesian_product (A,B: Type) : Type ≝
 583  couple: ∀a:A.∀b:B. cartesian_product A B.
 584
 585 definition opcodemap ≝
 586  [ couple ? ? ADDd (mk_byte xA xB);
 587    couple ? ? BEQ (mk_byte x3 x7);
 588    couple ? ? BRA (mk_byte x3 x0);
 589    couple ? ? DECd (mk_byte x3 xA);
 590    couple ? ? LDAi (mk_byte xA x6);
 591    couple ? ? LDAd (mk_byte xB x6);
 592    couple ? ? STAd (mk_byte xB x7) ].
 593
 594 definition opcode_of_byte ≝
 595  λb.
 596   let rec aux l ≝
 597    match l with
 598     [ nil ⇒ ADDd
 599     | cons c tl ⇒
 600        match c with
 601         [ couple op n ⇒
 602            match eqbyte n b with
 603             [ true ⇒ op
 604             | false ⇒ aux tl
 605             ]]]
 606   in
 607    aux opcodemap.
 608
 609 definition magic_of_opcode ≝
 610  λop1.
 611   match op1 with
 612    [ ADDd ⇒ 0
 613    | BEQ ⇒  1
 614    | BRA ⇒  2
 615    | DECd ⇒ 3
 616    | LDAi ⇒ 4
 617    | LDAd ⇒ 5
 618    | STAd ⇒ 6 ].
 619
 620 definition opcodeeqb ≝
 621  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
 622
 623 definition byte_of_opcode : opcode → byte ≝
 624  λop.
 625   let rec aux l ≝
 626    match l with
 627     [ nil ⇒ mk_byte x0 x0
 628     | cons c tl ⇒
 629        match c with
 630         [ couple op' n ⇒
 631            match opcodeeqb op op' with
 632             [ true ⇒ n
 633             | false ⇒ aux tl
 634             ]]]
 635   in
 636    aux opcodemap.
 637
 638 record status : Type ≝ {
 639   acc : byte;
 640   pc  : addr;
 641   spc : addr;
 642   zf  : bool;
 643   cf  : bool;
 644   mem : addr → byte;
 645   clk : nat
 646 }.
 647
 648 definition update ≝
 649  λf: addr → byte.λa.λv.λx.
 650   match eqb x a with
 651    [ true ⇒ v
 652    | false ⇒ f x ].
 653
 654 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
 655
 656 definition tick ≝
 657  λs:status.
 658   (* fetch *)
 659   let opc ≝ opcode_of_byte (mem s (pc s)) in
 660   let op1 ≝ mem s (S (pc s)) in
 661   let clk' ≝ cycles_of_opcode opc in
 662   match eqb (S (clk s)) clk' with
 663    [ true ⇒
 664       match opc with
 665        [ ADDd ⇒
 666           let x ≝ nat_of_byte (mem s op1) in
 667           let acc' ≝ acc s + x in (* signed!!! *)
 668            mk_status (byte_of_nat acc') (2 + pc s) (spc s)
 669             (eqb O acc') (cf s) (mem s) 0
 670        | BEQ ⇒
 671           mk_status
 672            (acc s)
 673            (match zf s with
 674              [ true ⇒ mmod16 (2 + op1 + pc s) (*\mod 256*)   (* signed!!! *)
 675              | false ⇒ 2 + pc s
 676              ])
 677            (spc s)
 678            (zf s)
 679            (cf s)
 680            (mem s)
 681            0
 682        | BRA ⇒
 683           mk_status
 684            (acc s) (mmod16 (2 + op1 + pc s) (*\mod 256*)) (* signed!!! *)
 685            (spc s)
 686            (zf s)
 687            (cf s)
 688            (mem s)
 689            0
 690        | DECd ⇒
 691           let x ≝ bpred (mem s op1) in (* signed!!! *)
 692           let mem' ≝ update (mem s) op1 x in
 693            mk_status (acc s) (2 + pc s) (spc s)
 694             (eqb O x) (cf s) mem' 0 (* check zb!!! *)
 695        | LDAi ⇒
 696           mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
 697        | LDAd ⇒
 698           let x ≝ mem s op1 in
 699            mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
 700        | STAd ⇒
 701           mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
 702            (update (mem s) op1 (acc s)) 0
 703        ]
 704    | false ⇒
 705        mk_status
 706         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
 707    ].
 708
 709 let rec execute s n on n ≝
 710  match n with
 711   [ O ⇒ s
 712   | S n' ⇒ execute (tick s) n'
 713   ].
 714
 715 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
 716  intros; reflexivity.
 717 qed.
 718
 719 notation "hvbox(# break a)"
 720   non associative with precedence 80
 721 for @{ 'byte_of_opcode $a }.
 722 interpretation "byte_of_opcode" 'byte_of_opcode a =
 723  (cic:/matita/assembly/byte_of_opcode.con a).
 724
 725 definition mult_source : list byte ≝
 726   [#LDAi; mk_byte x0 x0; (* A := 0 *)
 727    #STAd; mk_byte x2 x0; (* Z := A *)
 728    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
 729    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
 730    #LDAd; mk_byte x2 x0; (* A := Z *)
 731    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
 732    #ADDd; mk_byte x1 xE; (* A += X *)
 733    #STAd; mk_byte x2 x0; (* Z := A *)
 734    #BRA;  mk_byte xF x2; (* goto l1 *)
 735    #LDAd; mk_byte x2 x0].(* (l2) *)
 736
 737 definition mult_status ≝
 738  λx,y.
 739   mk_status (mk_byte x0 x0) 0 0 false false
 740    (λa:addr.
 741      match leb a 29 with
 742       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
 743       | false ⇒
 744          match eqb a 30 with
 745           [ true ⇒ x
 746           | false ⇒ y
 747           ]
 748       ]) 0.
 749
 750 (*
 751 lemma foobar:
 752  ∀x.
 753   let y ≝ mk_byte x0 x1 in
 754   let i ≝ 14 + 23 * nat_of_byte y in
 755   let s ≝ execute (mult_status x y) i in
 756    pc s = 20 ∧ mem s 32 = x.
 757  intros;
 758  letin w ≝ 22;
 759  letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc;
 760  letin acc' ≝ (acc (execute (mult_status x y) w)); change in acc' with (byte_of_nat x);
 761  letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z;
 762  letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x;
 763  (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*)
 764  split;
 765   [ normalize; reflexivity
 766   | change with (byte_of_nat x = x);
 767  normalize;
 768  split;
 769   [ reflexivity
 770   | change with (byte_of_nat (x + 0));
 771  letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www;
 772  letin xxx ≝ (260 \mod 256); reduce in xxx;
 773  letin xxx ≝ ((18 + 242) \mod 256);
 774  whd in xxx;
 775  letin pc' ≝ (pc s);
 776  normalize in pc';
 777  letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s)));
 778  normalize in opcode;
 779  csc.
 780  split;
 781  reduce in s;
 782  reflexivity.
 783 qed.
 784
 785 lemma goo1:
 786  ∀x,y.
 787   let i ≝ 14 + 23 * nat_of_byte y in
 788   let s ≝ execute (mult_status x y) i in
 789    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
 790  intros;
 791 qed.
 792
 793 lemma goo: True.
 794  letin s0 ≝ mult_status;
 795  letin pc0 ≝ (pc s0);
 796  reduce in pc0;
 797  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
 798  reduce in i0;
 799
 800  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
 801  letin pc1 ≝ (pc s1);
 802  reduce in pc1;
 803  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
 804  reduce in i1;
 805
 806  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
 807  letin pc2 ≝ (pc s2);
 808  reduce in pc2;
 809  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
 810  reduce in i2;
 811
 812  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
 813  letin pc3 ≝ (pc s3);
 814  reduce in pc3;
 815  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
 816  reduce in i3;
 817  letin zf3 ≝ (zf s3);
 818  reduce in zf3;
 819
 820  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
 821  letin pc4 ≝ (pc s4);
 822  reduce in pc4;
 823  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
 824  reduce in i4;
 825
 826  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
 827  letin pc5 ≝ (pc s5);
 828  reduce in pc5;
 829  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
 830  reduce in i5;
 831
 832  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
 833  letin pc6 ≝ (pc s6);
 834  reduce in pc6;
 835  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
 836  reduce in i6;
 837
 838  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
 839  letin pc7 ≝ (pc s7);
 840  reduce in pc7;
 841  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
 842  reduce in i7;
 843
 844  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
 845  letin pc8 ≝ (pc s8);
 846  reduce in pc8;
 847  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
 848  reduce in i8;
 849
 850  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
 851  letin pc9 ≝ (pc s9);
 852  reduce in pc9;
 853  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
 854  reduce in i9;
 855
 856  exact I.
 857 qed.
 858 *)