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