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 "30" non associative with precedence 80 for @{ 'x30 }.
  65 interpretation "natural number" 'x30 =
  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/1)))))))))))))))))))))))))))))))).
  97
  98 notation "31" non associative with precedence 80 for @{ 'x31 }.
  99 interpretation "natural number" 'x31 =
 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/1))))))))))))))))))))))))))))))))).
 132
 133 notation "32" non associative with precedence 80 for @{ 'x32 }.
 134 interpretation "natural number" 'x32 =
 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/1)))))))))))))))))))))))))))))))))).
 168
 169 notation "255" non associative with precedence 80 for @{ 'x255 }.
 170 interpretation "natural number" 'x255 =
 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/2)
 323 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 324 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 325 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 326 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 327 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 328 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 329 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 330 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 331 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 332 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 333 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 334 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 335 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 336 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 337 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 338 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 339 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 340 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 341 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 342 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 343 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 344 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 345 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 346 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 347 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 348 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 349 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 350 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 351 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 352 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 353 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 354 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 355 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 356 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 357 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 358 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 359 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 360 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 361 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 362 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 363 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 364 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 365 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 366 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 367 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 368 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 369 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 370 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 371 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 372 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 373 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 374 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 375 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 376 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 377 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 378 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 379 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 380 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 381 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 382 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 383 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 384 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 385 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 386 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 387 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 388 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 389 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 390 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 391 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 392 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 393 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 394 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 395 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 396 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 397 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 398 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 399 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 400 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 401 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 402 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 403 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 404 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 405 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 406 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 407 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 408 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 409 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 410 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 411 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 412 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 413 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 414 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 415 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 416 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 417 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 418 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 419 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 420 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 421 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 422 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 423 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 424 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 425 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 426 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
 427 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 428 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 429 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 430 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
 431
 432 notation "256" non associative with precedence 80 for @{ 'x256 }.
 433 interpretation "natural number" 'x256 =
 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/2)
 586 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 587 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 588 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 589 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 590 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 591 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 592 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 593 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 594 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 595 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 596 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 597 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 598 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 599 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 600 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 601 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 602 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 603 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 604 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 605 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 606 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 607 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 608 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 609 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 610 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 611 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 612 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 613 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 614 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 615 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 616 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 617 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 618 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 619 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 620 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 621 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 622 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 623 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 624 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 625 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 626 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 627 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 628 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 629 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 630 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 631 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 632 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 633 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 634 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 635 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 636 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 637 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 638 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 639 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 640 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 641 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 642 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 643 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 644 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 645 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 646 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 647 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 648 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 649 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 650 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 651 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 652 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 653 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 654 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 655 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 656 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 657 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 658 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 659 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 660 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 661 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 662 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 663 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 664 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 665 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 666 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 667 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 668 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 669 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 670 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 671 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 672 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 673 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 674 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 675 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 676 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 677 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 678 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 679 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 680 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 681 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 682 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 683 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 684 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 685 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 686 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 687 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 688 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 689 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
 690 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
 691 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 692 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 693 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 694 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
 695
 696 inductive exadecimal : Type ≝
 697    x0: exadecimal
 698  | x1: exadecimal
 699  | x2: exadecimal
 700  | x3: exadecimal
 701  | x4: exadecimal
 702  | x5: exadecimal
 703  | x6: exadecimal
 704  | x7: exadecimal
 705  | x8: exadecimal
 706  | x9: exadecimal
 707  | xA: exadecimal
 708  | xB: exadecimal
 709  | xC: exadecimal
 710  | xD: exadecimal
 711  | xE: exadecimal
 712  | xF: exadecimal.
 713
 714 record byte : Type ≝ {
 715  bh: exadecimal;
 716  bl: exadecimal
 717 }.
 718
 719 definition eqex ≝
 720  λb1,b2.
 721   match b1 with
 722    [ x0 ⇒
 723        match b2 with
 724         [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 725         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 726         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 727         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 728    | x1 ⇒
 729        match b2 with
 730         [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
 731         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 732         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 733         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 734    | x2 ⇒
 735        match b2 with
 736         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
 737         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 738         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 739         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 740    | x3 ⇒
 741        match b2 with
 742         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
 743         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 744         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 745         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 746    | x4 ⇒
 747        match b2 with
 748         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 749         | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 750         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 751         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 752    | x5 ⇒
 753        match b2 with
 754         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 755         | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
 756         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 757         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 758    | x6 ⇒
 759        match b2 with
 760         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 761         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
 762         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 763         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 764    | x7 ⇒
 765        match b2 with
 766         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 767         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
 768         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 769         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 770    | x8 ⇒
 771        match b2 with
 772         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 773         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 774         | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 775         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 776    | x9 ⇒
 777        match b2 with
 778         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 779         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 780         | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
 781         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 782    | xA ⇒
 783        match b2 with
 784         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 785         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 786         | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
 787         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 788    | xB ⇒
 789        match b2 with
 790         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 791         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 792         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
 793         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 794    | xC ⇒
 795        match b2 with
 796         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 797         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 798         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 799         | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
 800    | xD ⇒
 801        match b2 with
 802         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 803         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 804         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 805         | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
 806    | xE ⇒
 807        match b2 with
 808         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 809         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 810         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 811         | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ]
 812    | xF ⇒
 813        match b2 with
 814         [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
 815         | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
 816         | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
 817         | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]].
 818
 819
 820 definition eqbyte ≝
 821  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 822
 823 inductive cartesian_product (A,B: Type) : Type ≝
 824  couple: ∀a:A.∀b:B. cartesian_product A B.
 825
 826 definition plusex ≝
 827  λb1,b2,c.
 828   match c with
 829    [ true ⇒
 830       match b1 with
 831        [ x0 ⇒
 832            match b2 with
 833             [ x0 ⇒ couple exadecimal bool x1 false
 834             | x1 ⇒ couple exadecimal bool x2 false
 835             | x2 ⇒ couple exadecimal bool x3 false
 836             | x3 ⇒ couple exadecimal bool x4 false
 837             | x4 ⇒ couple exadecimal bool x5 false
 838             | x5 ⇒ couple exadecimal bool x6 false
 839             | x6 ⇒ couple exadecimal bool x7 false
 840             | x7 ⇒ couple exadecimal bool x8 false
 841             | x8 ⇒ couple exadecimal bool x9 false
 842             | x9 ⇒ couple exadecimal bool xA false
 843             | xA ⇒ couple exadecimal bool xB false
 844             | xB ⇒ couple exadecimal bool xC false
 845             | xC ⇒ couple exadecimal bool xD false
 846             | xD ⇒ couple exadecimal bool xE false
 847             | xE ⇒ couple exadecimal bool xF false
 848             | xF ⇒ couple exadecimal bool x0 true ]
 849        | x1 ⇒
 850            match b2 with
 851             [ x0 ⇒ couple exadecimal bool x2 false
 852             | x1 ⇒ couple exadecimal bool x3 false
 853             | x2 ⇒ couple exadecimal bool x4 false
 854             | x3 ⇒ couple exadecimal bool x5 false
 855             | x4 ⇒ couple exadecimal bool x6 false
 856             | x5 ⇒ couple exadecimal bool x7 false
 857             | x6 ⇒ couple exadecimal bool x8 false
 858             | x7 ⇒ couple exadecimal bool x9 false
 859             | x8 ⇒ couple exadecimal bool xA false
 860             | x9 ⇒ couple exadecimal bool xB false
 861             | xA ⇒ couple exadecimal bool xC false
 862             | xB ⇒ couple exadecimal bool xD false
 863             | xC ⇒ couple exadecimal bool xE false
 864             | xD ⇒ couple exadecimal bool xF false
 865             | xE ⇒ couple exadecimal bool x0 true
 866             | xF ⇒ couple exadecimal bool x1 true ]
 867        | x2 ⇒
 868            match b2 with
 869             [ x0 ⇒ couple exadecimal bool x3 false
 870             | x1 ⇒ couple exadecimal bool x4 false
 871             | x2 ⇒ couple exadecimal bool x5 false
 872             | x3 ⇒ couple exadecimal bool x6 false
 873             | x4 ⇒ couple exadecimal bool x7 false
 874             | x5 ⇒ couple exadecimal bool x8 false
 875             | x6 ⇒ couple exadecimal bool x9 false
 876             | x7 ⇒ couple exadecimal bool xA false
 877             | x8 ⇒ couple exadecimal bool xB false
 878             | x9 ⇒ couple exadecimal bool xC false
 879             | xA ⇒ couple exadecimal bool xD false
 880             | xB ⇒ couple exadecimal bool xE false
 881             | xC ⇒ couple exadecimal bool xF false
 882             | xD ⇒ couple exadecimal bool x0 true
 883             | xE ⇒ couple exadecimal bool x1 true
 884             | xF ⇒ couple exadecimal bool x2 true ]
 885        | x3 ⇒
 886            match b2 with
 887             [ x0 ⇒ couple exadecimal bool x4 false
 888             | x1 ⇒ couple exadecimal bool x5 false
 889             | x2 ⇒ couple exadecimal bool x6 false
 890             | x3 ⇒ couple exadecimal bool x7 false
 891             | x4 ⇒ couple exadecimal bool x8 false
 892             | x5 ⇒ couple exadecimal bool x9 false
 893             | x6 ⇒ couple exadecimal bool xA false
 894             | x7 ⇒ couple exadecimal bool xB false
 895             | x8 ⇒ couple exadecimal bool xC false
 896             | x9 ⇒ couple exadecimal bool xD false
 897             | xA ⇒ couple exadecimal bool xE false
 898             | xB ⇒ couple exadecimal bool xF false
 899             | xC ⇒ couple exadecimal bool x0 true
 900             | xD ⇒ couple exadecimal bool x1 true
 901             | xE ⇒ couple exadecimal bool x2 true
 902             | xF ⇒ couple exadecimal bool x3 true ]
 903        | x4 ⇒
 904            match b2 with
 905             [ x0 ⇒ couple exadecimal bool x5 false
 906             | x1 ⇒ couple exadecimal bool x6 false
 907             | x2 ⇒ couple exadecimal bool x7 false
 908             | x3 ⇒ couple exadecimal bool x8 false
 909             | x4 ⇒ couple exadecimal bool x9 false
 910             | x5 ⇒ couple exadecimal bool xA false
 911             | x6 ⇒ couple exadecimal bool xB false
 912             | x7 ⇒ couple exadecimal bool xC false
 913             | x8 ⇒ couple exadecimal bool xD false
 914             | x9 ⇒ couple exadecimal bool xE false
 915             | xA ⇒ couple exadecimal bool xF false
 916             | xB ⇒ couple exadecimal bool x0 true
 917             | xC ⇒ couple exadecimal bool x1 true
 918             | xD ⇒ couple exadecimal bool x2 true
 919             | xE ⇒ couple exadecimal bool x3 true
 920             | xF ⇒ couple exadecimal bool x4 true ]
 921        | x5 ⇒
 922            match b2 with
 923             [ x0 ⇒ couple exadecimal bool x6 false
 924             | x1 ⇒ couple exadecimal bool x7 false
 925             | x2 ⇒ couple exadecimal bool x8 false
 926             | x3 ⇒ couple exadecimal bool x9 false
 927             | x4 ⇒ couple exadecimal bool xA false
 928             | x5 ⇒ couple exadecimal bool xB false
 929             | x6 ⇒ couple exadecimal bool xC false
 930             | x7 ⇒ couple exadecimal bool xD false
 931             | x8 ⇒ couple exadecimal bool xE false
 932             | x9 ⇒ couple exadecimal bool xF false
 933             | xA ⇒ couple exadecimal bool x0 true
 934             | xB ⇒ couple exadecimal bool x1 true
 935             | xC ⇒ couple exadecimal bool x2 true
 936             | xD ⇒ couple exadecimal bool x3 true
 937             | xE ⇒ couple exadecimal bool x4 true
 938             | xF ⇒ couple exadecimal bool x5 true ]
 939        | x6 ⇒
 940            match b2 with
 941             [ x0 ⇒ couple exadecimal bool x7 false
 942             | x1 ⇒ couple exadecimal bool x8 false
 943             | x2 ⇒ couple exadecimal bool x9 false
 944             | x3 ⇒ couple exadecimal bool xA false
 945             | x4 ⇒ couple exadecimal bool xB false
 946             | x5 ⇒ couple exadecimal bool xC false
 947             | x6 ⇒ couple exadecimal bool xD false
 948             | x7 ⇒ couple exadecimal bool xE false
 949             | x8 ⇒ couple exadecimal bool xF false
 950             | x9 ⇒ couple exadecimal bool x0 true
 951             | xA ⇒ couple exadecimal bool x1 true
 952             | xB ⇒ couple exadecimal bool x2 true
 953             | xC ⇒ couple exadecimal bool x3 true
 954             | xD ⇒ couple exadecimal bool x4 true
 955             | xE ⇒ couple exadecimal bool x5 true
 956             | xF ⇒ couple exadecimal bool x6 true ]
 957        | x7 ⇒
 958            match b2 with
 959             [ x0 ⇒ couple exadecimal bool x8 false
 960             | x1 ⇒ couple exadecimal bool x9 false
 961             | x2 ⇒ couple exadecimal bool xA false
 962             | x3 ⇒ couple exadecimal bool xB false
 963             | x4 ⇒ couple exadecimal bool xC false
 964             | x5 ⇒ couple exadecimal bool xD false
 965             | x6 ⇒ couple exadecimal bool xE false
 966             | x7 ⇒ couple exadecimal bool xF false
 967             | x8 ⇒ couple exadecimal bool x0 true
 968             | x9 ⇒ couple exadecimal bool x1 true
 969             | xA ⇒ couple exadecimal bool x2 true
 970             | xB ⇒ couple exadecimal bool x3 true
 971             | xC ⇒ couple exadecimal bool x4 true
 972             | xD ⇒ couple exadecimal bool x5 true
 973             | xE ⇒ couple exadecimal bool x6 true
 974             | xF ⇒ couple exadecimal bool x7 true ]
 975        | x8 ⇒
 976            match b2 with
 977             [ x0 ⇒ couple exadecimal bool x9 false
 978             | x1 ⇒ couple exadecimal bool xA false
 979             | x2 ⇒ couple exadecimal bool xB false
 980             | x3 ⇒ couple exadecimal bool xC false
 981             | x4 ⇒ couple exadecimal bool xD false
 982             | x5 ⇒ couple exadecimal bool xE false
 983             | x6 ⇒ couple exadecimal bool xF false
 984             | x7 ⇒ couple exadecimal bool x0 true
 985             | x8 ⇒ couple exadecimal bool x1 true
 986             | x9 ⇒ couple exadecimal bool x2 true
 987             | xA ⇒ couple exadecimal bool x3 true
 988             | xB ⇒ couple exadecimal bool x4 true
 989             | xC ⇒ couple exadecimal bool x5 true
 990             | xD ⇒ couple exadecimal bool x6 true
 991             | xE ⇒ couple exadecimal bool x7 true
 992             | xF ⇒ couple exadecimal bool x8 true ]
 993        | x9 ⇒
 994            match b2 with
 995             [ x0 ⇒ couple exadecimal bool xA false
 996             | x1 ⇒ couple exadecimal bool xB false
 997             | x2 ⇒ couple exadecimal bool xC false
 998             | x3 ⇒ couple exadecimal bool xD false
 999             | x4 ⇒ couple exadecimal bool xE false
1000             | x5 ⇒ couple exadecimal bool xF false
1001             | x6 ⇒ couple exadecimal bool x0 true
1002             | x7 ⇒ couple exadecimal bool x1 true
1003             | x8 ⇒ couple exadecimal bool x2 true
1004             | x9 ⇒ couple exadecimal bool x3 true
1005             | xA ⇒ couple exadecimal bool x4 true
1006             | xB ⇒ couple exadecimal bool x5 true
1007             | xC ⇒ couple exadecimal bool x6 true
1008             | xD ⇒ couple exadecimal bool x7 true
1009             | xE ⇒ couple exadecimal bool x8 true
1010             | xF ⇒ couple exadecimal bool x9 true ]
1011        | xA ⇒
1012            match b2 with
1013             [ x0 ⇒ couple exadecimal bool xB false
1014             | x1 ⇒ couple exadecimal bool xC false
1015             | x2 ⇒ couple exadecimal bool xD false
1016             | x3 ⇒ couple exadecimal bool xE false
1017             | x4 ⇒ couple exadecimal bool xF false
1018             | x5 ⇒ couple exadecimal bool x0 true
1019             | x6 ⇒ couple exadecimal bool x1 true
1020             | x7 ⇒ couple exadecimal bool x2 true
1021             | x8 ⇒ couple exadecimal bool x3 true
1022             | x9 ⇒ couple exadecimal bool x4 true
1023             | xA ⇒ couple exadecimal bool x5 true
1024             | xB ⇒ couple exadecimal bool x6 true
1025             | xC ⇒ couple exadecimal bool x7 true
1026             | xD ⇒ couple exadecimal bool x8 true
1027             | xE ⇒ couple exadecimal bool x9 true
1028             | xF ⇒ couple exadecimal bool xA true ]
1029        | xB ⇒
1030            match b2 with
1031             [ x0 ⇒ couple exadecimal bool xC false
1032             | x1 ⇒ couple exadecimal bool xD false
1033             | x2 ⇒ couple exadecimal bool xE false
1034             | x3 ⇒ couple exadecimal bool xF false
1035             | x4 ⇒ couple exadecimal bool x0 true
1036             | x5 ⇒ couple exadecimal bool x1 true
1037             | x6 ⇒ couple exadecimal bool x2 true
1038             | x7 ⇒ couple exadecimal bool x3 true
1039             | x8 ⇒ couple exadecimal bool x4 true
1040             | x9 ⇒ couple exadecimal bool x5 true
1041             | xA ⇒ couple exadecimal bool x6 true
1042             | xB ⇒ couple exadecimal bool x7 true
1043             | xC ⇒ couple exadecimal bool x8 true
1044             | xD ⇒ couple exadecimal bool x9 true
1045             | xE ⇒ couple exadecimal bool xA true
1046             | xF ⇒ couple exadecimal bool xB true ]
1047        | xC ⇒
1048            match b2 with
1049             [ x0 ⇒ couple exadecimal bool xD false
1050             | x1 ⇒ couple exadecimal bool xE false
1051             | x2 ⇒ couple exadecimal bool xF false
1052             | x3 ⇒ couple exadecimal bool x0 true
1053             | x4 ⇒ couple exadecimal bool x1 true
1054             | x5 ⇒ couple exadecimal bool x2 true
1055             | x6 ⇒ couple exadecimal bool x3 true
1056             | x7 ⇒ couple exadecimal bool x4 true
1057             | x8 ⇒ couple exadecimal bool x5 true
1058             | x9 ⇒ couple exadecimal bool x6 true
1059             | xA ⇒ couple exadecimal bool x7 true
1060             | xB ⇒ couple exadecimal bool x8 true
1061             | xC ⇒ couple exadecimal bool x9 true
1062             | xD ⇒ couple exadecimal bool xA true
1063             | xE ⇒ couple exadecimal bool xB true
1064             | xF ⇒ couple exadecimal bool xC true ]
1065        | xD ⇒
1066            match b2 with
1067             [ x0 ⇒ couple exadecimal bool xE false
1068             | x1 ⇒ couple exadecimal bool xF false
1069             | x2 ⇒ couple exadecimal bool x0 true
1070             | x3 ⇒ couple exadecimal bool x1 true
1071             | x4 ⇒ couple exadecimal bool x2 true
1072             | x5 ⇒ couple exadecimal bool x3 true
1073             | x6 ⇒ couple exadecimal bool x4 true
1074             | x7 ⇒ couple exadecimal bool x5 true
1075             | x8 ⇒ couple exadecimal bool x6 true
1076             | x9 ⇒ couple exadecimal bool x7 true
1077             | xA ⇒ couple exadecimal bool x8 true
1078             | xB ⇒ couple exadecimal bool x9 true
1079             | xC ⇒ couple exadecimal bool xA true
1080             | xD ⇒ couple exadecimal bool xB true
1081             | xE ⇒ couple exadecimal bool xC true
1082             | xF ⇒ couple exadecimal bool xD true ]
1083        | xE ⇒
1084            match b2 with
1085             [ x0 ⇒ couple exadecimal bool xF false
1086             | x1 ⇒ couple exadecimal bool x0 true
1087             | x2 ⇒ couple exadecimal bool x1 true
1088             | x3 ⇒ couple exadecimal bool x2 true
1089             | x4 ⇒ couple exadecimal bool x3 true
1090             | x5 ⇒ couple exadecimal bool x4 true
1091             | x6 ⇒ couple exadecimal bool x5 true
1092             | x7 ⇒ couple exadecimal bool x6 true
1093             | x8 ⇒ couple exadecimal bool x7 true
1094             | x9 ⇒ couple exadecimal bool x8 true
1095             | xA ⇒ couple exadecimal bool x9 true
1096             | xB ⇒ couple exadecimal bool xA true
1097             | xC ⇒ couple exadecimal bool xB true
1098             | xD ⇒ couple exadecimal bool xC true
1099             | xE ⇒ couple exadecimal bool xD true
1100             | xF ⇒ couple exadecimal bool xE true ]
1101        | xF ⇒
1102            match b2 with
1103             [ x0 ⇒ couple exadecimal bool x0 true
1104             | x1 ⇒ couple exadecimal bool x1 true
1105             | x2 ⇒ couple exadecimal bool x2 true
1106             | x3 ⇒ couple exadecimal bool x3 true
1107             | x4 ⇒ couple exadecimal bool x4 true
1108             | x5 ⇒ couple exadecimal bool x5 true
1109             | x6 ⇒ couple exadecimal bool x6 true
1110             | x7 ⇒ couple exadecimal bool x7 true
1111             | x8 ⇒ couple exadecimal bool x8 true
1112             | x9 ⇒ couple exadecimal bool x9 true
1113             | xA ⇒ couple exadecimal bool xA true
1114             | xB ⇒ couple exadecimal bool xB true
1115             | xC ⇒ couple exadecimal bool xC true
1116             | xD ⇒ couple exadecimal bool xD true
1117             | xE ⇒ couple exadecimal bool xE true
1118             | xF ⇒ couple exadecimal bool xF true ]
1119        ]
1120    | false ⇒
1121       match b1 with
1122        [ x0 ⇒
1123            match b2 with
1124             [ x0 ⇒ couple exadecimal bool x0 false
1125             | x1 ⇒ couple exadecimal bool x1 false
1126             | x2 ⇒ couple exadecimal bool x2 false
1127             | x3 ⇒ couple exadecimal bool x3 false
1128             | x4 ⇒ couple exadecimal bool x4 false
1129             | x5 ⇒ couple exadecimal bool x5 false
1130             | x6 ⇒ couple exadecimal bool x6 false
1131             | x7 ⇒ couple exadecimal bool x7 false
1132             | x8 ⇒ couple exadecimal bool x8 false
1133             | x9 ⇒ couple exadecimal bool x9 false
1134             | xA ⇒ couple exadecimal bool xA false
1135             | xB ⇒ couple exadecimal bool xB false
1136             | xC ⇒ couple exadecimal bool xC false
1137             | xD ⇒ couple exadecimal bool xD false
1138             | xE ⇒ couple exadecimal bool xE false
1139             | xF ⇒ couple exadecimal bool xF false ]
1140        | x1 ⇒
1141            match b2 with
1142             [ x0 ⇒ couple exadecimal bool x1 false
1143             | x1 ⇒ couple exadecimal bool x2 false
1144             | x2 ⇒ couple exadecimal bool x3 false
1145             | x3 ⇒ couple exadecimal bool x4 false
1146             | x4 ⇒ couple exadecimal bool x5 false
1147             | x5 ⇒ couple exadecimal bool x6 false
1148             | x6 ⇒ couple exadecimal bool x7 false
1149             | x7 ⇒ couple exadecimal bool x8 false
1150             | x8 ⇒ couple exadecimal bool x9 false
1151             | x9 ⇒ couple exadecimal bool xA false
1152             | xA ⇒ couple exadecimal bool xB false
1153             | xB ⇒ couple exadecimal bool xC false
1154             | xC ⇒ couple exadecimal bool xD false
1155             | xD ⇒ couple exadecimal bool xE false
1156             | xE ⇒ couple exadecimal bool xF false
1157             | xF ⇒ couple exadecimal bool x0 true ]
1158        | x2 ⇒
1159            match b2 with
1160             [ x0 ⇒ couple exadecimal bool x2 false
1161             | x1 ⇒ couple exadecimal bool x3 false
1162             | x2 ⇒ couple exadecimal bool x4 false
1163             | x3 ⇒ couple exadecimal bool x5 false
1164             | x4 ⇒ couple exadecimal bool x6 false
1165             | x5 ⇒ couple exadecimal bool x7 false
1166             | x6 ⇒ couple exadecimal bool x8 false
1167             | x7 ⇒ couple exadecimal bool x9 false
1168             | x8 ⇒ couple exadecimal bool xA false
1169             | x9 ⇒ couple exadecimal bool xB false
1170             | xA ⇒ couple exadecimal bool xC false
1171             | xB ⇒ couple exadecimal bool xD false
1172             | xC ⇒ couple exadecimal bool xE false
1173             | xD ⇒ couple exadecimal bool xF false
1174             | xE ⇒ couple exadecimal bool x0 true
1175             | xF ⇒ couple exadecimal bool x1 true ]
1176        | x3 ⇒
1177            match b2 with
1178             [ x0 ⇒ couple exadecimal bool x3 false
1179             | x1 ⇒ couple exadecimal bool x4 false
1180             | x2 ⇒ couple exadecimal bool x5 false
1181             | x3 ⇒ couple exadecimal bool x6 false
1182             | x4 ⇒ couple exadecimal bool x7 false
1183             | x5 ⇒ couple exadecimal bool x8 false
1184             | x6 ⇒ couple exadecimal bool x9 false
1185             | x7 ⇒ couple exadecimal bool xA false
1186             | x8 ⇒ couple exadecimal bool xB false
1187             | x9 ⇒ couple exadecimal bool xC false
1188             | xA ⇒ couple exadecimal bool xD false
1189             | xB ⇒ couple exadecimal bool xE false
1190             | xC ⇒ couple exadecimal bool xF false
1191             | xD ⇒ couple exadecimal bool x0 true
1192             | xE ⇒ couple exadecimal bool x1 true
1193             | xF ⇒ couple exadecimal bool x2 true ]
1194        | x4 ⇒
1195            match b2 with
1196             [ x0 ⇒ couple exadecimal bool x4 false
1197             | x1 ⇒ couple exadecimal bool x5 false
1198             | x2 ⇒ couple exadecimal bool x6 false
1199             | x3 ⇒ couple exadecimal bool x7 false
1200             | x4 ⇒ couple exadecimal bool x8 false
1201             | x5 ⇒ couple exadecimal bool x9 false
1202             | x6 ⇒ couple exadecimal bool xA false
1203             | x7 ⇒ couple exadecimal bool xB false
1204             | x8 ⇒ couple exadecimal bool xC false
1205             | x9 ⇒ couple exadecimal bool xD false
1206             | xA ⇒ couple exadecimal bool xE false
1207             | xB ⇒ couple exadecimal bool xF false
1208             | xC ⇒ couple exadecimal bool x0 true
1209             | xD ⇒ couple exadecimal bool x1 true
1210             | xE ⇒ couple exadecimal bool x2 true
1211             | xF ⇒ couple exadecimal bool x3 true ]
1212        | x5 ⇒
1213            match b2 with
1214             [ x0 ⇒ couple exadecimal bool x5 false
1215             | x1 ⇒ couple exadecimal bool x6 false
1216             | x2 ⇒ couple exadecimal bool x7 false
1217             | x3 ⇒ couple exadecimal bool x8 false
1218             | x4 ⇒ couple exadecimal bool x9 false
1219             | x5 ⇒ couple exadecimal bool xA false
1220             | x6 ⇒ couple exadecimal bool xB false
1221             | x7 ⇒ couple exadecimal bool xC false
1222             | x8 ⇒ couple exadecimal bool xD false
1223             | x9 ⇒ couple exadecimal bool xE false
1224             | xA ⇒ couple exadecimal bool xF false
1225             | xB ⇒ couple exadecimal bool x0 true
1226             | xC ⇒ couple exadecimal bool x1 true
1227             | xD ⇒ couple exadecimal bool x2 true
1228             | xE ⇒ couple exadecimal bool x3 true
1229             | xF ⇒ couple exadecimal bool x4 true ]
1230        | x6 ⇒
1231            match b2 with
1232             [ x0 ⇒ couple exadecimal bool x6 false
1233             | x1 ⇒ couple exadecimal bool x7 false
1234             | x2 ⇒ couple exadecimal bool x8 false
1235             | x3 ⇒ couple exadecimal bool x9 false
1236             | x4 ⇒ couple exadecimal bool xA false
1237             | x5 ⇒ couple exadecimal bool xB false
1238             | x6 ⇒ couple exadecimal bool xC false
1239             | x7 ⇒ couple exadecimal bool xD false
1240             | x8 ⇒ couple exadecimal bool xE false
1241             | x9 ⇒ couple exadecimal bool xF false
1242             | xA ⇒ couple exadecimal bool x0 true
1243             | xB ⇒ couple exadecimal bool x1 true
1244             | xC ⇒ couple exadecimal bool x2 true
1245             | xD ⇒ couple exadecimal bool x3 true
1246             | xE ⇒ couple exadecimal bool x4 true
1247             | xF ⇒ couple exadecimal bool x5 true ]
1248        | x7 ⇒
1249            match b2 with
1250             [ x0 ⇒ couple exadecimal bool x7 false
1251             | x1 ⇒ couple exadecimal bool x8 false
1252             | x2 ⇒ couple exadecimal bool x9 false
1253             | x3 ⇒ couple exadecimal bool xA false
1254             | x4 ⇒ couple exadecimal bool xB false
1255             | x5 ⇒ couple exadecimal bool xC false
1256             | x6 ⇒ couple exadecimal bool xD false
1257             | x7 ⇒ couple exadecimal bool xE false
1258             | x8 ⇒ couple exadecimal bool xF false
1259             | x9 ⇒ couple exadecimal bool x0 true
1260             | xA ⇒ couple exadecimal bool x1 true
1261             | xB ⇒ couple exadecimal bool x2 true
1262             | xC ⇒ couple exadecimal bool x3 true
1263             | xD ⇒ couple exadecimal bool x4 true
1264             | xE ⇒ couple exadecimal bool x5 true
1265             | xF ⇒ couple exadecimal bool x6 true ]
1266        | x8 ⇒
1267            match b2 with
1268             [ x0 ⇒ couple exadecimal bool x8 false
1269             | x1 ⇒ couple exadecimal bool x9 false
1270             | x2 ⇒ couple exadecimal bool xA false
1271             | x3 ⇒ couple exadecimal bool xB false
1272             | x4 ⇒ couple exadecimal bool xC false
1273             | x5 ⇒ couple exadecimal bool xD false
1274             | x6 ⇒ couple exadecimal bool xE false
1275             | x7 ⇒ couple exadecimal bool xF false
1276             | x8 ⇒ couple exadecimal bool x0 true
1277             | x9 ⇒ couple exadecimal bool x1 true
1278             | xA ⇒ couple exadecimal bool x2 true
1279             | xB ⇒ couple exadecimal bool x3 true
1280             | xC ⇒ couple exadecimal bool x4 true
1281             | xD ⇒ couple exadecimal bool x5 true
1282             | xE ⇒ couple exadecimal bool x6 true
1283             | xF ⇒ couple exadecimal bool x7 true ]
1284        | x9 ⇒
1285            match b2 with
1286             [ x0 ⇒ couple exadecimal bool x9 false
1287             | x1 ⇒ couple exadecimal bool xA false
1288             | x2 ⇒ couple exadecimal bool xB false
1289             | x3 ⇒ couple exadecimal bool xC false
1290             | x4 ⇒ couple exadecimal bool xD false
1291             | x5 ⇒ couple exadecimal bool xE false
1292             | x6 ⇒ couple exadecimal bool xF false
1293             | x7 ⇒ couple exadecimal bool x0 true
1294             | x8 ⇒ couple exadecimal bool x1 true
1295             | x9 ⇒ couple exadecimal bool x2 true
1296             | xA ⇒ couple exadecimal bool x3 true
1297             | xB ⇒ couple exadecimal bool x4 true
1298             | xC ⇒ couple exadecimal bool x5 true
1299             | xD ⇒ couple exadecimal bool x6 true
1300             | xE ⇒ couple exadecimal bool x7 true
1301             | xF ⇒ couple exadecimal bool x8 true ]
1302        | xA ⇒
1303            match b2 with
1304             [ x0 ⇒ couple exadecimal bool xA false
1305             | x1 ⇒ couple exadecimal bool xB false
1306             | x2 ⇒ couple exadecimal bool xC false
1307             | x3 ⇒ couple exadecimal bool xD false
1308             | x4 ⇒ couple exadecimal bool xE false
1309             | x5 ⇒ couple exadecimal bool xF false
1310             | x6 ⇒ couple exadecimal bool x0 true
1311             | x7 ⇒ couple exadecimal bool x1 true
1312             | x8 ⇒ couple exadecimal bool x2 true
1313             | x9 ⇒ couple exadecimal bool x3 true
1314             | xA ⇒ couple exadecimal bool x4 true
1315             | xB ⇒ couple exadecimal bool x5 true
1316             | xC ⇒ couple exadecimal bool x6 true
1317             | xD ⇒ couple exadecimal bool x7 true
1318             | xE ⇒ couple exadecimal bool x8 true
1319             | xF ⇒ couple exadecimal bool x9 true ]
1320        | xB ⇒
1321            match b2 with
1322             [ x0 ⇒ couple exadecimal bool xB false
1323             | x1 ⇒ couple exadecimal bool xC false
1324             | x2 ⇒ couple exadecimal bool xD false
1325             | x3 ⇒ couple exadecimal bool xE false
1326             | x4 ⇒ couple exadecimal bool xF false
1327             | x5 ⇒ couple exadecimal bool x0 true
1328             | x6 ⇒ couple exadecimal bool x1 true
1329             | x7 ⇒ couple exadecimal bool x2 true
1330             | x8 ⇒ couple exadecimal bool x3 true
1331             | x9 ⇒ couple exadecimal bool x4 true
1332             | xA ⇒ couple exadecimal bool x5 true
1333             | xB ⇒ couple exadecimal bool x6 true
1334             | xC ⇒ couple exadecimal bool x7 true
1335             | xD ⇒ couple exadecimal bool x8 true
1336             | xE ⇒ couple exadecimal bool x9 true
1337             | xF ⇒ couple exadecimal bool xA true ]
1338        | xC ⇒
1339            match b2 with
1340             [ x0 ⇒ couple exadecimal bool xC false
1341             | x1 ⇒ couple exadecimal bool xD false
1342             | x2 ⇒ couple exadecimal bool xE false
1343             | x3 ⇒ couple exadecimal bool xF false
1344             | x4 ⇒ couple exadecimal bool x0 true
1345             | x5 ⇒ couple exadecimal bool x1 true
1346             | x6 ⇒ couple exadecimal bool x2 true
1347             | x7 ⇒ couple exadecimal bool x3 true
1348             | x8 ⇒ couple exadecimal bool x4 true
1349             | x9 ⇒ couple exadecimal bool x5 true
1350             | xA ⇒ couple exadecimal bool x6 true
1351             | xB ⇒ couple exadecimal bool x7 true
1352             | xC ⇒ couple exadecimal bool x8 true
1353             | xD ⇒ couple exadecimal bool x9 true
1354             | xE ⇒ couple exadecimal bool xA true
1355             | xF ⇒ couple exadecimal bool xB true ]
1356        | xD ⇒
1357            match b2 with
1358             [ x0 ⇒ couple exadecimal bool xD false
1359             | x1 ⇒ couple exadecimal bool xE false
1360             | x2 ⇒ couple exadecimal bool xF false
1361             | x3 ⇒ couple exadecimal bool x0 true
1362             | x4 ⇒ couple exadecimal bool x1 true
1363             | x5 ⇒ couple exadecimal bool x2 true
1364             | x6 ⇒ couple exadecimal bool x3 true
1365             | x7 ⇒ couple exadecimal bool x4 true
1366             | x8 ⇒ couple exadecimal bool x5 true
1367             | x9 ⇒ couple exadecimal bool x6 true
1368             | xA ⇒ couple exadecimal bool x7 true
1369             | xB ⇒ couple exadecimal bool x8 true
1370             | xC ⇒ couple exadecimal bool x9 true
1371             | xD ⇒ couple exadecimal bool xA true
1372             | xE ⇒ couple exadecimal bool xB true
1373             | xF ⇒ couple exadecimal bool xC true ]
1374        | xE ⇒
1375            match b2 with
1376             [ x0 ⇒ couple exadecimal bool xE false
1377             | x1 ⇒ couple exadecimal bool xF false
1378             | x2 ⇒ couple exadecimal bool x0 true
1379             | x3 ⇒ couple exadecimal bool x1 true
1380             | x4 ⇒ couple exadecimal bool x2 true
1381             | x5 ⇒ couple exadecimal bool x3 true
1382             | x6 ⇒ couple exadecimal bool x4 true
1383             | x7 ⇒ couple exadecimal bool x5 true
1384             | x8 ⇒ couple exadecimal bool x6 true
1385             | x9 ⇒ couple exadecimal bool x7 true
1386             | xA ⇒ couple exadecimal bool x8 true
1387             | xB ⇒ couple exadecimal bool x9 true
1388             | xC ⇒ couple exadecimal bool xA true
1389             | xD ⇒ couple exadecimal bool xB true
1390             | xE ⇒ couple exadecimal bool xC true
1391             | xF ⇒ couple exadecimal bool xD true ]
1392        | xF ⇒
1393            match b2 with
1394             [ x0 ⇒ couple exadecimal bool xF false
1395             | x1 ⇒ couple exadecimal bool x0 true
1396             | x2 ⇒ couple exadecimal bool x1 true
1397             | x3 ⇒ couple exadecimal bool x2 true
1398             | x4 ⇒ couple exadecimal bool x3 true
1399             | x5 ⇒ couple exadecimal bool x4 true
1400             | x6 ⇒ couple exadecimal bool x5 true
1401             | x7 ⇒ couple exadecimal bool x6 true
1402             | x8 ⇒ couple exadecimal bool x7 true
1403             | x9 ⇒ couple exadecimal bool x8 true
1404             | xA ⇒ couple exadecimal bool x9 true
1405             | xB ⇒ couple exadecimal bool xA true
1406             | xC ⇒ couple exadecimal bool xB true
1407             | xD ⇒ couple exadecimal bool xC true
1408             | xE ⇒ couple exadecimal bool xD true
1409             | xF ⇒ couple exadecimal bool xE true ]
1410        ]
1411    ]
1412 .
1413
1414 definition plusbyte ≝
1415  λb1,b2,c.
1416   match plusex (bl b1) (bl b2) c with
1417    [ couple l c' ⇒
1418       match plusex (bh b1) (bh b2) c' with
1419        [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
1420
1421 alias num (instance 0) = "natural number".
1422 definition nat_of_exadecimal ≝
1423  λb.
1424   match b with
1425    [ x0 ⇒ 0
1426    | x1 ⇒ 1
1427    | x2 ⇒ 2
1428    | x3 ⇒ 3
1429    | x4 ⇒ 4
1430    | x5 ⇒ 5
1431    | x6 ⇒ 6
1432    | x7 ⇒ 7
1433    | x8 ⇒ 8
1434    | x9 ⇒ 9
1435    | xA ⇒ 10
1436    | xB ⇒ 11
1437    | xC ⇒ 12
1438    | xD ⇒ 13
1439    | xE ⇒ 14
1440    | xF ⇒ 15
1441    ].
1442
1443 coercion cic:/matita/assembly/nat_of_exadecimal.con.
1444
1445 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
1446
1447 coercion cic:/matita/assembly/nat_of_byte.con.
1448
1449 let rec exadecimal_of_nat b ≝
1450   match b with [ O ⇒ x0 | S b ⇒
1451   match b with [ O ⇒ x1 | S b ⇒
1452   match b with [ O ⇒ x2 | S b ⇒
1453   match b with [ O ⇒ x3 | S b ⇒
1454   match b with [ O ⇒ x4 | S b ⇒
1455   match b with [ O ⇒ x5 | S b ⇒
1456   match b with [ O ⇒ x6 | S b ⇒
1457   match b with [ O ⇒ x7 | S b ⇒
1458   match b with [ O ⇒ x8 | S b ⇒
1459   match b with [ O ⇒ x9 | S b ⇒
1460   match b with [ O ⇒ xA | S b ⇒
1461   match b with [ O ⇒ xB | S b ⇒
1462   match b with [ O ⇒ xC | S b ⇒
1463   match b with [ O ⇒ xD | S b ⇒
1464   match b with [ O ⇒ xE | S b ⇒
1465   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
1466
1467 definition byte_of_nat ≝
1468  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
1469
1470 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
1471  intros;
1472  elim b;
1473  elim e;
1474  elim e1;
1475  reflexivity.
1476 qed.
1477
1478 axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
1479 (* intros;
1480  unfold byte_of_nat;
1481 *)
1482
1483 definition nat_of_bool ≝
1484  λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
1485
1486 (* Way too slow. Handles 2^32 goals!
1487 lemma plusbyte_ok:
1488  ∀b1,b2,c.
1489   match plusbyte b1 b2 c with
1490    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
1491    ].
1492  intros;
1493  elim c;
1494  elim b1;
1495  elim e;
1496  elim e1;
1497  elim b2;
1498  elim e2;
1499  elim e3;
1500  reflexivity.
1501 qed.
1502 *)
1503
1504 (*
1505 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1506  intros; elim n; [ reflexivity | unfold byte_of_nat.
1507 qed.
1508 *)
1509
1510 definition addr ≝ nat.
1511
1512 definition xpred ≝
1513  λb.
1514   match b with
1515    [ x0 ⇒ xF
1516    | x1 ⇒ x0
1517    | x2 ⇒ x1
1518    | x3 ⇒ x2
1519    | x4 ⇒ x3
1520    | x5 ⇒ x4
1521    | x6 ⇒ x5
1522    | x7 ⇒ x6
1523    | x8 ⇒ x7
1524    | x9 ⇒ x8
1525    | xA ⇒ x9
1526    | xB ⇒ xA
1527    | xC ⇒ xB
1528    | xD ⇒ xC
1529    | xE ⇒ xD
1530    | xF ⇒ xE ].
1531
1532 definition bpred ≝
1533  λb.
1534   match eqex (bl b) x0 with
1535    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1536    | false ⇒ mk_byte (bh b) (xpred (bl b))
1537    ].
1538
1539 (* Way too slow and subsumed by previous theorem
1540 lemma bpred_pred:
1541  ∀b.
1542   match eqbyte b (mk_byte x0 x0) with
1543    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1544    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1545  intros;
1546  elim b;
1547  elim e;
1548  elim e1;
1549  reflexivity.
1550 qed.
1551 *)
1552
1553 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1554
1555 coercion cic:/matita/assembly/addr_of_byte.con.
1556
1557 inductive opcode: Type ≝
1558    ADDd: opcode  (* 3 clock, 171 *)
1559  | BEQ: opcode   (* 3, 55 *)
1560  | BRA: opcode   (* 3, 48 *)
1561  | DECd: opcode  (* 5, 58 *)
1562  | LDAi: opcode  (* 2, 166 *)
1563  | LDAd: opcode  (* 3, 182 *)
1564  | STAd: opcode. (* 3, 183 *)
1565
1566 let rec cycles_of_opcode op : nat ≝
1567  match op with
1568   [ ADDd ⇒ 3
1569   | BEQ ⇒ 3
1570   | BRA ⇒ 3
1571   | DECd ⇒ 5
1572   | LDAi ⇒ 2
1573   | LDAd ⇒ 3
1574   | STAd ⇒ 3
1575   ].
1576
1577 definition opcodemap ≝
1578  [ couple ? ? ADDd (mk_byte xA xB);
1579    couple ? ? BEQ (mk_byte x3 x7);
1580    couple ? ? BRA (mk_byte x3 x0);
1581    couple ? ? DECd (mk_byte x3 xA);
1582    couple ? ? LDAi (mk_byte xA x6);
1583    couple ? ? LDAd (mk_byte xB x6);
1584    couple ? ? STAd (mk_byte xB x7) ].
1585
1586 definition opcode_of_byte ≝
1587  λb.
1588   let rec aux l ≝
1589    match l with
1590     [ nil ⇒ ADDd
1591     | cons c tl ⇒
1592        match c with
1593         [ couple op n ⇒
1594            match eqbyte n b with
1595             [ true ⇒ op
1596             | false ⇒ aux tl
1597             ]]]
1598   in
1599    aux opcodemap.
1600
1601 definition magic_of_opcode ≝
1602  λop1.
1603   match op1 with
1604    [ ADDd ⇒ 0
1605    | BEQ ⇒  1
1606    | BRA ⇒  2
1607    | DECd ⇒ 3
1608    | LDAi ⇒ 4
1609    | LDAd ⇒ 5
1610    | STAd ⇒ 6 ].
1611
1612 definition opcodeeqb ≝
1613  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1614
1615 definition byte_of_opcode : opcode → byte ≝
1616  λop.
1617   let rec aux l ≝
1618    match l with
1619     [ nil ⇒ mk_byte x0 x0
1620     | cons c tl ⇒
1621        match c with
1622         [ couple op' n ⇒
1623            match opcodeeqb op op' with
1624             [ true ⇒ n
1625             | false ⇒ aux tl
1626             ]]]
1627   in
1628    aux opcodemap.
1629
1630 record status : Type ≝ {
1631   acc : byte;
1632   pc  : addr;
1633   spc : addr;
1634   zf  : bool;
1635   cf  : bool;
1636   mem : addr → byte;
1637   clk : nat
1638 }.
1639
1640 definition update ≝
1641  λf: addr → byte.λa.λv.λx.
1642   match eqb x a with
1643    [ true ⇒ v
1644    | false ⇒ f x ].
1645
1646 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1647
1648 definition tick ≝
1649  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1650   let opc ≝ opcode_of_byte (mem pc) in
1651   let op1 ≝ mem (S pc) in
1652   let clk' ≝ cycles_of_opcode opc in
1653   match eqb (S clk) clk' with
1654    [ true ⇒
1655       match opc with
1656        [ ADDd ⇒
1657           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1658           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1659           let c' ≝ match res with [ couple _ c' ⇒ c'] in
1660            mk_status acc' (2 + pc) spc
1661             (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
1662        | BEQ ⇒
1663           mk_status
1664            acc
1665            (match zf with
1666              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
1667              | false ⇒ 2 + pc
1668              ])
1669            spc
1670            zf
1671            cf
1672            mem
1673            0
1674        | BRA ⇒
1675           mk_status
1676            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1677            spc
1678            zf
1679            cf
1680            mem
1681            0
1682        | DECd ⇒
1683           let x ≝ bpred (mem op1) in (* signed!!! *)
1684           let mem' ≝ update mem op1 x in
1685            mk_status acc (2 + pc) spc
1686             (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
1687        | LDAi ⇒
1688           mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
1689        | LDAd ⇒
1690           let x ≝ mem op1 in
1691            mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
1692        | STAd ⇒
1693           mk_status acc (2 + pc) spc zf cf
1694            (update mem op1 acc) 0
1695        ]
1696    | false ⇒
1697        mk_status
1698         acc pc spc zf cf mem (S clk)
1699    ]].
1700
1701 let rec execute s n on n ≝
1702  match n with
1703   [ O ⇒ s
1704   | S n' ⇒ execute (tick s) n'
1705   ].
1706
1707 lemma breakpoint:
1708  ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
1709  intros;
1710  generalize in match s; clear s;
1711  elim n1;
1712   [ reflexivity
1713   | simplify;
1714     apply H;
1715   ]
1716 qed.
1717
1718 notation "hvbox(# break a)"
1719   non associative with precedence 80
1720 for @{ 'byte_of_opcode $a }.
1721 interpretation "byte_of_opcode" 'byte_of_opcode a =
1722  (cic:/matita/assembly/byte_of_opcode.con a).
1723
1724 definition mult_source : list byte ≝
1725   [#LDAi; mk_byte x0 x0; (* A := 0 *)
1726    #STAd; mk_byte x2 x0; (* Z := A *)
1727    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1728    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
1729    #LDAd; mk_byte x2 x0; (* A := Z *)
1730    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1731    #ADDd; mk_byte x1 xE; (* A += X *)
1732    #STAd; mk_byte x2 x0; (* Z := A *)
1733    #BRA;  mk_byte xF x2; (* goto l1 *)
1734    #LDAd; mk_byte x2 x0].(* (l2) *)
1735
1736 definition mult_memory ≝
1737  λx,y.λa:addr.
1738      match leb a 29 with
1739       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1740       | false ⇒
1741          match eqb a 30 with
1742           [ true ⇒ x
1743           | false ⇒ y
1744           ]
1745       ].
1746
1747 definition mult_status ≝
1748  λx,y.
1749   mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
1750
1751 lemma plusbyte_O_x:
1752  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1753  intros;
1754  elim b;
1755  elim e;
1756  elim e1;
1757  reflexivity.
1758 qed.
1759
1760 definition plusbytenc ≝
1761  λx,y.
1762   match plusbyte x y false with
1763    [couple res _ ⇒ res].
1764
1765 definition plusbytec ≝
1766  λx,y.
1767   match plusbyte x y false with
1768    [couple _ c ⇒ c].
1769
1770 lemma plusbytenc_O_x:
1771  ∀x. plusbytenc (mk_byte x0 x0) x = x.
1772  intros;
1773  unfold plusbytenc;
1774  rewrite > plusbyte_O_x;
1775  reflexivity.
1776 qed.
1777
1778 lemma test_O_O:
1779   let i ≝ 14 in
1780   let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1781    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1782  normalize;
1783  split;
1784  reflexivity.
1785 qed.
1786
1787
1788 lemma test_0_2:
1789   let x ≝ mk_byte x0 x0 in
1790   let y ≝ mk_byte x0 x2 in
1791   let i ≝ 14 + 23 * nat_of_byte y in
1792   let s ≝ execute (mult_status x y) i in
1793    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1794  intros;
1795  split;
1796  reflexivity.
1797 qed.
1798
1799 lemma test_x_1:
1800  ∀x.
1801   let y ≝ mk_byte x0 x1 in
1802   let i ≝ 14 + 23 * nat_of_byte y in
1803   let s ≝ execute (mult_status x y) i in
1804    pc s = 20 ∧ mem s 32 = x.
1805  intros;
1806  split;
1807   [ reflexivity
1808   | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1809     rewrite > plusbytenc_O_x;
1810     reflexivity
1811   ].
1812 qed.
1813
1814 lemma test_x_2:
1815  ∀x.
1816   let y ≝ mk_byte x0 x2 in
1817   let i ≝ 14 + 23 * nat_of_byte y in
1818   let s ≝ execute (mult_status x y) i in
1819    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1820  intros;
1821  split;
1822   [ reflexivity
1823   | change in ⊢ (? ? % ?) with
1824      (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1825     rewrite > plusbytenc_O_x;
1826     reflexivity
1827   ].
1828 qed.
1829
1830 axiom byte_elim:
1831  ∀P:byte → Prop.
1832   (P (mk_byte x0 x0)) →
1833    (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
1834     ∀b:byte. P b.
1835 (* Tedious proof, easy to automate but not trivial
1836  intros;
1837  elim b;
1838  elim e;
1839   [ elim e1;
1840      [ assumption
1841      | apply (H1 0);
1842         [ apply lt_O_S
1843         | assumption
1844         ]
1845      | apply (H1 1);
1846         [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
1847           apply lt_S_S;
1848           apply lt_O_S
1849         | apply (H1 0);
1850 *)
1851
1852 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
1853  unfold lt;
1854  intros;
1855  autobatch.
1856 qed.
1857
1858 axiom daemon: False.
1859
1860 (*axiom loop_invariant:
1861  ∀x,y:byte.∀j:nat. j ≤ y →
1862   let s ≝ execute (mult_status x y) (5 + 23*j) in
1863    pc s = 4 ∧
1864    mem s 30 = x ∧
1865    mem s 31 = byte_of_nat (y - j) ∧
1866    mem s 32 = byte_of_nat (x * j).
1867
1868  intros 2;
1869  apply (byte_elim ? ? ? y);
1870   [ intros;
1871     simplify in H;
1872     cut (j=O);
1873      [ unfold s; clear s;
1874        rewrite > Hcut;
1875        reflexivity
1876      | (* easy *) elim daemon
1877      ]
1878   | intros;
1879     unfold s;
1880     cut (j < S i ∨ j = S i);
1881     [ elim Hcut;
1882        [ rewrite > nat_of_byte_byte_of_nat in H1;
1883          [2: apply (lt_trans ? 255);
1884              [ assumption
1885              | unfold lt;
1886                (* ???????? *)
1887              ]
1888          | generalize in match (H1 j); clear H1;
1889            intros;
1890            unfold lt in H3;
1891            cut (j ≤ i);
1892             [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro;
1893               apply H1
1894             | letin xxx ≝ H3;
1895               inversion xxx;
1896                [ intro;
1897                  rewrite > (injective_S ? ? H1);
1898                  autobatch
1899                | intros;
1900                  (* facile *) elim daemon
1901                ]
1902             ]
1903          ]
1904        |
1905        ]
1906     | (* easy *)
1907     ]
1908   ].
1909 qed.
1910 *)
1911
1912 axiom status_eq:
1913  ∀s,s'.
1914   acc s = acc s' →
1915   pc s = pc s' →
1916   spc s = spc s' →
1917   zf s = zf s' →
1918   cf s = cf s' →
1919   (∀a. mem s a = mem s' a) →
1920   clk s = clk s' →
1921    s=s'.
1922
1923 lemma eq_eqex_S_x0_false:
1924  ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
1925  intro;
1926  cases n 0; [ intro; simplify; reflexivity | clear n];
1927  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1928  cases n 0; [ intro; simplify; reflexivity | clear n];
1929  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1930  cases n 0; [ intro; simplify; reflexivity | clear n];
1931  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1932  cases n 0; [ intro; simplify; reflexivity | clear n];
1933  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1934  cases n 0; [ intro; simplify; reflexivity | clear n];
1935  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1936  cases n 0; [ intro; simplify; reflexivity | clear n];
1937  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1938  cases n 0; [ intro; simplify; reflexivity | clear n];
1939  cases n1 0; [ intro; simplify; reflexivity | clear n1];
1940  cases n 0; [ intro; simplify; reflexivity | clear n];
1941  intro;
1942  unfold lt in H;
1943  cut (S n1 ≤ 0);
1944   [ elim (not_le_Sn_O ? Hcut)
1945   | do 15 (apply le_S_S_to_le);
1946     assumption
1947   ]
1948 qed.
1949
1950 lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
1951  intros;
1952  unfold div;
1953  apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
1954  cut (∃w.m = S w);
1955   [ elim Hcut;
1956     rewrite > H2;
1957     rewrite > H2 in H1;
1958     clear Hcut; clear H2; clear H; (*clear m;*)
1959     simplify;
1960     unfold in ⊢ (? ? % ?);
1961     cut (∃z.n = S z);
1962      [ elim Hcut; clear Hcut;
1963        rewrite > H in H1;
1964        rewrite > H; clear m;
1965        change in ⊢ (? ? % ?)  with
1966         (match leb (S a1) a with
1967          [ true ⇒ O
1968          | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
1969        cut (S a1 ≰ a);
1970         [ apply (leb_elim (S a1) a);
1971            [ intro;
1972              elim (Hcut H2)
1973            | intro;
1974              simplify;
1975              reflexivity
1976            ]
1977         | intro;
1978           autobatch
1979         ]
1980      | elim H1; autobatch
1981      ]
1982   | autobatch
1983   ].
1984 qed.
1985
1986 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
1987  ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
1988  intros;
1989  unfold byte_of_nat;
1990  cut (b < 15 ∨ b ≥ 15);
1991   [ elim Hcut;
1992     [ unfold eqbyte;
1993       change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
1994       rewrite > eq_eqex_S_x0_false;
1995        [ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
1996          rewrite > andb_sym;
1997          reflexivity
1998        | assumption
1999        ]
2000     | unfold eqbyte;
2001       change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
2002       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
2003        [ autobatch
2004        | unfold in H1;
2005          apply le_S_S;
2006          assumption
2007        | clearbody K;
2008          elim K; clear K;
2009          rewrite > H2;
2010          rewrite > eq_eqex_S_x0_false;
2011           [ reflexivity
2012           | unfold lt;
2013             unfold lt in H;
2014             rewrite < H2;
2015             clear H2; clear a; clear H1; clear Hcut;
2016             elim daemon (* trivial arithmetic property over <= and div *)
2017           ]
2018        ]
2019     ]
2020   | elim daemon
2021   ].
2022 qed.
2023
2024 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
2025  intro;
2026  elim b;
2027  simplify;
2028  autobatch.
2029 qed.
2030
2031 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
2032  intro;
2033  unfold nat_of_byte;
2034  letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
2035  letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
2036  unfold lt in H K ⊢ %;
2037  letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
2038  letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
2039  apply le_S_S;
2040  cut (16*bh b ≤ 16*15);
2041   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
2042     simplify in Hf:(? ? %);
2043     assumption
2044   | autobatch
2045   ]
2046 qed.
2047
2048 lemma exadecimal_of_nat_mod:
2049  ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
2050  elim daemon.
2051 (*
2052  intros;
2053  cases n; [ reflexivity | ];
2054  cases n1; [ reflexivity | ];
2055  cases n2; [ reflexivity | ];
2056  cases n3; [ reflexivity | ];
2057  cases n4; [ reflexivity | ];
2058  cases n5; [ reflexivity | ];
2059  cases n6; [ reflexivity | ];
2060  cases n7; [ reflexivity | ];
2061  cases n8; [ reflexivity | ];
2062  cases n9; [ reflexivity | ];
2063  cases n10; [ reflexivity | ];
2064  cases n11; [ reflexivity | ];
2065  cases n12; [ reflexivity | ];
2066  cases n13; [ reflexivity | ];
2067  cases n14; [ reflexivity | ];
2068  cases n15; [ reflexivity | ];
2069  change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
2070  cut ((16 + n16) \mod 16 = n16 \mod 16);
2071   [ rewrite > Hcut;
2072     simplify in ⊢ (? ? % ?);
2073
2074   | unfold mod;
2075     change with (mod_aux (16+n16) (16+n16) 15 = n16);
2076     unfold mod_aux;
2077     change with
2078      (match leb (16+n16) 15 with
2079        [true ⇒ 16+n16
2080        | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
2081        ] = n16);
2082     cut (leb (16+n16) 15 = false);
2083      [ rewrite > Hcut;
2084        change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
2085        cut (16+n16-16 = n16);
2086         [ rewrite > Hcut1; clear Hcut1;
2087
2088         |
2089         ]
2090      |
2091      ]
2092   ]*)
2093 qed.
2094
2095 lemma eq_bpred_S_a_a:
2096  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
2097 elim daemon. (*
2098  intros;
2099  unfold byte_of_nat;
2100  cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
2101   [ elim Hcut;
2102      [
2103      |
2104      ]
2105   | autobatch
2106   ].*)
2107 qed.
2108
2109 lemma plusbyteenc_S:
2110  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
2111  intros;
2112  elim daemon.
2113 qed.
2114
2115 (*
2116 lemma loop_invariant':
2117  ∀x,y:byte.∀j:nat. j ≤ y →
2118   execute (mult_status x y) (5 + 23*j)
2119    =
2120     mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j))) false
2121      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
2122       (byte_of_nat (x * j)))
2123      0.
2124  intros 3;
2125  elim j;
2126   [ do 2 (rewrite < times_n_O);
2127     apply status_eq;
2128     [1,2,3,4,5,7: normalize; reflexivity
2129     | intro;
2130       elim daemon
2131     ]
2132   | cut (5 + 23 * S n = 5 + 23 * n + 23);
2133     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
2134       letin H' ≝ (H ?); clearbody H'; clear H;
2135       [ autobatch
2136       | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
2137         clear Hcut;
2138         rewrite > xxx;
2139         clear xxx;
2140         apply (transitive_eq ? ? ? ? K);
2141         clear K;
2142         rewrite > H';
2143         clear H';
2144         cut (∃z.y-n=S z ∧ z < 255);
2145          [ elim Hcut; clear Hcut;
2146            elim H; clear H;
2147            rewrite > H2;
2148            (* instruction 1 *)
2149            letin K ≝
2150             (breakpoint
2151               (mk_status (byte_of_nat (x*n)) 4 O true false
2152                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2153                (byte_of_nat (x*n))) O)
2154               3 20); clearbody K;
2155            normalize in K:(? ? (? ? %) ?);
2156            apply transitive_eq; [2: apply K | skip | ]; clear K;
2157            change in ⊢ (? ? (? % ?) ?) with
2158            (mk_status
2159             (byte_of_nat (S a))
2160             6
2161             0
2162             (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
2163             false
2164             (update
2165              (update (update (mult_memory x y) 30 x)
2166                31 (byte_of_nat (S a)))
2167               32 (byte_of_nat (x*n)))
2168             0);
2169            (* instruction 2 *)
2170            letin K ≝
2171             (breakpoint
2172               (mk_status (byte_of_nat (S a)) 6 O
2173                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) false
2174                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2175                  (byte_of_nat (x*n))) O)
2176               3 17); clearbody K;
2177            normalize in K:(? ? (? ? %) ?);
2178            apply transitive_eq; [2: apply K | skip | ]; clear K;
2179            whd in ⊢ (? ? (? % ?) ?);
2180            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
2181            rewrite > K; clear K;
2182            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2183            (* instruction 3 *)
2184            letin K ≝
2185             (breakpoint
2186               (mk_status (byte_of_nat (S a)) 8 O
2187                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) false
2188                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2189                  (byte_of_nat (x*n))) O)
2190               3 14); clearbody K;
2191            normalize in K:(? ? (? ? %) ?);
2192            apply transitive_eq; [2: apply K | skip | ]; clear K;
2193            whd in ⊢ (? ? (? % ?) ?);
2194            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
2195            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2196            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
2197            (* instruction DECd *)
2198            letin K ≝
2199             (breakpoint
2200              (mk_status (byte_of_nat (x*n)) 10 O
2201               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) false
2202                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2203                 (byte_of_nat (x*n))) O)
2204              5 9); clearbody K;
2205            normalize in K:(? ? (? ? %) ?);
2206            apply transitive_eq; [2: apply K | skip | ]; clear K;
2207            whd in ⊢ (? ? (? % ?) ?);
2208            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
2209            rewrite > (eq_bpred_S_a_a ? H3);
2210            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2211            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
2212            cut (y - S n = a);
2213             [2: elim daemon | ];
2214            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
2215            (* instruction ADDd *)
2216            letin K ≝
2217             (breakpoint
2218              (mk_status (byte_of_nat (x*n)) 12
2219               O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n))) false
2220               (update
2221                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
2222                32 (byte_of_nat (x*n))) 31
2223                (byte_of_nat (y-S n))) O)
2224              3 6); clearbody K;
2225            normalize in K:(? ? (? ? %) ?);
2226            apply transitive_eq; [2: apply K | skip | ]; clear K;
2227            whd in ⊢ (? ? (? % ?) ?);
2228            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
2229             (plusbytenc (byte_of_nat (x*n)) x);
2230            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
2231             (plusbytenc (byte_of_nat (x*n)) x);
2232            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2233            normalize in \vdash (? ?
2234             (?
2235              (? ? ? ? ? match ? ? % ? in cartesian_product return ? with [couple\rArr ?] ? ?)
2236              ?) ?);
2237            rewrite > plusbyteenc_S;
2238            (* instruction STAd *)
2239            letin K ≝
2240             (breakpoint
2241              (mk_status (byte_of_nat (x*S n)) 14 O
2242               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
2243                match plusbyte (byte_of_nat (x*n)) x false
2244                 in cartesian_product
2245                return \lambda c:(cartesian_product byte bool).bool
2246               with
2247               [couple (_:byte) (c':bool)\rArr c']
2248                (update
2249                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
2250                 32 (byte_of_nat (x*n))) 31
2251                 (byte_of_nat (y-S n))) O)
2252             3 3); clearbody K;
2253            normalize in K:(? ? (? ? %) ?);
2254            apply transitive_eq; [2: apply K | skip | ]; clear K;
2255            whd in ⊢ (? ? (? % ?) ?);
2256            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2257            (* instruction BRA *)
2258            whd in ⊢ (? ? % ?);
2259            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
2260            apply status_eq;
2261             [1,2,3,4,7: normalize; reflexivity
2262             |6: intro;
2263               elim daemon
2264             |5: FALSO!
2265             ]
2266          | exists;
2267             [ apply (y - S n)
2268             | split;
2269                [ rewrite < (minus_S_S y n);
2270                  autobatch
2271                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
2272                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
2273                  autobatch
2274                ]
2275             ]
2276          ]
2277       ]
2278     | autobatch paramodulation
2279     ]
2280   ]
2281 qed.
2282
2283 theorem test_x_y:
2284  ∀x,y.
2285   let i ≝ 14 + 23 * nat_of_byte y in
2286   let s ≝ execute (mult_status x y) i in
2287    pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
2288  intros;
2289  generalize in match (loop_invariant' x y y (le_n y)); intro;
2290  generalize in match (breakpoint (mult_status x y) (5 + 23*y) 9); intro;
2291  cut (5 + 23*y +9 = 14 + 23* y);
2292   [2: autobatch paramodulation
2293   | rewrite > Hcut in H1;
2294     change in H1:(? ? % ?) with s;
2295     letin s0 ≝ (execute (mult_status x y) (S (S (S (S (S O))))+S 22*y));
2296     generalize in match H; intro K; clear H;
2297     change in K with
2298      (s0 =
2299       mk_status (byte_of_nat (x*y)) 4 0 true false
2300        (update
2301         (update
2302          (update (mult_memory x y) 30 x)
2303          31 (byte_of_nat (y-y)))
2304          32 (byte_of_nat (x*y))) O);
2305     clear Hcut;
2306     generalize in match H1; intro K1; clear H1;
2307     change in K1 with (s = execute s0 9);
2308     rewrite > K in K1;
2309     clear K; clear s0; clearbody s; clear i;
2310     rewrite < minus_n_n in K1;
2311     split;
2312     rewrite > K1;
2313     reflexivity
2314   ]
2315 qed.*)