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 "255" non associative with precedence 80 for @{ 'x255 }.
  65 interpretation "natural number" 'x255 =
  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/1)
 322 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 323 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 324 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 325 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
 326
 327 notation "256" non associative with precedence 80 for @{ 'x256 }.
 328 interpretation "natural number" 'x256 =
 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/2)
 505 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 506 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 507 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 508 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 509 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 510 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 511 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 512 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 513 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 514 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 515 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 516 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 517 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 518 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 519 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 520 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 521 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 522 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 523 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 524 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 525 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 526 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 527 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 528 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 529 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 530 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 531 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 532 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 533 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 534 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 535 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 536 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 537 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 538 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 539 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 540 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 541 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 542 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 543 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 544 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 545 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 546 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 547 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 548 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 549 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 550 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 551 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 552 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 553 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 554 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 555 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 556 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 557 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 558 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 559 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 560 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 561 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 562 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 563 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 564 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 565 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 566 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 567 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 568 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 569 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 570 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 571 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 572 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 573 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 574 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 575 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 576 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 577 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 578 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 579 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 580 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 581 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 582 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 583 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 584 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 585 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
 586 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 587 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 588 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 589 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
 590
 591 inductive exadecimal : Type ≝
 592    x0: exadecimal
 593  | x1: exadecimal
 594  | x2: exadecimal
 595  | x3: exadecimal
 596  | x4: exadecimal
 597  | x5: exadecimal
 598  | x6: exadecimal
 599  | x7: exadecimal
 600  | x8: exadecimal
 601  | x9: exadecimal
 602  | xA: exadecimal
 603  | xB: exadecimal
 604  | xC: exadecimal
 605  | xD: exadecimal
 606  | xE: exadecimal
 607  | xF: exadecimal.
 608
 609 record byte : Type ≝ {
 610  bh: exadecimal;
 611  bl: exadecimal
 612 }.
 613
 614 definition eqex ≝
 615  λb1,b2.
 616   match b1 with
 617    [ x0 ⇒
 618        match b2 with
 619         [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 620         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 621         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 622         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 623    | x1 ⇒
 624        match b2 with
 625         [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
 626         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 627         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 628         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 629    | x2 ⇒
 630        match b2 with
 631         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
 632         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 633         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 634         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 635    | x3 ⇒
 636        match b2 with
 637         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 638         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 639         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 640         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 641    | x4 ⇒
 642        match b2 with
 643         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 644         | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 645         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 646         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 647    | x5 ⇒
 648        match b2 with
 649         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 650         | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 651         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 652         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 653    | x6 ⇒
 654        match b2 with
 655         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 656         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
 657         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 658         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 659    | x7 ⇒
 660        match b2 with
 661         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 662         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 663         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 664         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 665    | x8 ⇒
 666        match b2 with
 667         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 668         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 669         | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 670         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 671    | x9 ⇒
 672        match b2 with
 673         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 674         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 675         | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 676         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 677    | xA ⇒
 678        match b2 with
 679         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 680         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 681         | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 682         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 683    | xB ⇒
 684        match b2 with
 685         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 686         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 687         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 688         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 689    | xC ⇒
 690        match b2 with
 691         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 692         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 693         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 694         | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 695    | xD ⇒
 696        match b2 with
 697         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 698         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 699         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 700         | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 701    | xE ⇒
 702        match b2 with
 703         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 704         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 705         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 706         | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ]
 707    | xF ⇒
 708        match b2 with
 709         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 710         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 711         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 712         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]].
 713
 714
 715 definition eqbyte ≝
 716  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 717
 718 inductive cartesian_product (A,B: Type) : Type ≝
 719  couple: ∀a:A.∀b:B. cartesian_product A B.
 720
 721 definition plusex ≝
 722  λb1,b2,c.
 723   match c with
 724    [ true ⇒
 725       match b1 with
 726        [ x0 ⇒
 727            match b2 with
 728             [ x0 ⇒ couple exadecimal bool x1 false
 729             | x1 ⇒ couple exadecimal bool x2 false
 730             | x2 ⇒ couple exadecimal bool x3 false
 731             | x3 ⇒ couple exadecimal bool x4 false
 732             | x4 ⇒ couple exadecimal bool x5 false
 733             | x5 ⇒ couple exadecimal bool x6 false
 734             | x6 ⇒ couple exadecimal bool x7 false
 735             | x7 ⇒ couple exadecimal bool x8 false
 736             | x8 ⇒ couple exadecimal bool x9 false
 737             | x9 ⇒ couple exadecimal bool xA false
 738             | xA ⇒ couple exadecimal bool xB false
 739             | xB ⇒ couple exadecimal bool xC false
 740             | xC ⇒ couple exadecimal bool xD false
 741             | xD ⇒ couple exadecimal bool xE false
 742             | xE ⇒ couple exadecimal bool xF false
 743             | xF ⇒ couple exadecimal bool x0 true ]
 744        | x1 ⇒
 745            match b2 with
 746             [ x0 ⇒ couple exadecimal bool x2 false
 747             | x1 ⇒ couple exadecimal bool x3 false
 748             | x2 ⇒ couple exadecimal bool x4 false
 749             | x3 ⇒ couple exadecimal bool x5 false
 750             | x4 ⇒ couple exadecimal bool x6 false
 751             | x5 ⇒ couple exadecimal bool x7 false
 752             | x6 ⇒ couple exadecimal bool x8 false
 753             | x7 ⇒ couple exadecimal bool x9 false
 754             | x8 ⇒ couple exadecimal bool xA false
 755             | x9 ⇒ couple exadecimal bool xB false
 756             | xA ⇒ couple exadecimal bool xC false
 757             | xB ⇒ couple exadecimal bool xD false
 758             | xC ⇒ couple exadecimal bool xE false
 759             | xD ⇒ couple exadecimal bool xF false
 760             | xE ⇒ couple exadecimal bool x0 true
 761             | xF ⇒ couple exadecimal bool x1 true ]
 762        | x2 ⇒
 763            match b2 with
 764             [ x0 ⇒ couple exadecimal bool x3 false
 765             | x1 ⇒ couple exadecimal bool x4 false
 766             | x2 ⇒ couple exadecimal bool x5 false
 767             | x3 ⇒ couple exadecimal bool x6 false
 768             | x4 ⇒ couple exadecimal bool x7 false
 769             | x5 ⇒ couple exadecimal bool x8 false
 770             | x6 ⇒ couple exadecimal bool x9 false
 771             | x7 ⇒ couple exadecimal bool xA false
 772             | x8 ⇒ couple exadecimal bool xB false
 773             | x9 ⇒ couple exadecimal bool xC false
 774             | xA ⇒ couple exadecimal bool xD false
 775             | xB ⇒ couple exadecimal bool xE false
 776             | xC ⇒ couple exadecimal bool xF false
 777             | xD ⇒ couple exadecimal bool x0 true
 778             | xE ⇒ couple exadecimal bool x1 true
 779             | xF ⇒ couple exadecimal bool x2 true ]
 780        | x3 ⇒
 781            match b2 with
 782             [ x0 ⇒ couple exadecimal bool x4 false
 783             | x1 ⇒ couple exadecimal bool x5 false
 784             | x2 ⇒ couple exadecimal bool x6 false
 785             | x3 ⇒ couple exadecimal bool x7 false
 786             | x4 ⇒ couple exadecimal bool x8 false
 787             | x5 ⇒ couple exadecimal bool x9 false
 788             | x6 ⇒ couple exadecimal bool xA false
 789             | x7 ⇒ couple exadecimal bool xB false
 790             | x8 ⇒ couple exadecimal bool xC false
 791             | x9 ⇒ couple exadecimal bool xD false
 792             | xA ⇒ couple exadecimal bool xE false
 793             | xB ⇒ couple exadecimal bool xF false
 794             | xC ⇒ couple exadecimal bool x0 true
 795             | xD ⇒ couple exadecimal bool x1 true
 796             | xE ⇒ couple exadecimal bool x2 true
 797             | xF ⇒ couple exadecimal bool x3 true ]
 798        | x4 ⇒
 799            match b2 with
 800             [ x0 ⇒ couple exadecimal bool x5 false
 801             | x1 ⇒ couple exadecimal bool x6 false
 802             | x2 ⇒ couple exadecimal bool x7 false
 803             | x3 ⇒ couple exadecimal bool x8 false
 804             | x4 ⇒ couple exadecimal bool x9 false
 805             | x5 ⇒ couple exadecimal bool xA false
 806             | x6 ⇒ couple exadecimal bool xB false
 807             | x7 ⇒ couple exadecimal bool xC false
 808             | x8 ⇒ couple exadecimal bool xD false
 809             | x9 ⇒ couple exadecimal bool xE false
 810             | xA ⇒ couple exadecimal bool xF false
 811             | xB ⇒ couple exadecimal bool x0 true
 812             | xC ⇒ couple exadecimal bool x1 true
 813             | xD ⇒ couple exadecimal bool x2 true
 814             | xE ⇒ couple exadecimal bool x3 true
 815             | xF ⇒ couple exadecimal bool x4 true ]
 816        | x5 ⇒
 817            match b2 with
 818             [ x0 ⇒ couple exadecimal bool x6 false
 819             | x1 ⇒ couple exadecimal bool x7 false
 820             | x2 ⇒ couple exadecimal bool x8 false
 821             | x3 ⇒ couple exadecimal bool x9 false
 822             | x4 ⇒ couple exadecimal bool xA false
 823             | x5 ⇒ couple exadecimal bool xB false
 824             | x6 ⇒ couple exadecimal bool xC false
 825             | x7 ⇒ couple exadecimal bool xD false
 826             | x8 ⇒ couple exadecimal bool xE false
 827             | x9 ⇒ couple exadecimal bool xF false
 828             | xA ⇒ couple exadecimal bool x0 true
 829             | xB ⇒ couple exadecimal bool x1 true
 830             | xC ⇒ couple exadecimal bool x2 true
 831             | xD ⇒ couple exadecimal bool x3 true
 832             | xE ⇒ couple exadecimal bool x4 true
 833             | xF ⇒ couple exadecimal bool x5 true ]
 834        | x6 ⇒
 835            match b2 with
 836             [ x0 ⇒ couple exadecimal bool x7 false
 837             | x1 ⇒ couple exadecimal bool x8 false
 838             | x2 ⇒ couple exadecimal bool x9 false
 839             | x3 ⇒ couple exadecimal bool xA false
 840             | x4 ⇒ couple exadecimal bool xB false
 841             | x5 ⇒ couple exadecimal bool xC false
 842             | x6 ⇒ couple exadecimal bool xD false
 843             | x7 ⇒ couple exadecimal bool xE false
 844             | x8 ⇒ couple exadecimal bool xF false
 845             | x9 ⇒ couple exadecimal bool x0 true
 846             | xA ⇒ couple exadecimal bool x1 true
 847             | xB ⇒ couple exadecimal bool x2 true
 848             | xC ⇒ couple exadecimal bool x3 true
 849             | xD ⇒ couple exadecimal bool x4 true
 850             | xE ⇒ couple exadecimal bool x5 true
 851             | xF ⇒ couple exadecimal bool x6 true ]
 852        | x7 ⇒
 853            match b2 with
 854             [ x0 ⇒ couple exadecimal bool x8 false
 855             | x1 ⇒ couple exadecimal bool x9 false
 856             | x2 ⇒ couple exadecimal bool xA false
 857             | x3 ⇒ couple exadecimal bool xB false
 858             | x4 ⇒ couple exadecimal bool xC false
 859             | x5 ⇒ couple exadecimal bool xD false
 860             | x6 ⇒ couple exadecimal bool xE false
 861             | x7 ⇒ couple exadecimal bool xF false
 862             | x8 ⇒ couple exadecimal bool x0 true
 863             | x9 ⇒ couple exadecimal bool x1 true
 864             | xA ⇒ couple exadecimal bool x2 true
 865             | xB ⇒ couple exadecimal bool x3 true
 866             | xC ⇒ couple exadecimal bool x4 true
 867             | xD ⇒ couple exadecimal bool x5 true
 868             | xE ⇒ couple exadecimal bool x6 true
 869             | xF ⇒ couple exadecimal bool x7 true ]
 870        | x8 ⇒
 871            match b2 with
 872             [ x0 ⇒ couple exadecimal bool x9 false
 873             | x1 ⇒ couple exadecimal bool xA false
 874             | x2 ⇒ couple exadecimal bool xB false
 875             | x3 ⇒ couple exadecimal bool xC false
 876             | x4 ⇒ couple exadecimal bool xD false
 877             | x5 ⇒ couple exadecimal bool xE false
 878             | x6 ⇒ couple exadecimal bool xF false
 879             | x7 ⇒ couple exadecimal bool x0 true
 880             | x8 ⇒ couple exadecimal bool x1 true
 881             | x9 ⇒ couple exadecimal bool x2 true
 882             | xA ⇒ couple exadecimal bool x3 true
 883             | xB ⇒ couple exadecimal bool x4 true
 884             | xC ⇒ couple exadecimal bool x5 true
 885             | xD ⇒ couple exadecimal bool x6 true
 886             | xE ⇒ couple exadecimal bool x7 true
 887             | xF ⇒ couple exadecimal bool x8 true ]
 888        | x9 ⇒
 889            match b2 with
 890             [ x0 ⇒ couple exadecimal bool xA false
 891             | x1 ⇒ couple exadecimal bool xB false
 892             | x2 ⇒ couple exadecimal bool xC false
 893             | x3 ⇒ couple exadecimal bool xD false
 894             | x4 ⇒ couple exadecimal bool xE false
 895             | x5 ⇒ couple exadecimal bool xF false
 896             | x6 ⇒ couple exadecimal bool x0 true
 897             | x7 ⇒ couple exadecimal bool x1 true
 898             | x8 ⇒ couple exadecimal bool x2 true
 899             | x9 ⇒ couple exadecimal bool x3 true
 900             | xA ⇒ couple exadecimal bool x4 true
 901             | xB ⇒ couple exadecimal bool x5 true
 902             | xC ⇒ couple exadecimal bool x6 true
 903             | xD ⇒ couple exadecimal bool x7 true
 904             | xE ⇒ couple exadecimal bool x8 true
 905             | xF ⇒ couple exadecimal bool x9 true ]
 906        | xA ⇒
 907            match b2 with
 908             [ x0 ⇒ couple exadecimal bool xB false
 909             | x1 ⇒ couple exadecimal bool xC false
 910             | x2 ⇒ couple exadecimal bool xD false
 911             | x3 ⇒ couple exadecimal bool xE false
 912             | x4 ⇒ couple exadecimal bool xF false
 913             | x5 ⇒ couple exadecimal bool x0 true
 914             | x6 ⇒ couple exadecimal bool x1 true
 915             | x7 ⇒ couple exadecimal bool x2 true
 916             | x8 ⇒ couple exadecimal bool x3 true
 917             | x9 ⇒ couple exadecimal bool x4 true
 918             | xA ⇒ couple exadecimal bool x5 true
 919             | xB ⇒ couple exadecimal bool x6 true
 920             | xC ⇒ couple exadecimal bool x7 true
 921             | xD ⇒ couple exadecimal bool x8 true
 922             | xE ⇒ couple exadecimal bool x9 true
 923             | xF ⇒ couple exadecimal bool xA true ]
 924        | xB ⇒
 925            match b2 with
 926             [ x0 ⇒ couple exadecimal bool xC false
 927             | x1 ⇒ couple exadecimal bool xD false
 928             | x2 ⇒ couple exadecimal bool xE false
 929             | x3 ⇒ couple exadecimal bool xF false
 930             | x4 ⇒ couple exadecimal bool x0 true
 931             | x5 ⇒ couple exadecimal bool x1 true
 932             | x6 ⇒ couple exadecimal bool x2 true
 933             | x7 ⇒ couple exadecimal bool x3 true
 934             | x8 ⇒ couple exadecimal bool x4 true
 935             | x9 ⇒ couple exadecimal bool x5 true
 936             | xA ⇒ couple exadecimal bool x6 true
 937             | xB ⇒ couple exadecimal bool x7 true
 938             | xC ⇒ couple exadecimal bool x8 true
 939             | xD ⇒ couple exadecimal bool x9 true
 940             | xE ⇒ couple exadecimal bool xA true
 941             | xF ⇒ couple exadecimal bool xB true ]
 942        | xC ⇒
 943            match b2 with
 944             [ x0 ⇒ couple exadecimal bool xD false
 945             | x1 ⇒ couple exadecimal bool xE false
 946             | x2 ⇒ couple exadecimal bool xF false
 947             | x3 ⇒ couple exadecimal bool x0 true
 948             | x4 ⇒ couple exadecimal bool x1 true
 949             | x5 ⇒ couple exadecimal bool x2 true
 950             | x6 ⇒ couple exadecimal bool x3 true
 951             | x7 ⇒ couple exadecimal bool x4 true
 952             | x8 ⇒ couple exadecimal bool x5 true
 953             | x9 ⇒ couple exadecimal bool x6 true
 954             | xA ⇒ couple exadecimal bool x7 true
 955             | xB ⇒ couple exadecimal bool x8 true
 956             | xC ⇒ couple exadecimal bool x9 true
 957             | xD ⇒ couple exadecimal bool xA true
 958             | xE ⇒ couple exadecimal bool xB true
 959             | xF ⇒ couple exadecimal bool xC true ]
 960        | xD ⇒
 961            match b2 with
 962             [ x0 ⇒ couple exadecimal bool xE false
 963             | x1 ⇒ couple exadecimal bool xF false
 964             | x2 ⇒ couple exadecimal bool x0 true
 965             | x3 ⇒ couple exadecimal bool x1 true
 966             | x4 ⇒ couple exadecimal bool x2 true
 967             | x5 ⇒ couple exadecimal bool x3 true
 968             | x6 ⇒ couple exadecimal bool x4 true
 969             | x7 ⇒ couple exadecimal bool x5 true
 970             | x8 ⇒ couple exadecimal bool x6 true
 971             | x9 ⇒ couple exadecimal bool x7 true
 972             | xA ⇒ couple exadecimal bool x8 true
 973             | xB ⇒ couple exadecimal bool x9 true
 974             | xC ⇒ couple exadecimal bool xA true
 975             | xD ⇒ couple exadecimal bool xB true
 976             | xE ⇒ couple exadecimal bool xC true
 977             | xF ⇒ couple exadecimal bool xD true ]
 978        | xE ⇒
 979            match b2 with
 980             [ x0 ⇒ couple exadecimal bool xF false
 981             | x1 ⇒ couple exadecimal bool x0 true
 982             | x2 ⇒ couple exadecimal bool x1 true
 983             | x3 ⇒ couple exadecimal bool x2 true
 984             | x4 ⇒ couple exadecimal bool x3 true
 985             | x5 ⇒ couple exadecimal bool x4 true
 986             | x6 ⇒ couple exadecimal bool x5 true
 987             | x7 ⇒ couple exadecimal bool x6 true
 988             | x8 ⇒ couple exadecimal bool x7 true
 989             | x9 ⇒ couple exadecimal bool x8 true
 990             | xA ⇒ couple exadecimal bool x9 true
 991             | xB ⇒ couple exadecimal bool xA true
 992             | xC ⇒ couple exadecimal bool xB true
 993             | xD ⇒ couple exadecimal bool xC true
 994             | xE ⇒ couple exadecimal bool xD true
 995             | xF ⇒ couple exadecimal bool xE true ]
 996        | xF ⇒
 997            match b2 with
 998             [ x0 ⇒ couple exadecimal bool x0 true
 999             | x1 ⇒ couple exadecimal bool x1 true
1000             | x2 ⇒ couple exadecimal bool x2 true
1001             | x3 ⇒ couple exadecimal bool x3 true
1002             | x4 ⇒ couple exadecimal bool x4 true
1003             | x5 ⇒ couple exadecimal bool x5 true
1004             | x6 ⇒ couple exadecimal bool x6 true
1005             | x7 ⇒ couple exadecimal bool x7 true
1006             | x8 ⇒ couple exadecimal bool x8 true
1007             | x9 ⇒ couple exadecimal bool x9 true
1008             | xA ⇒ couple exadecimal bool xA true
1009             | xB ⇒ couple exadecimal bool xB true
1010             | xC ⇒ couple exadecimal bool xC true
1011             | xD ⇒ couple exadecimal bool xD true
1012             | xE ⇒ couple exadecimal bool xE true
1013             | xF ⇒ couple exadecimal bool xF true ]
1014        ]
1015    | false ⇒
1016       match b1 with
1017        [ x0 ⇒
1018            match b2 with
1019             [ x0 ⇒ couple exadecimal bool x0 false
1020             | x1 ⇒ couple exadecimal bool x1 false
1021             | x2 ⇒ couple exadecimal bool x2 false
1022             | x3 ⇒ couple exadecimal bool x3 false
1023             | x4 ⇒ couple exadecimal bool x4 false
1024             | x5 ⇒ couple exadecimal bool x5 false
1025             | x6 ⇒ couple exadecimal bool x6 false
1026             | x7 ⇒ couple exadecimal bool x7 false
1027             | x8 ⇒ couple exadecimal bool x8 false
1028             | x9 ⇒ couple exadecimal bool x9 false
1029             | xA ⇒ couple exadecimal bool xA false
1030             | xB ⇒ couple exadecimal bool xB false
1031             | xC ⇒ couple exadecimal bool xC false
1032             | xD ⇒ couple exadecimal bool xD false
1033             | xE ⇒ couple exadecimal bool xE false
1034             | xF ⇒ couple exadecimal bool xF false ]
1035        | x1 ⇒
1036            match b2 with
1037             [ x0 ⇒ couple exadecimal bool x1 false
1038             | x1 ⇒ couple exadecimal bool x2 false
1039             | x2 ⇒ couple exadecimal bool x3 false
1040             | x3 ⇒ couple exadecimal bool x4 false
1041             | x4 ⇒ couple exadecimal bool x5 false
1042             | x5 ⇒ couple exadecimal bool x6 false
1043             | x6 ⇒ couple exadecimal bool x7 false
1044             | x7 ⇒ couple exadecimal bool x8 false
1045             | x8 ⇒ couple exadecimal bool x9 false
1046             | x9 ⇒ couple exadecimal bool xA false
1047             | xA ⇒ couple exadecimal bool xB false
1048             | xB ⇒ couple exadecimal bool xC false
1049             | xC ⇒ couple exadecimal bool xD false
1050             | xD ⇒ couple exadecimal bool xE false
1051             | xE ⇒ couple exadecimal bool xF false
1052             | xF ⇒ couple exadecimal bool x0 true ]
1053        | x2 ⇒
1054            match b2 with
1055             [ x0 ⇒ couple exadecimal bool x2 false
1056             | x1 ⇒ couple exadecimal bool x3 false
1057             | x2 ⇒ couple exadecimal bool x4 false
1058             | x3 ⇒ couple exadecimal bool x5 false
1059             | x4 ⇒ couple exadecimal bool x6 false
1060             | x5 ⇒ couple exadecimal bool x7 false
1061             | x6 ⇒ couple exadecimal bool x8 false
1062             | x7 ⇒ couple exadecimal bool x9 false
1063             | x8 ⇒ couple exadecimal bool xA false
1064             | x9 ⇒ couple exadecimal bool xB false
1065             | xA ⇒ couple exadecimal bool xC false
1066             | xB ⇒ couple exadecimal bool xD false
1067             | xC ⇒ couple exadecimal bool xE false
1068             | xD ⇒ couple exadecimal bool xF false
1069             | xE ⇒ couple exadecimal bool x0 true
1070             | xF ⇒ couple exadecimal bool x1 true ]
1071        | x3 ⇒
1072            match b2 with
1073             [ x0 ⇒ couple exadecimal bool x3 false
1074             | x1 ⇒ couple exadecimal bool x4 false
1075             | x2 ⇒ couple exadecimal bool x5 false
1076             | x3 ⇒ couple exadecimal bool x6 false
1077             | x4 ⇒ couple exadecimal bool x7 false
1078             | x5 ⇒ couple exadecimal bool x8 false
1079             | x6 ⇒ couple exadecimal bool x9 false
1080             | x7 ⇒ couple exadecimal bool xA false
1081             | x8 ⇒ couple exadecimal bool xB false
1082             | x9 ⇒ couple exadecimal bool xC false
1083             | xA ⇒ couple exadecimal bool xD false
1084             | xB ⇒ couple exadecimal bool xE false
1085             | xC ⇒ couple exadecimal bool xF false
1086             | xD ⇒ couple exadecimal bool x0 true
1087             | xE ⇒ couple exadecimal bool x1 true
1088             | xF ⇒ couple exadecimal bool x2 true ]
1089        | x4 ⇒
1090            match b2 with
1091             [ x0 ⇒ couple exadecimal bool x4 false
1092             | x1 ⇒ couple exadecimal bool x5 false
1093             | x2 ⇒ couple exadecimal bool x6 false
1094             | x3 ⇒ couple exadecimal bool x7 false
1095             | x4 ⇒ couple exadecimal bool x8 false
1096             | x5 ⇒ couple exadecimal bool x9 false
1097             | x6 ⇒ couple exadecimal bool xA false
1098             | x7 ⇒ couple exadecimal bool xB false
1099             | x8 ⇒ couple exadecimal bool xC false
1100             | x9 ⇒ couple exadecimal bool xD false
1101             | xA ⇒ couple exadecimal bool xE false
1102             | xB ⇒ couple exadecimal bool xF false
1103             | xC ⇒ couple exadecimal bool x0 true
1104             | xD ⇒ couple exadecimal bool x1 true
1105             | xE ⇒ couple exadecimal bool x2 true
1106             | xF ⇒ couple exadecimal bool x3 true ]
1107        | x5 ⇒
1108            match b2 with
1109             [ x0 ⇒ couple exadecimal bool x5 false
1110             | x1 ⇒ couple exadecimal bool x6 false
1111             | x2 ⇒ couple exadecimal bool x7 false
1112             | x3 ⇒ couple exadecimal bool x8 false
1113             | x4 ⇒ couple exadecimal bool x9 false
1114             | x5 ⇒ couple exadecimal bool xA false
1115             | x6 ⇒ couple exadecimal bool xB false
1116             | x7 ⇒ couple exadecimal bool xC false
1117             | x8 ⇒ couple exadecimal bool xD false
1118             | x9 ⇒ couple exadecimal bool xE false
1119             | xA ⇒ couple exadecimal bool xF false
1120             | xB ⇒ couple exadecimal bool x0 true
1121             | xC ⇒ couple exadecimal bool x1 true
1122             | xD ⇒ couple exadecimal bool x2 true
1123             | xE ⇒ couple exadecimal bool x3 true
1124             | xF ⇒ couple exadecimal bool x4 true ]
1125        | x6 ⇒
1126            match b2 with
1127             [ x0 ⇒ couple exadecimal bool x6 false
1128             | x1 ⇒ couple exadecimal bool x7 false
1129             | x2 ⇒ couple exadecimal bool x8 false
1130             | x3 ⇒ couple exadecimal bool x9 false
1131             | x4 ⇒ couple exadecimal bool xA false
1132             | x5 ⇒ couple exadecimal bool xB false
1133             | x6 ⇒ couple exadecimal bool xC false
1134             | x7 ⇒ couple exadecimal bool xD false
1135             | x8 ⇒ couple exadecimal bool xE false
1136             | x9 ⇒ couple exadecimal bool xF false
1137             | xA ⇒ couple exadecimal bool x0 true
1138             | xB ⇒ couple exadecimal bool x1 true
1139             | xC ⇒ couple exadecimal bool x2 true
1140             | xD ⇒ couple exadecimal bool x3 true
1141             | xE ⇒ couple exadecimal bool x4 true
1142             | xF ⇒ couple exadecimal bool x5 true ]
1143        | x7 ⇒
1144            match b2 with
1145             [ x0 ⇒ couple exadecimal bool x7 false
1146             | x1 ⇒ couple exadecimal bool x8 false
1147             | x2 ⇒ couple exadecimal bool x9 false
1148             | x3 ⇒ couple exadecimal bool xA false
1149             | x4 ⇒ couple exadecimal bool xB false
1150             | x5 ⇒ couple exadecimal bool xC false
1151             | x6 ⇒ couple exadecimal bool xD false
1152             | x7 ⇒ couple exadecimal bool xE false
1153             | x8 ⇒ couple exadecimal bool xF false
1154             | x9 ⇒ couple exadecimal bool x0 true
1155             | xA ⇒ couple exadecimal bool x1 true
1156             | xB ⇒ couple exadecimal bool x2 true
1157             | xC ⇒ couple exadecimal bool x3 true
1158             | xD ⇒ couple exadecimal bool x4 true
1159             | xE ⇒ couple exadecimal bool x5 true
1160             | xF ⇒ couple exadecimal bool x6 true ]
1161        | x8 ⇒
1162            match b2 with
1163             [ x0 ⇒ couple exadecimal bool x8 false
1164             | x1 ⇒ couple exadecimal bool x9 false
1165             | x2 ⇒ couple exadecimal bool xA false
1166             | x3 ⇒ couple exadecimal bool xB false
1167             | x4 ⇒ couple exadecimal bool xC false
1168             | x5 ⇒ couple exadecimal bool xD false
1169             | x6 ⇒ couple exadecimal bool xE false
1170             | x7 ⇒ couple exadecimal bool xF false
1171             | x8 ⇒ couple exadecimal bool x0 true
1172             | x9 ⇒ couple exadecimal bool x1 true
1173             | xA ⇒ couple exadecimal bool x2 true
1174             | xB ⇒ couple exadecimal bool x3 true
1175             | xC ⇒ couple exadecimal bool x4 true
1176             | xD ⇒ couple exadecimal bool x5 true
1177             | xE ⇒ couple exadecimal bool x6 true
1178             | xF ⇒ couple exadecimal bool x7 true ]
1179        | x9 ⇒
1180            match b2 with
1181             [ x0 ⇒ couple exadecimal bool x9 false
1182             | x1 ⇒ couple exadecimal bool xA false
1183             | x2 ⇒ couple exadecimal bool xB false
1184             | x3 ⇒ couple exadecimal bool xC false
1185             | x4 ⇒ couple exadecimal bool xD false
1186             | x5 ⇒ couple exadecimal bool xE false
1187             | x6 ⇒ couple exadecimal bool xF false
1188             | x7 ⇒ couple exadecimal bool x0 true
1189             | x8 ⇒ couple exadecimal bool x1 true
1190             | x9 ⇒ couple exadecimal bool x2 true
1191             | xA ⇒ couple exadecimal bool x3 true
1192             | xB ⇒ couple exadecimal bool x4 true
1193             | xC ⇒ couple exadecimal bool x5 true
1194             | xD ⇒ couple exadecimal bool x6 true
1195             | xE ⇒ couple exadecimal bool x7 true
1196             | xF ⇒ couple exadecimal bool x8 true ]
1197        | xA ⇒
1198            match b2 with
1199             [ x0 ⇒ couple exadecimal bool xA false
1200             | x1 ⇒ couple exadecimal bool xB false
1201             | x2 ⇒ couple exadecimal bool xC false
1202             | x3 ⇒ couple exadecimal bool xD false
1203             | x4 ⇒ couple exadecimal bool xE false
1204             | x5 ⇒ couple exadecimal bool xF false
1205             | x6 ⇒ couple exadecimal bool x0 true
1206             | x7 ⇒ couple exadecimal bool x1 true
1207             | x8 ⇒ couple exadecimal bool x2 true
1208             | x9 ⇒ couple exadecimal bool x3 true
1209             | xA ⇒ couple exadecimal bool x4 true
1210             | xB ⇒ couple exadecimal bool x5 true
1211             | xC ⇒ couple exadecimal bool x6 true
1212             | xD ⇒ couple exadecimal bool x7 true
1213             | xE ⇒ couple exadecimal bool x8 true
1214             | xF ⇒ couple exadecimal bool x9 true ]
1215        | xB ⇒
1216            match b2 with
1217             [ x0 ⇒ couple exadecimal bool xB false
1218             | x1 ⇒ couple exadecimal bool xC false
1219             | x2 ⇒ couple exadecimal bool xD false
1220             | x3 ⇒ couple exadecimal bool xE false
1221             | x4 ⇒ couple exadecimal bool xF false
1222             | x5 ⇒ couple exadecimal bool x0 true
1223             | x6 ⇒ couple exadecimal bool x1 true
1224             | x7 ⇒ couple exadecimal bool x2 true
1225             | x8 ⇒ couple exadecimal bool x3 true
1226             | x9 ⇒ couple exadecimal bool x4 true
1227             | xA ⇒ couple exadecimal bool x5 true
1228             | xB ⇒ couple exadecimal bool x6 true
1229             | xC ⇒ couple exadecimal bool x7 true
1230             | xD ⇒ couple exadecimal bool x8 true
1231             | xE ⇒ couple exadecimal bool x9 true
1232             | xF ⇒ couple exadecimal bool xA true ]
1233        | xC ⇒
1234            match b2 with
1235             [ x0 ⇒ couple exadecimal bool xC false
1236             | x1 ⇒ couple exadecimal bool xD false
1237             | x2 ⇒ couple exadecimal bool xE false
1238             | x3 ⇒ couple exadecimal bool xF false
1239             | x4 ⇒ couple exadecimal bool x0 true
1240             | x5 ⇒ couple exadecimal bool x1 true
1241             | x6 ⇒ couple exadecimal bool x2 true
1242             | x7 ⇒ couple exadecimal bool x3 true
1243             | x8 ⇒ couple exadecimal bool x4 true
1244             | x9 ⇒ couple exadecimal bool x5 true
1245             | xA ⇒ couple exadecimal bool x6 true
1246             | xB ⇒ couple exadecimal bool x7 true
1247             | xC ⇒ couple exadecimal bool x8 true
1248             | xD ⇒ couple exadecimal bool x9 true
1249             | xE ⇒ couple exadecimal bool xA true
1250             | xF ⇒ couple exadecimal bool xB true ]
1251        | xD ⇒
1252            match b2 with
1253             [ x0 ⇒ couple exadecimal bool xD false
1254             | x1 ⇒ couple exadecimal bool xE false
1255             | x2 ⇒ couple exadecimal bool xF false
1256             | x3 ⇒ couple exadecimal bool x0 true
1257             | x4 ⇒ couple exadecimal bool x1 true
1258             | x5 ⇒ couple exadecimal bool x2 true
1259             | x6 ⇒ couple exadecimal bool x3 true
1260             | x7 ⇒ couple exadecimal bool x4 true
1261             | x8 ⇒ couple exadecimal bool x5 true
1262             | x9 ⇒ couple exadecimal bool x6 true
1263             | xA ⇒ couple exadecimal bool x7 true
1264             | xB ⇒ couple exadecimal bool x8 true
1265             | xC ⇒ couple exadecimal bool x9 true
1266             | xD ⇒ couple exadecimal bool xA true
1267             | xE ⇒ couple exadecimal bool xB true
1268             | xF ⇒ couple exadecimal bool xC true ]
1269        | xE ⇒
1270            match b2 with
1271             [ x0 ⇒ couple exadecimal bool xE false
1272             | x1 ⇒ couple exadecimal bool xF false
1273             | x2 ⇒ couple exadecimal bool x0 true
1274             | x3 ⇒ couple exadecimal bool x1 true
1275             | x4 ⇒ couple exadecimal bool x2 true
1276             | x5 ⇒ couple exadecimal bool x3 true
1277             | x6 ⇒ couple exadecimal bool x4 true
1278             | x7 ⇒ couple exadecimal bool x5 true
1279             | x8 ⇒ couple exadecimal bool x6 true
1280             | x9 ⇒ couple exadecimal bool x7 true
1281             | xA ⇒ couple exadecimal bool x8 true
1282             | xB ⇒ couple exadecimal bool x9 true
1283             | xC ⇒ couple exadecimal bool xA true
1284             | xD ⇒ couple exadecimal bool xB true
1285             | xE ⇒ couple exadecimal bool xC true
1286             | xF ⇒ couple exadecimal bool xD true ]
1287        | xF ⇒
1288            match b2 with
1289             [ x0 ⇒ couple exadecimal bool xF false
1290             | x1 ⇒ couple exadecimal bool x0 true
1291             | x2 ⇒ couple exadecimal bool x1 true
1292             | x3 ⇒ couple exadecimal bool x2 true
1293             | x4 ⇒ couple exadecimal bool x3 true
1294             | x5 ⇒ couple exadecimal bool x4 true
1295             | x6 ⇒ couple exadecimal bool x5 true
1296             | x7 ⇒ couple exadecimal bool x6 true
1297             | x8 ⇒ couple exadecimal bool x7 true
1298             | x9 ⇒ couple exadecimal bool x8 true
1299             | xA ⇒ couple exadecimal bool x9 true
1300             | xB ⇒ couple exadecimal bool xA true
1301             | xC ⇒ couple exadecimal bool xB true
1302             | xD ⇒ couple exadecimal bool xC true
1303             | xE ⇒ couple exadecimal bool xD true
1304             | xF ⇒ couple exadecimal bool xE true ]
1305        ]
1306    ]
1307 .
1308
1309 definition plusbyte ≝
1310  λb1,b2,c.
1311   match plusex (bl b1) (bl b2) c with
1312    [ couple l c' ⇒
1313       match plusex (bh b1) (bh b2) c' with
1314        [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
1315
1316 alias num (instance 0) = "natural number".
1317 definition nat_of_exadecimal ≝
1318  λb.
1319   match b with
1320    [ x0 ⇒ 0
1321    | x1 ⇒ 1
1322    | x2 ⇒ 2
1323    | x3 ⇒ 3
1324    | x4 ⇒ 4
1325    | x5 ⇒ 5
1326    | x6 ⇒ 6
1327    | x7 ⇒ 7
1328    | x8 ⇒ 8
1329    | x9 ⇒ 9
1330    | xA ⇒ 10
1331    | xB ⇒ 11
1332    | xC ⇒ 12
1333    | xD ⇒ 13
1334    | xE ⇒ 14
1335    | xF ⇒ 15
1336    ].
1337
1338 coercion cic:/matita/assembly/nat_of_exadecimal.con.
1339
1340 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
1341
1342 coercion cic:/matita/assembly/nat_of_byte.con.
1343
1344 let rec exadecimal_of_nat b ≝
1345   match b with [ O ⇒ x0 | S b ⇒
1346   match b with [ O ⇒ x1 | S b ⇒
1347   match b with [ O ⇒ x2 | S b ⇒
1348   match b with [ O ⇒ x3 | S b ⇒
1349   match b with [ O ⇒ x4 | S b ⇒
1350   match b with [ O ⇒ x5 | S b ⇒
1351   match b with [ O ⇒ x6 | S b ⇒
1352   match b with [ O ⇒ x7 | S b ⇒
1353   match b with [ O ⇒ x8 | S b ⇒
1354   match b with [ O ⇒ x9 | S b ⇒
1355   match b with [ O ⇒ xA | S b ⇒
1356   match b with [ O ⇒ xB | S b ⇒
1357   match b with [ O ⇒ xC | S b ⇒
1358   match b with [ O ⇒ xD | S b ⇒
1359   match b with [ O ⇒ xE | S b ⇒
1360   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
1361
1362 definition byte_of_nat ≝
1363  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
1364
1365 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
1366  intros;
1367  elim b;
1368  elim e;
1369  elim e1;
1370  reflexivity.
1371 qed.
1372
1373 axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
1374 (* intros;
1375  unfold byte_of_nat;
1376 *)
1377
1378 definition nat_of_bool ≝
1379  λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
1380
1381 (* Way too slow. Handles 2^32 goals!
1382 lemma plusbyte_ok:
1383  ∀b1,b2,c.
1384   match plusbyte b1 b2 c with
1385    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
1386    ].
1387  intros;
1388  elim c;
1389  elim b1;
1390  elim e;
1391  elim e1;
1392  elim b2;
1393  elim e2;
1394  elim e3;
1395  reflexivity.
1396 qed.
1397 *)
1398
1399 (*
1400 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1401  intros; elim n; [ reflexivity | unfold byte_of_nat.
1402 qed.
1403 *)
1404
1405 definition addr ≝ nat.
1406
1407 definition xpred ≝
1408  λb.
1409   match b with
1410    [ x0 ⇒ xF
1411    | x1 ⇒ x0
1412    | x2 ⇒ x1
1413    | x3 ⇒ x2
1414    | x4 ⇒ x3
1415    | x5 ⇒ x4
1416    | x6 ⇒ x5
1417    | x7 ⇒ x6
1418    | x8 ⇒ x7
1419    | x9 ⇒ x8
1420    | xA ⇒ x9
1421    | xB ⇒ xA
1422    | xC ⇒ xB
1423    | xD ⇒ xC
1424    | xE ⇒ xD
1425    | xF ⇒ xE ].
1426
1427 definition bpred ≝
1428  λb.
1429   match eqex (bl b) x0 with
1430    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1431    | false ⇒ mk_byte (bh b) (xpred (bl b))
1432    ].
1433
1434 (* Way too slow and subsumed by previous theorem
1435 lemma bpred_pred:
1436  ∀b.
1437   match eqbyte b (mk_byte x0 x0) with
1438    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1439    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1440  intros;
1441  elim b;
1442  elim e;
1443  elim e1;
1444  reflexivity.
1445 qed.
1446 *)
1447
1448 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1449
1450 coercion cic:/matita/assembly/addr_of_byte.con.
1451
1452 inductive opcode: Type ≝
1453    ADDd: opcode  (* 3 clock, 171 *)
1454  | BEQ: opcode   (* 3, 55 *)
1455  | BRA: opcode   (* 3, 48 *)
1456  | DECd: opcode  (* 5, 58 *)
1457  | LDAi: opcode  (* 2, 166 *)
1458  | LDAd: opcode  (* 3, 182 *)
1459  | STAd: opcode. (* 3, 183 *)
1460
1461 let rec cycles_of_opcode op : nat ≝
1462  match op with
1463   [ ADDd ⇒ 3
1464   | BEQ ⇒ 3
1465   | BRA ⇒ 3
1466   | DECd ⇒ 5
1467   | LDAi ⇒ 2
1468   | LDAd ⇒ 3
1469   | STAd ⇒ 3
1470   ].
1471
1472 definition opcodemap ≝
1473  [ couple ? ? ADDd (mk_byte xA xB);
1474    couple ? ? BEQ (mk_byte x3 x7);
1475    couple ? ? BRA (mk_byte x3 x0);
1476    couple ? ? DECd (mk_byte x3 xA);
1477    couple ? ? LDAi (mk_byte xA x6);
1478    couple ? ? LDAd (mk_byte xB x6);
1479    couple ? ? STAd (mk_byte xB x7) ].
1480
1481 definition opcode_of_byte ≝
1482  λb.
1483   let rec aux l ≝
1484    match l with
1485     [ nil ⇒ ADDd
1486     | cons c tl ⇒
1487        match c with
1488         [ couple op n ⇒
1489            match eqbyte n b with
1490             [ true ⇒ op
1491             | false ⇒ aux tl
1492             ]]]
1493   in
1494    aux opcodemap.
1495
1496 definition magic_of_opcode ≝
1497  λop1.
1498   match op1 with
1499    [ ADDd ⇒ 0
1500    | BEQ ⇒  1
1501    | BRA ⇒  2
1502    | DECd ⇒ 3
1503    | LDAi ⇒ 4
1504    | LDAd ⇒ 5
1505    | STAd ⇒ 6 ].
1506
1507 definition opcodeeqb ≝
1508  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1509
1510 definition byte_of_opcode : opcode → byte ≝
1511  λop.
1512   let rec aux l ≝
1513    match l with
1514     [ nil ⇒ mk_byte x0 x0
1515     | cons c tl ⇒
1516        match c with
1517         [ couple op' n ⇒
1518            match opcodeeqb op op' with
1519             [ true ⇒ n
1520             | false ⇒ aux tl
1521             ]]]
1522   in
1523    aux opcodemap.
1524
1525 record status : Type ≝ {
1526   acc : byte;
1527   pc  : addr;
1528   spc : addr;
1529   zf  : bool;
1530   cf  : bool;
1531   mem : addr → byte;
1532   clk : nat
1533 }.
1534
1535 definition update ≝
1536  λf: addr → byte.λa.λv.λx.
1537   match eqb x a with
1538    [ true ⇒ v
1539    | false ⇒ f x ].
1540
1541 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1542
1543 definition tick ≝
1544  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1545   let opc ≝ opcode_of_byte (mem pc) in
1546   let op1 ≝ mem (S pc) in
1547   let clk' ≝ cycles_of_opcode opc in
1548   match eqb (S clk) clk' with
1549    [ true ⇒
1550       match opc with
1551        [ ADDd ⇒
1552           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1553           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1554           let c' ≝ match res with [ couple _ c' ⇒ c'] in
1555            mk_status acc' (2 + pc) spc
1556             (eqb O (nat_of_byte acc')) c' mem 0 (* verify carrier! *)
1557        | BEQ ⇒
1558           mk_status
1559            acc
1560            (match zf with
1561              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
1562              | false ⇒ 2 + pc
1563              ])
1564            spc
1565            zf
1566            cf
1567            mem
1568            0
1569        | BRA ⇒
1570           mk_status
1571            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1572            spc
1573            zf
1574            cf
1575            mem
1576            0
1577        | DECd ⇒
1578           let x ≝ bpred (mem op1) in (* signed!!! *)
1579           let mem' ≝ update mem op1 x in
1580            mk_status acc (2 + pc) spc
1581             (eqb O x) cf mem' 0 (* check zb!!! *)
1582        | LDAi ⇒
1583           mk_status op1 (2 + pc) spc (eqb O op1) cf mem 0
1584        | LDAd ⇒
1585           let x ≝ mem op1 in
1586            mk_status x (2 + pc) spc (eqb O x) cf mem 0
1587        | STAd ⇒
1588           mk_status acc (2 + pc) spc zf cf
1589            (update mem op1 acc) 0
1590        ]
1591    | false ⇒
1592        mk_status
1593         acc pc spc zf cf mem (S clk)
1594    ]].
1595
1596 let rec execute s n on n ≝
1597  match n with
1598   [ O ⇒ s
1599   | S n' ⇒ execute (tick s) n'
1600   ].
1601
1602 lemma breakpoint:
1603  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
1604  intros;
1605  generalize in match s; clear s;
1606  elim n1;
1607   [ reflexivity
1608   | simplify;
1609     apply H;
1610   ]
1611 qed.
1612
1613 notation "hvbox(# break a)"
1614   non associative with precedence 80
1615 for @{ 'byte_of_opcode $a }.
1616 interpretation "byte_of_opcode" 'byte_of_opcode a =
1617  (cic:/matita/assembly/byte_of_opcode.con a).
1618
1619 definition mult_source : list byte ≝
1620   [#LDAi; mk_byte x0 x0; (* A := 0 *)
1621    #STAd; mk_byte x2 x0; (* Z := A *)
1622    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1623    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
1624    #LDAd; mk_byte x2 x0; (* A := Z *)
1625    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1626    #ADDd; mk_byte x1 xE; (* A += X *)
1627    #STAd; mk_byte x2 x0; (* Z := A *)
1628    #BRA;  mk_byte xF x2; (* goto l1 *)
1629    #LDAd; mk_byte x2 x0].(* (l2) *)
1630
1631 definition mult_memory ≝
1632  λx,y.λa:addr.
1633      match leb a 29 with
1634       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1635       | false ⇒
1636          match eqb a 30 with
1637           [ true ⇒ x
1638           | false ⇒ y
1639           ]
1640       ].
1641
1642 definition mult_status ≝
1643  λx,y.
1644   mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
1645
1646 lemma plusbyte_O_x:
1647  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1648  intros;
1649  elim b;
1650  elim e;
1651  elim e1;
1652  reflexivity.
1653 qed.
1654
1655 definition plusbytenc ≝
1656  λx,y.
1657   match plusbyte x y false with
1658    [couple res _ ⇒ res].
1659
1660 lemma plusbytenc_O_x:
1661  ∀x. plusbytenc (mk_byte x0 x0) x = x.
1662  intros;
1663  unfold plusbytenc;
1664  rewrite > plusbyte_O_x;
1665  reflexivity.
1666 qed.
1667
1668 lemma test_O_O:
1669   let i ≝ 14 in
1670   let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1671    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1672  normalize;
1673  split;
1674  reflexivity.
1675 qed.
1676
1677
1678 lemma test_0_2:
1679   let x ≝ mk_byte x0 x0 in
1680   let y ≝ mk_byte x0 x2 in
1681   let i ≝ 14 + 23 * nat_of_byte y in
1682   let s ≝ execute (mult_status x y) i in
1683    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1684  intros;
1685  split;
1686  reflexivity.
1687 qed.
1688
1689 lemma test_x_1:
1690  ∀x.
1691   let y ≝ mk_byte x0 x1 in
1692   let i ≝ 14 + 23 * nat_of_byte y in
1693   let s ≝ execute (mult_status x y) i in
1694    pc s = 20 ∧ mem s 32 = x.
1695  intros;
1696  split;
1697   [ reflexivity
1698   | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1699     rewrite > plusbytenc_O_x;
1700     reflexivity
1701   ].
1702 qed.
1703
1704 lemma test_x_2:
1705  ∀x.
1706   let y ≝ mk_byte x0 x2 in
1707   let i ≝ 14 + 23 * nat_of_byte y in
1708   let s ≝ execute (mult_status x y) i in
1709    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1710  intros;
1711  split;
1712   [ reflexivity
1713   | change in ⊢ (? ? % ?) with
1714      (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1715     rewrite > plusbytenc_O_x;
1716     reflexivity
1717   ].
1718 qed.
1719
1720 axiom byte_elim:
1721  ∀P:byte → Prop.
1722   (P (mk_byte x0 x0)) →
1723    (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
1724     ∀b:byte. P b.
1725 (* Tedious proof, easy to automate but not trivial
1726  intros;
1727  elim b;
1728  elim e;
1729   [ elim e1;
1730      [ assumption
1731      | apply (H1 0);
1732         [ apply lt_O_S
1733         | assumption
1734         ]
1735      | apply (H1 1);
1736         [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
1737           apply lt_S_S;
1738           apply lt_O_S
1739         | apply (H1 0);
1740 *)
1741
1742 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
1743  unfold lt;
1744  intros;
1745  autobatch.
1746 qed.
1747
1748 axiom daemon: False.
1749
1750 (*axiom loop_invariant:
1751  ∀x,y:byte.∀j:nat. j ≤ y →
1752   let s ≝ execute (mult_status x y) (5 + 23*j) in
1753    pc s = 4 ∧
1754    mem s 30 = x ∧
1755    mem s 31 = byte_of_nat (y - j) ∧
1756    mem s 32 = byte_of_nat (x * j).
1757
1758  intros 2;
1759  apply (byte_elim ? ? ? y);
1760   [ intros;
1761     simplify in H;
1762     cut (j=O);
1763      [ unfold s; clear s;
1764        rewrite > Hcut;
1765        reflexivity
1766      | (* easy *) elim daemon
1767      ]
1768   | intros;
1769     unfold s;
1770     cut (j < S i ∨ j = S i);
1771     [ elim Hcut;
1772        [ rewrite > nat_of_byte_byte_of_nat in H1;
1773          [2: apply (lt_trans ? 255);
1774              [ assumption
1775              | unfold lt;
1776                (* ???????? *)
1777              ]
1778          | generalize in match (H1 j); clear H1;
1779            intros;
1780            unfold lt in H3;
1781            cut (j ≤ i);
1782             [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro;
1783               apply H1
1784             | letin xxx ≝ H3;
1785               inversion xxx;
1786                [ intro;
1787                  rewrite > (injective_S ? ? H1);
1788                  autobatch
1789                | intros;
1790                  (* facile *) elim daemon
1791                ]
1792             ]
1793          ]
1794        |
1795        ]
1796     | (* easy *)
1797     ]
1798   ].
1799 qed.
1800 *)
1801
1802 axiom status_eq:
1803  ∀s,s'.
1804   acc s = acc s' →
1805   pc s = pc s' →
1806   spc s = spc s' →
1807   zf s = zf s' →
1808   cf s = cf s' →
1809   (∀a. mem s a = mem s' a) →
1810   clk s = clk s' →
1811    s=s'.
1812 (*
1813 lemma loop_invariant':
1814  ∀x,y:byte.∀j:nat. j ≤ y →
1815   execute (mult_status x y) (5 + 23*j)
1816    =
1817     mk_status (byte_of_nat (x * j)) 4 0 true false
1818      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
1819       (byte_of_nat (x * j)))
1820      0.
1821  intros 3;
1822  elim j;
1823   [ do 2 (rewrite < times_n_O);
1824     apply status_eq;
1825     [1,2,3,4,5,7: normalize; reflexivity
1826     | intro;
1827       elim daemon
1828     ]
1829   | cut (5 + 23 * S n = 5 + 23 * n + 23);
1830     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
1831       letin H' ≝ (H ?); clearbody H'; clear H;
1832       [ autobatch
1833       | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
1834         clear Hcut;
1835         rewrite > xxx;
1836         clear xxx;
1837         apply (transitive_eq ? ? ? ? K);
1838         clear K;
1839         rewrite > H';
1840         clear H';
1841         TO BE FINISHED;
1842       ]
1843     | autobatch paramodulation
1844     ]
1845   ]
1846 (*
1847  intros 2;
1848  apply (byte_elim ? ? ? y);
1849   [ intros;
1850     simplify in H;
1851     generalize in match (le_n_O_to_eq ? H); intro;
1852     unfold s; clear s;
1853     rewrite < H1;
1854     rewrite < times_n_O;
1855     rewrite < times_n_O;
1856     apply status_eq;
1857      [1,2,3,4,5,7: normalize; reflexivity
1858      | intros;
1859        whd in ⊢ (? ? % %);
1860        normalize in ⊢ (? ? match ? ? % in bool return ? with [true\rArr ?|false\rArr ?] ?);
1861        elim (eqb a 32) in ⊢ (? ? % match % in bool return ? with [true\rArr ?|false\rArr ?]);
1862        simplify;
1863         [ reflexivity
1864         | whd in ⊢ (? ? % %);
1865           elim daemon
1866         ]
1867      ]
1868   | intros;
1869     cut (j = byte_of_nat (S i) ∨ j ≤ byte_of_nat i);
1870   ].
1871 *)
1872 qed.
1873
1874 theorem test_x_y:
1875  ∀x,y.
1876   let i ≝ 14 + 23 * nat_of_byte y in
1877   let s ≝ execute (mult_status x y) i in
1878    pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
1879  intros;
1880  generalize in match (loop_invariant' x y y (le_n y)); intro;
1881  generalize in match (breakpoint (mult_status x y) (5 + 23*y) 9); intro;
1882  cut (5 + 23*y +9 = 14 + 23* y);
1883   [2: autobatch paramodulation
1884   | rewrite > Hcut in H1;
1885     change in H1:(? ? % ?) with s;
1886     letin s0 ≝ (execute (mult_status x y) (S (S (S (S (S O))))+S 22*y));
1887     generalize in match H; intro K; clear H;
1888     change in K with
1889      (s0 =
1890       mk_status (byte_of_nat (x*y)) 4 0 true false
1891        (update
1892         (update
1893          (update (mult_memory x y) 30 x)
1894          31 (byte_of_nat (y-y)))
1895          32 (byte_of_nat (x*y))) O);
1896     clear Hcut;
1897     generalize in match H1; intro K1; clear H1;
1898     change in K1 with (s = execute s0 9);
1899     rewrite > K in K1;
1900     clear K; clear s0; clearbody s; clear i;
1901     rewrite < minus_n_n in K1;
1902     split;
1903     rewrite > K1;
1904     reflexivity
1905   ]
1906 qed.
1907
1908 (*
1909  letin w ≝ 22;
1910  letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc;
1911  letin acc' ≝ (acc (execute (mult_status x y) w));
1912  normalize in acc';
1913  change in acc' with x;
1914  letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z;
1915  letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x;
1916  (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*)
1917  split;
1918   [ normalize; reflexivity
1919   | change with (byte_of_nat x = x);
1920  normalize;
1921  split;
1922   [ reflexivity
1923   | change with (byte_of_nat (x + 0));
1924  letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www;
1925  letin xxx ≝ (260 \mod 256); reduce in xxx;
1926  letin xxx ≝ ((18 + 242) \mod 256);
1927  whd in xxx;
1928  letin pc' ≝ (pc s);
1929  normalize in pc';
1930  letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s)));
1931  normalize in opcode;
1932  csc.
1933  split;
1934  reduce in s;
1935  reflexivity.
1936 qed.
1937
1938 lemma goo1:
1939  ∀x,y.
1940   let i ≝ 14 + 23 * nat_of_byte y in
1941   let s ≝ execute (mult_status x y) i in
1942    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
1943  intros;
1944 qed.
1945
1946 lemma goo: True.
1947  letin s0 ≝ mult_status;
1948  letin pc0 ≝ (pc s0);
1949  reduce in pc0;
1950  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
1951  reduce in i0;
1952
1953  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
1954  letin pc1 ≝ (pc s1);
1955  reduce in pc1;
1956  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
1957  reduce in i1;
1958
1959  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
1960  letin pc2 ≝ (pc s2);
1961  reduce in pc2;
1962  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
1963  reduce in i2;
1964
1965  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
1966  letin pc3 ≝ (pc s3);
1967  reduce in pc3;
1968  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
1969  reduce in i3;
1970  letin zf3 ≝ (zf s3);
1971  reduce in zf3;
1972
1973  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
1974  letin pc4 ≝ (pc s4);
1975  reduce in pc4;
1976  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
1977  reduce in i4;
1978
1979  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
1980  letin pc5 ≝ (pc s5);
1981  reduce in pc5;
1982  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
1983  reduce in i5;
1984
1985  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
1986  letin pc6 ≝ (pc s6);
1987  reduce in pc6;
1988  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
1989  reduce in i6;
1990
1991  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
1992  letin pc7 ≝ (pc s7);
1993  reduce in pc7;
1994  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
1995  reduce in i7;
1996
1997  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
1998  letin pc8 ≝ (pc s8);
1999  reduce in pc8;
2000  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
2001  reduce in i8;
2002
2003  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
2004  letin pc9 ≝ (pc s9);
2005  reduce in pc9;
2006  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
2007  reduce in i9;
2008
2009  exact I.
2010 qed.
2011 *)*)