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 "nat/compare.ma".*)
  19 include "list/list.ma".
  20
  21 inductive exadecimal : Type ≝
  22    x0: exadecimal
  23  | x1: exadecimal
  24  | x2: exadecimal
  25  | x3: exadecimal
  26  | x4: exadecimal
  27  | x5: exadecimal
  28  | x6: exadecimal
  29  | x7: exadecimal
  30  | x8: exadecimal
  31  | x9: exadecimal
  32  | xA: exadecimal
  33  | xB: exadecimal
  34  | xC: exadecimal
  35  | xD: exadecimal
  36  | xE: exadecimal
  37  | xF: exadecimal.
  38
  39 record byte : Type ≝ {
  40  bh: exadecimal;
  41  bl: exadecimal
  42 }.
  43
  44 definition eqex ≝
  45  λb1,b2.
  46   match b1 with
  47    [ x0 ⇒
  48        match b2 with
  49         [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  50         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  51         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  52         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  53    | x1 ⇒
  54        match b2 with
  55         [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
  56         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  57         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  58         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  59    | x2 ⇒
  60        match b2 with
  61         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
  62         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  63         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  64         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  65    | x3 ⇒
  66        match b2 with
  67         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
  68         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  69         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  70         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  71    | x4 ⇒
  72        match b2 with
  73         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  74         | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  75         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  76         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  77    | x5 ⇒
  78        match b2 with
  79         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  80         | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
  81         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  82         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  83    | x6 ⇒
  84        match b2 with
  85         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  86         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
  87         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  88         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  89    | x7 ⇒
  90        match b2 with
  91         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  92         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
  93         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
  94         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  95    | x8 ⇒
  96        match b2 with
  97         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
  98         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
  99         | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 100         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 101    | x9 ⇒
 102        match b2 with
 103         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 104         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 105         | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 106         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 107    | xA ⇒
 108        match b2 with
 109         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 110         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 111         | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 112         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 113    | xB ⇒
 114        match b2 with
 115         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 116         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 117         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 118         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 119    | xC ⇒
 120        match b2 with
 121         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 122         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 123         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 124         | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 125    | xD ⇒
 126        match b2 with
 127         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 128         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 129         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 130         | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 131    | xE ⇒
 132        match b2 with
 133         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 134         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 135         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 136         | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ]
 137    | xF ⇒
 138        match b2 with
 139         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 140         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 141         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 142         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]].
 143
 144
 145 definition eqbyte ≝
 146  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 147
 148 alias num (instance 0) = "natural number".
 149 definition nat_of_exadecimal ≝
 150  λb.
 151   match b with
 152    [ x0 ⇒ 0
 153    | x1 ⇒ 1
 154    | x2 ⇒ 2
 155    | x3 ⇒ 3
 156    | x4 ⇒ 4
 157    | x5 ⇒ 5
 158    | x6 ⇒ 6
 159    | x7 ⇒ 7
 160    | x8 ⇒ 8
 161    | x9 ⇒ 9
 162    | xA ⇒ 10
 163    | xB ⇒ 11
 164    | xC ⇒ 12
 165    | xD ⇒ 13
 166    | xE ⇒ 14
 167    | xF ⇒ 15
 168    ].
 169
 170 coercion cic:/matita/assembly/nat_of_exadecimal.con.
 171
 172 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
 173
 174 coercion cic:/matita/assembly/nat_of_byte.con.
 175
 176 let rec exadecimal_of_nat b ≝
 177   match b with [ O ⇒ x0 | S b ⇒
 178   match b with [ O ⇒ x1 | S b ⇒
 179   match b with [ O ⇒ x2 | S b ⇒
 180   match b with [ O ⇒ x3 | S b ⇒
 181   match b with [ O ⇒ x4 | S b ⇒
 182   match b with [ O ⇒ x5 | S b ⇒
 183   match b with [ O ⇒ x6 | S b ⇒
 184   match b with [ O ⇒ x7 | S b ⇒
 185   match b with [ O ⇒ x8 | S b ⇒
 186   match b with [ O ⇒ x9 | S b ⇒
 187   match b with [ O ⇒ xA | S b ⇒
 188   match b with [ O ⇒ xB | S b ⇒
 189   match b with [ O ⇒ xC | S b ⇒
 190   match b with [ O ⇒ xD | S b ⇒
 191   match b with [ O ⇒ xE | S b ⇒
 192   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
 193
 194 definition byte_of_nat ≝
 195  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
 196  (*
 197 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
 198  intros;
 199  elim b;
 200  elim e;
 201  elim e1;
 202  reflexivity.
 203 qed. *)
 204
 205 notation "14" non associative with precedence 80 for @{ 'x14 }.
 206 interpretation "natural number" 'x14 =
 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/2)
 221 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
 222
 223 notation "22" non associative with precedence 80 for @{ 'x22 }.
 224 interpretation "natural number" 'x22 =
 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/2)
 247 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
 248
 249 notation "256" non associative with precedence 80 for @{ 'x256 }.
 250 interpretation "natural number" 'x256 =
 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/2)
 504 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
 505 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 506 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 507 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 508 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
 509
 510 (*
 511 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
 512  intros; elim n; [ reflexivity | unfold byte_of_nat.
 513 qed.
 514 *)
 515
 516 definition addr ≝ nat.
 517
 518 definition xpred ≝
 519  λb.
 520   match b with
 521    [ x0 ⇒ xF
 522    | x1 ⇒ x0
 523    | x2 ⇒ x1
 524    | x3 ⇒ x2
 525    | x4 ⇒ x3
 526    | x5 ⇒ x4
 527    | x6 ⇒ x5
 528    | x7 ⇒ x6
 529    | x8 ⇒ x7
 530    | x9 ⇒ x8
 531    | xA ⇒ x9
 532    | xB ⇒ xA
 533    | xC ⇒ xB
 534    | xD ⇒ xC
 535    | xE ⇒ xD
 536    | xF ⇒ xE ].
 537
 538 definition bpred ≝
 539  λb.
 540   match eqex (bl b) x0 with
 541    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
 542    | false ⇒ mk_byte (bh b) (xpred (bl b))
 543    ].
 544
 545 (* way too slow!
 546 lemma bpred_pred:
 547  ∀b.
 548   match eqbyte b (mk_byte x0 x0) with
 549    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
 550    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
 551  intros;
 552  elim b;
 553  elim e;
 554  elim e1;
 555  whd;
 556  reflexivity.
 557 qed.
 558 *)
 559
 560 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
 561
 562 coercion cic:/matita/assembly/addr_of_byte.con.
 563
 564 inductive opcode: Type ≝
 565    ADDd: opcode  (* 3 clock, 171 *)
 566  | BEQ: opcode   (* 3, 55 *)
 567  | BRA: opcode   (* 3, 48 *)
 568  | DECd: opcode  (* 5, 58 *)
 569  | LDAi: opcode  (* 2, 166 *)
 570  | LDAd: opcode  (* 3, 182 *)
 571  | STAd: opcode. (* 3, 183 *)
 572
 573 let rec cycles_of_opcode op : nat ≝
 574  match op with
 575   [ ADDd ⇒ 3
 576   | BEQ ⇒ 3
 577   | BRA ⇒ 3
 578   | DECd ⇒ 5
 579   | LDAi ⇒ 2
 580   | LDAd ⇒ 3
 581   | STAd ⇒ 3
 582   ].
 583
 584 inductive cartesian_product (A,B: Type) : Type ≝
 585  couple: ∀a:A.∀b:B. cartesian_product A B.
 586
 587 definition opcodemap ≝
 588  [ couple ? ? ADDd (mk_byte xA xB);
 589    couple ? ? BEQ (mk_byte x3 x7);
 590    couple ? ? BRA (mk_byte x3 x0);
 591    couple ? ? DECd (mk_byte x3 xA);
 592    couple ? ? LDAi (mk_byte xA x6);
 593    couple ? ? LDAd (mk_byte xB x6);
 594    couple ? ? STAd (mk_byte xB x7) ].
 595
 596 definition opcode_of_byte ≝
 597  λb.
 598   let rec aux l ≝
 599    match l with
 600     [ nil ⇒ ADDd
 601     | cons c tl ⇒
 602        match c with
 603         [ couple op n ⇒
 604            match eqbyte n b with
 605             [ true ⇒ op
 606             | false ⇒ aux tl
 607             ]]]
 608   in
 609    aux opcodemap.
 610
 611 definition magic_of_opcode ≝
 612  λop1.
 613   match op1 with
 614    [ ADDd ⇒ 0
 615    | BEQ ⇒  1
 616    | BRA ⇒  2
 617    | DECd ⇒ 3
 618    | LDAi ⇒ 4
 619    | LDAd ⇒ 5
 620    | STAd ⇒ 6 ].
 621
 622 definition opcodeeqb ≝
 623  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
 624
 625 definition byte_of_opcode : opcode → byte ≝
 626  λop.
 627   let rec aux l ≝
 628    match l with
 629     [ nil ⇒ mk_byte x0 x0
 630     | cons c tl ⇒
 631        match c with
 632         [ couple op' n ⇒
 633            match opcodeeqb op op' with
 634             [ true ⇒ n
 635             | false ⇒ aux tl
 636             ]]]
 637   in
 638    aux opcodemap.
 639
 640 record status : Type ≝ {
 641   acc : byte;
 642   pc  : addr;
 643   spc : addr;
 644   zf  : bool;
 645   cf  : bool;
 646   mem : addr → byte;
 647   clk : nat
 648 }.
 649
 650 definition update ≝
 651  λf: addr → byte.λa.λv.λx.
 652   match eqb x a with
 653    [ true ⇒ v
 654    | false ⇒ f x ].
 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' ≝ x + acc s 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 ⇒ 2 + op1 + pc s   (* 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) (2 + op1 + pc s) (* 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;
 727    #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
 728    #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
 729    #BEQ;  mk_byte x0 xC;
 730    #LDAd; mk_byte x1 x2;
 731    #DECd; mk_byte x1 xF;
 732    #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
 733    #STAd; mk_byte x2 x0;
 734    #LDAd; mk_byte x1 xF;
 735    #BRA;  mk_byte xF x2; (* 242 = -14 *)
 736    #LDAd; mk_byte x2 x0].
 737
 738 definition mult_status ≝
 739  λx,y.
 740   mk_status (mk_byte x0 x0) 0 0 false false
 741    (λa:addr.
 742      match leb a 29 with
 743       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
 744       | false ⇒
 745          match eqb a 30 with
 746           [ true ⇒ x
 747           | false ⇒ y
 748           ]
 749       ]) 0.
 750
 751 (*
 752 lemma foobar:
 753  ∀x.
 754   (λi.
 755     let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
 756      (* pc s = 22 ∧*) mem s 32 = byte_of_nat 0) 14.
 757  intros;
 758  letin foo ≝ (execute (mult_status x (mk_byte x0 x0)) 8);
 759  whd in foo;
 760 reduce in foo:(? ? ? ? ? ? ? ?);
 761  whd in foo;
 762
 763   xxx.
 764  change with
 765    (let s ≝ execute (mult_status x (mk_byte x0 x0)) 14 in
 766     (* pc s = 22 ∧*)  eq ? (mem s 32) (byte_of_nat 0)).
 767     xxxxxxxxx
 768  whd in ⊢ ((\lambda i:?.(let s \def ? in ? ? % %)) ?).
 769
 770  reduce;
 771  (* split; *)
 772  reflexivity;
 773 qed.
 774
 775 lemma goo1:
 776  ∀x.
 777   let i ≝ 14 in
 778   let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
 779    pc s = 22 ∧ mem s 32 = byte_of_nat 0.
 780  intros;
 781  split;
 782   [ reduce;
 783
 784   |
 785   ].
 786 qed.
 787
 788 lemma goo1:
 789  ∀x,y.
 790   let i ≝ 14 + 23 * nat_of_byte y in
 791   let s ≝ execute (mult_status x y) i in
 792    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
 793  intros;
 794 qed.
 795
 796 lemma goo: True.
 797  letin s0 ≝ mult_status;
 798  letin pc0 ≝ (pc s0);
 799  reduce in pc0;
 800  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
 801  reduce in i0;
 802
 803  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
 804  letin pc1 ≝ (pc s1);
 805  reduce in pc1;
 806  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
 807  reduce in i1;
 808
 809  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
 810  letin pc2 ≝ (pc s2);
 811  reduce in pc2;
 812  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
 813  reduce in i2;
 814
 815  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
 816  letin pc3 ≝ (pc s3);
 817  reduce in pc3;
 818  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
 819  reduce in i3;
 820  letin zf3 ≝ (zf s3);
 821  reduce in zf3;
 822
 823  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
 824  letin pc4 ≝ (pc s4);
 825  reduce in pc4;
 826  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
 827  reduce in i4;
 828
 829  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
 830  letin pc5 ≝ (pc s5);
 831  reduce in pc5;
 832  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
 833  reduce in i5;
 834
 835  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
 836  letin pc6 ≝ (pc s6);
 837  reduce in pc6;
 838  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
 839  reduce in i6;
 840
 841  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
 842  letin pc7 ≝ (pc s7);
 843  reduce in pc7;
 844  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
 845  reduce in i7;
 846
 847  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
 848  letin pc8 ≝ (pc s8);
 849  reduce in pc8;
 850  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
 851  reduce in i8;
 852
 853  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
 854  letin pc9 ≝ (pc s9);
 855  reduce in pc9;
 856  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
 857  reduce in i9;
 858
 859  exact I.
 860 qed.
 861 *)