matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_exadecim.ml

   1 type exadecim =
   2 X0
   3  | X1
   4  | X2
   5  | X3
   6  | X4
   7  | X5
   8  | X6
   9  | X7
  10  | X8
  11  | X9
  12  | XA
  13  | XB
  14  | XC
  15  | XD
  16  | XE
  17  | XF
  18 ;;
  19
  20 let exadecim_rec =
  21 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function p8 -> (function p9 -> (function p10 -> (function p11 -> (function p12 -> (function p13 -> (function p14 -> (function p15 -> (function e ->
  22 (match e with
  23    X0 -> p
  24  | X1 -> p1
  25  | X2 -> p2
  26  | X3 -> p3
  27  | X4 -> p4
  28  | X5 -> p5
  29  | X6 -> p6
  30  | X7 -> p7
  31  | X8 -> p8
  32  | X9 -> p9
  33  | XA -> p10
  34  | XB -> p11
  35  | XC -> p12
  36  | XD -> p13
  37  | XE -> p14
  38  | XF -> p15)
  39 )))))))))))))))))
  40 ;;
  41
  42 let exadecim_rect =
  43 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function p5 -> (function p6 -> (function p7 -> (function p8 -> (function p9 -> (function p10 -> (function p11 -> (function p12 -> (function p13 -> (function p14 -> (function p15 -> (function e ->
  44 (match e with
  45    X0 -> p
  46  | X1 -> p1
  47  | X2 -> p2
  48  | X3 -> p3
  49  | X4 -> p4
  50  | X5 -> p5
  51  | X6 -> p6
  52  | X7 -> p7
  53  | X8 -> p8
  54  | X9 -> p9
  55  | XA -> p10
  56  | XB -> p11
  57  | XC -> p12
  58  | XD -> p13
  59  | XE -> p14
  60  | XF -> p15)
  61 )))))))))))))))))
  62 ;;
  63
  64 let eq_ex =
  65 (function e1 -> (function e2 ->
  66 (match e1 with
  67    X0 ->
  68 (match e2 with
  69    X0 -> Matita_datatypes_bool.True
  70  | X1 -> Matita_datatypes_bool.False
  71  | X2 -> Matita_datatypes_bool.False
  72  | X3 -> Matita_datatypes_bool.False
  73  | X4 -> Matita_datatypes_bool.False
  74  | X5 -> Matita_datatypes_bool.False
  75  | X6 -> Matita_datatypes_bool.False
  76  | X7 -> Matita_datatypes_bool.False
  77  | X8 -> Matita_datatypes_bool.False
  78  | X9 -> Matita_datatypes_bool.False
  79  | XA -> Matita_datatypes_bool.False
  80  | XB -> Matita_datatypes_bool.False
  81  | XC -> Matita_datatypes_bool.False
  82  | XD -> Matita_datatypes_bool.False
  83  | XE -> Matita_datatypes_bool.False
  84  | XF -> Matita_datatypes_bool.False)
  85
  86  | X1 ->
  87 (match e2 with
  88    X0 -> Matita_datatypes_bool.False
  89  | X1 -> Matita_datatypes_bool.True
  90  | X2 -> Matita_datatypes_bool.False
  91  | X3 -> Matita_datatypes_bool.False
  92  | X4 -> Matita_datatypes_bool.False
  93  | X5 -> Matita_datatypes_bool.False
  94  | X6 -> Matita_datatypes_bool.False
  95  | X7 -> Matita_datatypes_bool.False
  96  | X8 -> Matita_datatypes_bool.False
  97  | X9 -> Matita_datatypes_bool.False
  98  | XA -> Matita_datatypes_bool.False
  99  | XB -> Matita_datatypes_bool.False
 100  | XC -> Matita_datatypes_bool.False
 101  | XD -> Matita_datatypes_bool.False
 102  | XE -> Matita_datatypes_bool.False
 103  | XF -> Matita_datatypes_bool.False)
 104
 105  | X2 ->
 106 (match e2 with
 107    X0 -> Matita_datatypes_bool.False
 108  | X1 -> Matita_datatypes_bool.False
 109  | X2 -> Matita_datatypes_bool.True
 110  | X3 -> Matita_datatypes_bool.False
 111  | X4 -> Matita_datatypes_bool.False
 112  | X5 -> Matita_datatypes_bool.False
 113  | X6 -> Matita_datatypes_bool.False
 114  | X7 -> Matita_datatypes_bool.False
 115  | X8 -> Matita_datatypes_bool.False
 116  | X9 -> Matita_datatypes_bool.False
 117  | XA -> Matita_datatypes_bool.False
 118  | XB -> Matita_datatypes_bool.False
 119  | XC -> Matita_datatypes_bool.False
 120  | XD -> Matita_datatypes_bool.False
 121  | XE -> Matita_datatypes_bool.False
 122  | XF -> Matita_datatypes_bool.False)
 123
 124  | X3 ->
 125 (match e2 with
 126    X0 -> Matita_datatypes_bool.False
 127  | X1 -> Matita_datatypes_bool.False
 128  | X2 -> Matita_datatypes_bool.False
 129  | X3 -> Matita_datatypes_bool.True
 130  | X4 -> Matita_datatypes_bool.False
 131  | X5 -> Matita_datatypes_bool.False
 132  | X6 -> Matita_datatypes_bool.False
 133  | X7 -> Matita_datatypes_bool.False
 134  | X8 -> Matita_datatypes_bool.False
 135  | X9 -> Matita_datatypes_bool.False
 136  | XA -> Matita_datatypes_bool.False
 137  | XB -> Matita_datatypes_bool.False
 138  | XC -> Matita_datatypes_bool.False
 139  | XD -> Matita_datatypes_bool.False
 140  | XE -> Matita_datatypes_bool.False
 141  | XF -> Matita_datatypes_bool.False)
 142
 143  | X4 ->
 144 (match e2 with
 145    X0 -> Matita_datatypes_bool.False
 146  | X1 -> Matita_datatypes_bool.False
 147  | X2 -> Matita_datatypes_bool.False
 148  | X3 -> Matita_datatypes_bool.False
 149  | X4 -> Matita_datatypes_bool.True
 150  | X5 -> Matita_datatypes_bool.False
 151  | X6 -> Matita_datatypes_bool.False
 152  | X7 -> Matita_datatypes_bool.False
 153  | X8 -> Matita_datatypes_bool.False
 154  | X9 -> Matita_datatypes_bool.False
 155  | XA -> Matita_datatypes_bool.False
 156  | XB -> Matita_datatypes_bool.False
 157  | XC -> Matita_datatypes_bool.False
 158  | XD -> Matita_datatypes_bool.False
 159  | XE -> Matita_datatypes_bool.False
 160  | XF -> Matita_datatypes_bool.False)
 161
 162  | X5 ->
 163 (match e2 with
 164    X0 -> Matita_datatypes_bool.False
 165  | X1 -> Matita_datatypes_bool.False
 166  | X2 -> Matita_datatypes_bool.False
 167  | X3 -> Matita_datatypes_bool.False
 168  | X4 -> Matita_datatypes_bool.False
 169  | X5 -> Matita_datatypes_bool.True
 170  | X6 -> Matita_datatypes_bool.False
 171  | X7 -> Matita_datatypes_bool.False
 172  | X8 -> Matita_datatypes_bool.False
 173  | X9 -> Matita_datatypes_bool.False
 174  | XA -> Matita_datatypes_bool.False
 175  | XB -> Matita_datatypes_bool.False
 176  | XC -> Matita_datatypes_bool.False
 177  | XD -> Matita_datatypes_bool.False
 178  | XE -> Matita_datatypes_bool.False
 179  | XF -> Matita_datatypes_bool.False)
 180
 181  | X6 ->
 182 (match e2 with
 183    X0 -> Matita_datatypes_bool.False
 184  | X1 -> Matita_datatypes_bool.False
 185  | X2 -> Matita_datatypes_bool.False
 186  | X3 -> Matita_datatypes_bool.False
 187  | X4 -> Matita_datatypes_bool.False
 188  | X5 -> Matita_datatypes_bool.False
 189  | X6 -> Matita_datatypes_bool.True
 190  | X7 -> Matita_datatypes_bool.False
 191  | X8 -> Matita_datatypes_bool.False
 192  | X9 -> Matita_datatypes_bool.False
 193  | XA -> Matita_datatypes_bool.False
 194  | XB -> Matita_datatypes_bool.False
 195  | XC -> Matita_datatypes_bool.False
 196  | XD -> Matita_datatypes_bool.False
 197  | XE -> Matita_datatypes_bool.False
 198  | XF -> Matita_datatypes_bool.False)
 199
 200  | X7 ->
 201 (match e2 with
 202    X0 -> Matita_datatypes_bool.False
 203  | X1 -> Matita_datatypes_bool.False
 204  | X2 -> Matita_datatypes_bool.False
 205  | X3 -> Matita_datatypes_bool.False
 206  | X4 -> Matita_datatypes_bool.False
 207  | X5 -> Matita_datatypes_bool.False
 208  | X6 -> Matita_datatypes_bool.False
 209  | X7 -> Matita_datatypes_bool.True
 210  | X8 -> Matita_datatypes_bool.False
 211  | X9 -> Matita_datatypes_bool.False
 212  | XA -> Matita_datatypes_bool.False
 213  | XB -> Matita_datatypes_bool.False
 214  | XC -> Matita_datatypes_bool.False
 215  | XD -> Matita_datatypes_bool.False
 216  | XE -> Matita_datatypes_bool.False
 217  | XF -> Matita_datatypes_bool.False)
 218
 219  | X8 ->
 220 (match e2 with
 221    X0 -> Matita_datatypes_bool.False
 222  | X1 -> Matita_datatypes_bool.False
 223  | X2 -> Matita_datatypes_bool.False
 224  | X3 -> Matita_datatypes_bool.False
 225  | X4 -> Matita_datatypes_bool.False
 226  | X5 -> Matita_datatypes_bool.False
 227  | X6 -> Matita_datatypes_bool.False
 228  | X7 -> Matita_datatypes_bool.False
 229  | X8 -> Matita_datatypes_bool.True
 230  | X9 -> Matita_datatypes_bool.False
 231  | XA -> Matita_datatypes_bool.False
 232  | XB -> Matita_datatypes_bool.False
 233  | XC -> Matita_datatypes_bool.False
 234  | XD -> Matita_datatypes_bool.False
 235  | XE -> Matita_datatypes_bool.False
 236  | XF -> Matita_datatypes_bool.False)
 237
 238  | X9 ->
 239 (match e2 with
 240    X0 -> Matita_datatypes_bool.False
 241  | X1 -> Matita_datatypes_bool.False
 242  | X2 -> Matita_datatypes_bool.False
 243  | X3 -> Matita_datatypes_bool.False
 244  | X4 -> Matita_datatypes_bool.False
 245  | X5 -> Matita_datatypes_bool.False
 246  | X6 -> Matita_datatypes_bool.False
 247  | X7 -> Matita_datatypes_bool.False
 248  | X8 -> Matita_datatypes_bool.False
 249  | X9 -> Matita_datatypes_bool.True
 250  | XA -> Matita_datatypes_bool.False
 251  | XB -> Matita_datatypes_bool.False
 252  | XC -> Matita_datatypes_bool.False
 253  | XD -> Matita_datatypes_bool.False
 254  | XE -> Matita_datatypes_bool.False
 255  | XF -> Matita_datatypes_bool.False)
 256
 257  | XA ->
 258 (match e2 with
 259    X0 -> Matita_datatypes_bool.False
 260  | X1 -> Matita_datatypes_bool.False
 261  | X2 -> Matita_datatypes_bool.False
 262  | X3 -> Matita_datatypes_bool.False
 263  | X4 -> Matita_datatypes_bool.False
 264  | X5 -> Matita_datatypes_bool.False
 265  | X6 -> Matita_datatypes_bool.False
 266  | X7 -> Matita_datatypes_bool.False
 267  | X8 -> Matita_datatypes_bool.False
 268  | X9 -> Matita_datatypes_bool.False
 269  | XA -> Matita_datatypes_bool.True
 270  | XB -> Matita_datatypes_bool.False
 271  | XC -> Matita_datatypes_bool.False
 272  | XD -> Matita_datatypes_bool.False
 273  | XE -> Matita_datatypes_bool.False
 274  | XF -> Matita_datatypes_bool.False)
 275
 276  | XB ->
 277 (match e2 with
 278    X0 -> Matita_datatypes_bool.False
 279  | X1 -> Matita_datatypes_bool.False
 280  | X2 -> Matita_datatypes_bool.False
 281  | X3 -> Matita_datatypes_bool.False
 282  | X4 -> Matita_datatypes_bool.False
 283  | X5 -> Matita_datatypes_bool.False
 284  | X6 -> Matita_datatypes_bool.False
 285  | X7 -> Matita_datatypes_bool.False
 286  | X8 -> Matita_datatypes_bool.False
 287  | X9 -> Matita_datatypes_bool.False
 288  | XA -> Matita_datatypes_bool.False
 289  | XB -> Matita_datatypes_bool.True
 290  | XC -> Matita_datatypes_bool.False
 291  | XD -> Matita_datatypes_bool.False
 292  | XE -> Matita_datatypes_bool.False
 293  | XF -> Matita_datatypes_bool.False)
 294
 295  | XC ->
 296 (match e2 with
 297    X0 -> Matita_datatypes_bool.False
 298  | X1 -> Matita_datatypes_bool.False
 299  | X2 -> Matita_datatypes_bool.False
 300  | X3 -> Matita_datatypes_bool.False
 301  | X4 -> Matita_datatypes_bool.False
 302  | X5 -> Matita_datatypes_bool.False
 303  | X6 -> Matita_datatypes_bool.False
 304  | X7 -> Matita_datatypes_bool.False
 305  | X8 -> Matita_datatypes_bool.False
 306  | X9 -> Matita_datatypes_bool.False
 307  | XA -> Matita_datatypes_bool.False
 308  | XB -> Matita_datatypes_bool.False
 309  | XC -> Matita_datatypes_bool.True
 310  | XD -> Matita_datatypes_bool.False
 311  | XE -> Matita_datatypes_bool.False
 312  | XF -> Matita_datatypes_bool.False)
 313
 314  | XD ->
 315 (match e2 with
 316    X0 -> Matita_datatypes_bool.False
 317  | X1 -> Matita_datatypes_bool.False
 318  | X2 -> Matita_datatypes_bool.False
 319  | X3 -> Matita_datatypes_bool.False
 320  | X4 -> Matita_datatypes_bool.False
 321  | X5 -> Matita_datatypes_bool.False
 322  | X6 -> Matita_datatypes_bool.False
 323  | X7 -> Matita_datatypes_bool.False
 324  | X8 -> Matita_datatypes_bool.False
 325  | X9 -> Matita_datatypes_bool.False
 326  | XA -> Matita_datatypes_bool.False
 327  | XB -> Matita_datatypes_bool.False
 328  | XC -> Matita_datatypes_bool.False
 329  | XD -> Matita_datatypes_bool.True
 330  | XE -> Matita_datatypes_bool.False
 331  | XF -> Matita_datatypes_bool.False)
 332
 333  | XE ->
 334 (match e2 with
 335    X0 -> Matita_datatypes_bool.False
 336  | X1 -> Matita_datatypes_bool.False
 337  | X2 -> Matita_datatypes_bool.False
 338  | X3 -> Matita_datatypes_bool.False
 339  | X4 -> Matita_datatypes_bool.False
 340  | X5 -> Matita_datatypes_bool.False
 341  | X6 -> Matita_datatypes_bool.False
 342  | X7 -> Matita_datatypes_bool.False
 343  | X8 -> Matita_datatypes_bool.False
 344  | X9 -> Matita_datatypes_bool.False
 345  | XA -> Matita_datatypes_bool.False
 346  | XB -> Matita_datatypes_bool.False
 347  | XC -> Matita_datatypes_bool.False
 348  | XD -> Matita_datatypes_bool.False
 349  | XE -> Matita_datatypes_bool.True
 350  | XF -> Matita_datatypes_bool.False)
 351
 352  | XF ->
 353 (match e2 with
 354    X0 -> Matita_datatypes_bool.False
 355  | X1 -> Matita_datatypes_bool.False
 356  | X2 -> Matita_datatypes_bool.False
 357  | X3 -> Matita_datatypes_bool.False
 358  | X4 -> Matita_datatypes_bool.False
 359  | X5 -> Matita_datatypes_bool.False
 360  | X6 -> Matita_datatypes_bool.False
 361  | X7 -> Matita_datatypes_bool.False
 362  | X8 -> Matita_datatypes_bool.False
 363  | X9 -> Matita_datatypes_bool.False
 364  | XA -> Matita_datatypes_bool.False
 365  | XB -> Matita_datatypes_bool.False
 366  | XC -> Matita_datatypes_bool.False
 367  | XD -> Matita_datatypes_bool.False
 368  | XE -> Matita_datatypes_bool.False
 369  | XF -> Matita_datatypes_bool.True)
 370 )
 371 ))
 372 ;;
 373
 374 let lt_ex =
 375 (function e1 -> (function e2 ->
 376 (match e1 with
 377    X0 ->
 378 (match e2 with
 379    X0 -> Matita_datatypes_bool.False
 380  | X1 -> Matita_datatypes_bool.True
 381  | X2 -> Matita_datatypes_bool.True
 382  | X3 -> Matita_datatypes_bool.True
 383  | X4 -> Matita_datatypes_bool.True
 384  | X5 -> Matita_datatypes_bool.True
 385  | X6 -> Matita_datatypes_bool.True
 386  | X7 -> Matita_datatypes_bool.True
 387  | X8 -> Matita_datatypes_bool.True
 388  | X9 -> Matita_datatypes_bool.True
 389  | XA -> Matita_datatypes_bool.True
 390  | XB -> Matita_datatypes_bool.True
 391  | XC -> Matita_datatypes_bool.True
 392  | XD -> Matita_datatypes_bool.True
 393  | XE -> Matita_datatypes_bool.True
 394  | XF -> Matita_datatypes_bool.True)
 395
 396  | X1 ->
 397 (match e2 with
 398    X0 -> Matita_datatypes_bool.False
 399  | X1 -> Matita_datatypes_bool.False
 400  | X2 -> Matita_datatypes_bool.True
 401  | X3 -> Matita_datatypes_bool.True
 402  | X4 -> Matita_datatypes_bool.True
 403  | X5 -> Matita_datatypes_bool.True
 404  | X6 -> Matita_datatypes_bool.True
 405  | X7 -> Matita_datatypes_bool.True
 406  | X8 -> Matita_datatypes_bool.True
 407  | X9 -> Matita_datatypes_bool.True
 408  | XA -> Matita_datatypes_bool.True
 409  | XB -> Matita_datatypes_bool.True
 410  | XC -> Matita_datatypes_bool.True
 411  | XD -> Matita_datatypes_bool.True
 412  | XE -> Matita_datatypes_bool.True
 413  | XF -> Matita_datatypes_bool.True)
 414
 415  | X2 ->
 416 (match e2 with
 417    X0 -> Matita_datatypes_bool.False
 418  | X1 -> Matita_datatypes_bool.False
 419  | X2 -> Matita_datatypes_bool.False
 420  | X3 -> Matita_datatypes_bool.True
 421  | X4 -> Matita_datatypes_bool.True
 422  | X5 -> Matita_datatypes_bool.True
 423  | X6 -> Matita_datatypes_bool.True
 424  | X7 -> Matita_datatypes_bool.True
 425  | X8 -> Matita_datatypes_bool.True
 426  | X9 -> Matita_datatypes_bool.True
 427  | XA -> Matita_datatypes_bool.True
 428  | XB -> Matita_datatypes_bool.True
 429  | XC -> Matita_datatypes_bool.True
 430  | XD -> Matita_datatypes_bool.True
 431  | XE -> Matita_datatypes_bool.True
 432  | XF -> Matita_datatypes_bool.True)
 433
 434  | X3 ->
 435 (match e2 with
 436    X0 -> Matita_datatypes_bool.False
 437  | X1 -> Matita_datatypes_bool.False
 438  | X2 -> Matita_datatypes_bool.False
 439  | X3 -> Matita_datatypes_bool.False
 440  | X4 -> Matita_datatypes_bool.True
 441  | X5 -> Matita_datatypes_bool.True
 442  | X6 -> Matita_datatypes_bool.True
 443  | X7 -> Matita_datatypes_bool.True
 444  | X8 -> Matita_datatypes_bool.True
 445  | X9 -> Matita_datatypes_bool.True
 446  | XA -> Matita_datatypes_bool.True
 447  | XB -> Matita_datatypes_bool.True
 448  | XC -> Matita_datatypes_bool.True
 449  | XD -> Matita_datatypes_bool.True
 450  | XE -> Matita_datatypes_bool.True
 451  | XF -> Matita_datatypes_bool.True)
 452
 453  | X4 ->
 454 (match e2 with
 455    X0 -> Matita_datatypes_bool.False
 456  | X1 -> Matita_datatypes_bool.False
 457  | X2 -> Matita_datatypes_bool.False
 458  | X3 -> Matita_datatypes_bool.False
 459  | X4 -> Matita_datatypes_bool.False
 460  | X5 -> Matita_datatypes_bool.True
 461  | X6 -> Matita_datatypes_bool.True
 462  | X7 -> Matita_datatypes_bool.True
 463  | X8 -> Matita_datatypes_bool.True
 464  | X9 -> Matita_datatypes_bool.True
 465  | XA -> Matita_datatypes_bool.True
 466  | XB -> Matita_datatypes_bool.True
 467  | XC -> Matita_datatypes_bool.True
 468  | XD -> Matita_datatypes_bool.True
 469  | XE -> Matita_datatypes_bool.True
 470  | XF -> Matita_datatypes_bool.True)
 471
 472  | X5 ->
 473 (match e2 with
 474    X0 -> Matita_datatypes_bool.False
 475  | X1 -> Matita_datatypes_bool.False
 476  | X2 -> Matita_datatypes_bool.False
 477  | X3 -> Matita_datatypes_bool.False
 478  | X4 -> Matita_datatypes_bool.False
 479  | X5 -> Matita_datatypes_bool.False
 480  | X6 -> Matita_datatypes_bool.True
 481  | X7 -> Matita_datatypes_bool.True
 482  | X8 -> Matita_datatypes_bool.True
 483  | X9 -> Matita_datatypes_bool.True
 484  | XA -> Matita_datatypes_bool.True
 485  | XB -> Matita_datatypes_bool.True
 486  | XC -> Matita_datatypes_bool.True
 487  | XD -> Matita_datatypes_bool.True
 488  | XE -> Matita_datatypes_bool.True
 489  | XF -> Matita_datatypes_bool.True)
 490
 491  | X6 ->
 492 (match e2 with
 493    X0 -> Matita_datatypes_bool.False
 494  | X1 -> Matita_datatypes_bool.False
 495  | X2 -> Matita_datatypes_bool.False
 496  | X3 -> Matita_datatypes_bool.False
 497  | X4 -> Matita_datatypes_bool.False
 498  | X5 -> Matita_datatypes_bool.False
 499  | X6 -> Matita_datatypes_bool.False
 500  | X7 -> Matita_datatypes_bool.True
 501  | X8 -> Matita_datatypes_bool.True
 502  | X9 -> Matita_datatypes_bool.True
 503  | XA -> Matita_datatypes_bool.True
 504  | XB -> Matita_datatypes_bool.True
 505  | XC -> Matita_datatypes_bool.True
 506  | XD -> Matita_datatypes_bool.True
 507  | XE -> Matita_datatypes_bool.True
 508  | XF -> Matita_datatypes_bool.True)
 509
 510  | X7 ->
 511 (match e2 with
 512    X0 -> Matita_datatypes_bool.False
 513  | X1 -> Matita_datatypes_bool.False
 514  | X2 -> Matita_datatypes_bool.False
 515  | X3 -> Matita_datatypes_bool.False
 516  | X4 -> Matita_datatypes_bool.False
 517  | X5 -> Matita_datatypes_bool.False
 518  | X6 -> Matita_datatypes_bool.False
 519  | X7 -> Matita_datatypes_bool.False
 520  | X8 -> Matita_datatypes_bool.True
 521  | X9 -> Matita_datatypes_bool.True
 522  | XA -> Matita_datatypes_bool.True
 523  | XB -> Matita_datatypes_bool.True
 524  | XC -> Matita_datatypes_bool.True
 525  | XD -> Matita_datatypes_bool.True
 526  | XE -> Matita_datatypes_bool.True
 527  | XF -> Matita_datatypes_bool.True)
 528
 529  | X8 ->
 530 (match e2 with
 531    X0 -> Matita_datatypes_bool.False
 532  | X1 -> Matita_datatypes_bool.False
 533  | X2 -> Matita_datatypes_bool.False
 534  | X3 -> Matita_datatypes_bool.False
 535  | X4 -> Matita_datatypes_bool.False
 536  | X5 -> Matita_datatypes_bool.False
 537  | X6 -> Matita_datatypes_bool.False
 538  | X7 -> Matita_datatypes_bool.False
 539  | X8 -> Matita_datatypes_bool.False
 540  | X9 -> Matita_datatypes_bool.True
 541  | XA -> Matita_datatypes_bool.True
 542  | XB -> Matita_datatypes_bool.True
 543  | XC -> Matita_datatypes_bool.True
 544  | XD -> Matita_datatypes_bool.True
 545  | XE -> Matita_datatypes_bool.True
 546  | XF -> Matita_datatypes_bool.True)
 547
 548  | X9 ->
 549 (match e2 with
 550    X0 -> Matita_datatypes_bool.False
 551  | X1 -> Matita_datatypes_bool.False
 552  | X2 -> Matita_datatypes_bool.False
 553  | X3 -> Matita_datatypes_bool.False
 554  | X4 -> Matita_datatypes_bool.False
 555  | X5 -> Matita_datatypes_bool.False
 556  | X6 -> Matita_datatypes_bool.False
 557  | X7 -> Matita_datatypes_bool.False
 558  | X8 -> Matita_datatypes_bool.False
 559  | X9 -> Matita_datatypes_bool.False
 560  | XA -> Matita_datatypes_bool.True
 561  | XB -> Matita_datatypes_bool.True
 562  | XC -> Matita_datatypes_bool.True
 563  | XD -> Matita_datatypes_bool.True
 564  | XE -> Matita_datatypes_bool.True
 565  | XF -> Matita_datatypes_bool.True)
 566
 567  | XA ->
 568 (match e2 with
 569    X0 -> Matita_datatypes_bool.False
 570  | X1 -> Matita_datatypes_bool.False
 571  | X2 -> Matita_datatypes_bool.False
 572  | X3 -> Matita_datatypes_bool.False
 573  | X4 -> Matita_datatypes_bool.False
 574  | X5 -> Matita_datatypes_bool.False
 575  | X6 -> Matita_datatypes_bool.False
 576  | X7 -> Matita_datatypes_bool.False
 577  | X8 -> Matita_datatypes_bool.False
 578  | X9 -> Matita_datatypes_bool.False
 579  | XA -> Matita_datatypes_bool.False
 580  | XB -> Matita_datatypes_bool.True
 581  | XC -> Matita_datatypes_bool.True
 582  | XD -> Matita_datatypes_bool.True
 583  | XE -> Matita_datatypes_bool.True
 584  | XF -> Matita_datatypes_bool.True)
 585
 586  | XB ->
 587 (match e2 with
 588    X0 -> Matita_datatypes_bool.False
 589  | X1 -> Matita_datatypes_bool.False
 590  | X2 -> Matita_datatypes_bool.False
 591  | X3 -> Matita_datatypes_bool.False
 592  | X4 -> Matita_datatypes_bool.False
 593  | X5 -> Matita_datatypes_bool.False
 594  | X6 -> Matita_datatypes_bool.False
 595  | X7 -> Matita_datatypes_bool.False
 596  | X8 -> Matita_datatypes_bool.False
 597  | X9 -> Matita_datatypes_bool.False
 598  | XA -> Matita_datatypes_bool.False
 599  | XB -> Matita_datatypes_bool.False
 600  | XC -> Matita_datatypes_bool.True
 601  | XD -> Matita_datatypes_bool.True
 602  | XE -> Matita_datatypes_bool.True
 603  | XF -> Matita_datatypes_bool.True)
 604
 605  | XC ->
 606 (match e2 with
 607    X0 -> Matita_datatypes_bool.False
 608  | X1 -> Matita_datatypes_bool.False
 609  | X2 -> Matita_datatypes_bool.False
 610  | X3 -> Matita_datatypes_bool.False
 611  | X4 -> Matita_datatypes_bool.False
 612  | X5 -> Matita_datatypes_bool.False
 613  | X6 -> Matita_datatypes_bool.False
 614  | X7 -> Matita_datatypes_bool.False
 615  | X8 -> Matita_datatypes_bool.False
 616  | X9 -> Matita_datatypes_bool.False
 617  | XA -> Matita_datatypes_bool.False
 618  | XB -> Matita_datatypes_bool.False
 619  | XC -> Matita_datatypes_bool.False
 620  | XD -> Matita_datatypes_bool.True
 621  | XE -> Matita_datatypes_bool.True
 622  | XF -> Matita_datatypes_bool.True)
 623
 624  | XD ->
 625 (match e2 with
 626    X0 -> Matita_datatypes_bool.False
 627  | X1 -> Matita_datatypes_bool.False
 628  | X2 -> Matita_datatypes_bool.False
 629  | X3 -> Matita_datatypes_bool.False
 630  | X4 -> Matita_datatypes_bool.False
 631  | X5 -> Matita_datatypes_bool.False
 632  | X6 -> Matita_datatypes_bool.False
 633  | X7 -> Matita_datatypes_bool.False
 634  | X8 -> Matita_datatypes_bool.False
 635  | X9 -> Matita_datatypes_bool.False
 636  | XA -> Matita_datatypes_bool.False
 637  | XB -> Matita_datatypes_bool.False
 638  | XC -> Matita_datatypes_bool.False
 639  | XD -> Matita_datatypes_bool.False
 640  | XE -> Matita_datatypes_bool.True
 641  | XF -> Matita_datatypes_bool.True)
 642
 643  | XE ->
 644 (match e2 with
 645    X0 -> Matita_datatypes_bool.False
 646  | X1 -> Matita_datatypes_bool.False
 647  | X2 -> Matita_datatypes_bool.False
 648  | X3 -> Matita_datatypes_bool.False
 649  | X4 -> Matita_datatypes_bool.False
 650  | X5 -> Matita_datatypes_bool.False
 651  | X6 -> Matita_datatypes_bool.False
 652  | X7 -> Matita_datatypes_bool.False
 653  | X8 -> Matita_datatypes_bool.False
 654  | X9 -> Matita_datatypes_bool.False
 655  | XA -> Matita_datatypes_bool.False
 656  | XB -> Matita_datatypes_bool.False
 657  | XC -> Matita_datatypes_bool.False
 658  | XD -> Matita_datatypes_bool.False
 659  | XE -> Matita_datatypes_bool.False
 660  | XF -> Matita_datatypes_bool.True)
 661
 662  | XF ->
 663 (match e2 with
 664    X0 -> Matita_datatypes_bool.False
 665  | X1 -> Matita_datatypes_bool.False
 666  | X2 -> Matita_datatypes_bool.False
 667  | X3 -> Matita_datatypes_bool.False
 668  | X4 -> Matita_datatypes_bool.False
 669  | X5 -> Matita_datatypes_bool.False
 670  | X6 -> Matita_datatypes_bool.False
 671  | X7 -> Matita_datatypes_bool.False
 672  | X8 -> Matita_datatypes_bool.False
 673  | X9 -> Matita_datatypes_bool.False
 674  | XA -> Matita_datatypes_bool.False
 675  | XB -> Matita_datatypes_bool.False
 676  | XC -> Matita_datatypes_bool.False
 677  | XD -> Matita_datatypes_bool.False
 678  | XE -> Matita_datatypes_bool.False
 679  | XF -> Matita_datatypes_bool.False)
 680 )
 681 ))
 682 ;;
 683
 684 let le_ex =
 685 (function e1 -> (function e2 ->
 686 (match e1 with
 687    X0 ->
 688 (match e2 with
 689    X0 -> Matita_datatypes_bool.True
 690  | X1 -> Matita_datatypes_bool.True
 691  | X2 -> Matita_datatypes_bool.True
 692  | X3 -> Matita_datatypes_bool.True
 693  | X4 -> Matita_datatypes_bool.True
 694  | X5 -> Matita_datatypes_bool.True
 695  | X6 -> Matita_datatypes_bool.True
 696  | X7 -> Matita_datatypes_bool.True
 697  | X8 -> Matita_datatypes_bool.True
 698  | X9 -> Matita_datatypes_bool.True
 699  | XA -> Matita_datatypes_bool.True
 700  | XB -> Matita_datatypes_bool.True
 701  | XC -> Matita_datatypes_bool.True
 702  | XD -> Matita_datatypes_bool.True
 703  | XE -> Matita_datatypes_bool.True
 704  | XF -> Matita_datatypes_bool.True)
 705
 706  | X1 ->
 707 (match e2 with
 708    X0 -> Matita_datatypes_bool.False
 709  | X1 -> Matita_datatypes_bool.True
 710  | X2 -> Matita_datatypes_bool.True
 711  | X3 -> Matita_datatypes_bool.True
 712  | X4 -> Matita_datatypes_bool.True
 713  | X5 -> Matita_datatypes_bool.True
 714  | X6 -> Matita_datatypes_bool.True
 715  | X7 -> Matita_datatypes_bool.True
 716  | X8 -> Matita_datatypes_bool.True
 717  | X9 -> Matita_datatypes_bool.True
 718  | XA -> Matita_datatypes_bool.True
 719  | XB -> Matita_datatypes_bool.True
 720  | XC -> Matita_datatypes_bool.True
 721  | XD -> Matita_datatypes_bool.True
 722  | XE -> Matita_datatypes_bool.True
 723  | XF -> Matita_datatypes_bool.True)
 724
 725  | X2 ->
 726 (match e2 with
 727    X0 -> Matita_datatypes_bool.False
 728  | X1 -> Matita_datatypes_bool.False
 729  | X2 -> Matita_datatypes_bool.True
 730  | X3 -> Matita_datatypes_bool.True
 731  | X4 -> Matita_datatypes_bool.True
 732  | X5 -> Matita_datatypes_bool.True
 733  | X6 -> Matita_datatypes_bool.True
 734  | X7 -> Matita_datatypes_bool.True
 735  | X8 -> Matita_datatypes_bool.True
 736  | X9 -> Matita_datatypes_bool.True
 737  | XA -> Matita_datatypes_bool.True
 738  | XB -> Matita_datatypes_bool.True
 739  | XC -> Matita_datatypes_bool.True
 740  | XD -> Matita_datatypes_bool.True
 741  | XE -> Matita_datatypes_bool.True
 742  | XF -> Matita_datatypes_bool.True)
 743
 744  | X3 ->
 745 (match e2 with
 746    X0 -> Matita_datatypes_bool.False
 747  | X1 -> Matita_datatypes_bool.False
 748  | X2 -> Matita_datatypes_bool.False
 749  | X3 -> Matita_datatypes_bool.True
 750  | X4 -> Matita_datatypes_bool.True
 751  | X5 -> Matita_datatypes_bool.True
 752  | X6 -> Matita_datatypes_bool.True
 753  | X7 -> Matita_datatypes_bool.True
 754  | X8 -> Matita_datatypes_bool.True
 755  | X9 -> Matita_datatypes_bool.True
 756  | XA -> Matita_datatypes_bool.True
 757  | XB -> Matita_datatypes_bool.True
 758  | XC -> Matita_datatypes_bool.True
 759  | XD -> Matita_datatypes_bool.True
 760  | XE -> Matita_datatypes_bool.True
 761  | XF -> Matita_datatypes_bool.True)
 762
 763  | X4 ->
 764 (match e2 with
 765    X0 -> Matita_datatypes_bool.False
 766  | X1 -> Matita_datatypes_bool.False
 767  | X2 -> Matita_datatypes_bool.False
 768  | X3 -> Matita_datatypes_bool.False
 769  | X4 -> Matita_datatypes_bool.True
 770  | X5 -> Matita_datatypes_bool.True
 771  | X6 -> Matita_datatypes_bool.True
 772  | X7 -> Matita_datatypes_bool.True
 773  | X8 -> Matita_datatypes_bool.True
 774  | X9 -> Matita_datatypes_bool.True
 775  | XA -> Matita_datatypes_bool.True
 776  | XB -> Matita_datatypes_bool.True
 777  | XC -> Matita_datatypes_bool.True
 778  | XD -> Matita_datatypes_bool.True
 779  | XE -> Matita_datatypes_bool.True
 780  | XF -> Matita_datatypes_bool.True)
 781
 782  | X5 ->
 783 (match e2 with
 784    X0 -> Matita_datatypes_bool.False
 785  | X1 -> Matita_datatypes_bool.False
 786  | X2 -> Matita_datatypes_bool.False
 787  | X3 -> Matita_datatypes_bool.False
 788  | X4 -> Matita_datatypes_bool.False
 789  | X5 -> Matita_datatypes_bool.True
 790  | X6 -> Matita_datatypes_bool.True
 791  | X7 -> Matita_datatypes_bool.True
 792  | X8 -> Matita_datatypes_bool.True
 793  | X9 -> Matita_datatypes_bool.True
 794  | XA -> Matita_datatypes_bool.True
 795  | XB -> Matita_datatypes_bool.True
 796  | XC -> Matita_datatypes_bool.True
 797  | XD -> Matita_datatypes_bool.True
 798  | XE -> Matita_datatypes_bool.True
 799  | XF -> Matita_datatypes_bool.True)
 800
 801  | X6 ->
 802 (match e2 with
 803    X0 -> Matita_datatypes_bool.False
 804  | X1 -> Matita_datatypes_bool.False
 805  | X2 -> Matita_datatypes_bool.False
 806  | X3 -> Matita_datatypes_bool.False
 807  | X4 -> Matita_datatypes_bool.False
 808  | X5 -> Matita_datatypes_bool.False
 809  | X6 -> Matita_datatypes_bool.True
 810  | X7 -> Matita_datatypes_bool.True
 811  | X8 -> Matita_datatypes_bool.True
 812  | X9 -> Matita_datatypes_bool.True
 813  | XA -> Matita_datatypes_bool.True
 814  | XB -> Matita_datatypes_bool.True
 815  | XC -> Matita_datatypes_bool.True
 816  | XD -> Matita_datatypes_bool.True
 817  | XE -> Matita_datatypes_bool.True
 818  | XF -> Matita_datatypes_bool.True)
 819
 820  | X7 ->
 821 (match e2 with
 822    X0 -> Matita_datatypes_bool.False
 823  | X1 -> Matita_datatypes_bool.False
 824  | X2 -> Matita_datatypes_bool.False
 825  | X3 -> Matita_datatypes_bool.False
 826  | X4 -> Matita_datatypes_bool.False
 827  | X5 -> Matita_datatypes_bool.False
 828  | X6 -> Matita_datatypes_bool.False
 829  | X7 -> Matita_datatypes_bool.True
 830  | X8 -> Matita_datatypes_bool.True
 831  | X9 -> Matita_datatypes_bool.True
 832  | XA -> Matita_datatypes_bool.True
 833  | XB -> Matita_datatypes_bool.True
 834  | XC -> Matita_datatypes_bool.True
 835  | XD -> Matita_datatypes_bool.True
 836  | XE -> Matita_datatypes_bool.True
 837  | XF -> Matita_datatypes_bool.True)
 838
 839  | X8 ->
 840 (match e2 with
 841    X0 -> Matita_datatypes_bool.False
 842  | X1 -> Matita_datatypes_bool.False
 843  | X2 -> Matita_datatypes_bool.False
 844  | X3 -> Matita_datatypes_bool.False
 845  | X4 -> Matita_datatypes_bool.False
 846  | X5 -> Matita_datatypes_bool.False
 847  | X6 -> Matita_datatypes_bool.False
 848  | X7 -> Matita_datatypes_bool.False
 849  | X8 -> Matita_datatypes_bool.True
 850  | X9 -> Matita_datatypes_bool.True
 851  | XA -> Matita_datatypes_bool.True
 852  | XB -> Matita_datatypes_bool.True
 853  | XC -> Matita_datatypes_bool.True
 854  | XD -> Matita_datatypes_bool.True
 855  | XE -> Matita_datatypes_bool.True
 856  | XF -> Matita_datatypes_bool.True)
 857
 858  | X9 ->
 859 (match e2 with
 860    X0 -> Matita_datatypes_bool.False
 861  | X1 -> Matita_datatypes_bool.False
 862  | X2 -> Matita_datatypes_bool.False
 863  | X3 -> Matita_datatypes_bool.False
 864  | X4 -> Matita_datatypes_bool.False
 865  | X5 -> Matita_datatypes_bool.False
 866  | X6 -> Matita_datatypes_bool.False
 867  | X7 -> Matita_datatypes_bool.False
 868  | X8 -> Matita_datatypes_bool.False
 869  | X9 -> Matita_datatypes_bool.True
 870  | XA -> Matita_datatypes_bool.True
 871  | XB -> Matita_datatypes_bool.True
 872  | XC -> Matita_datatypes_bool.True
 873  | XD -> Matita_datatypes_bool.True
 874  | XE -> Matita_datatypes_bool.True
 875  | XF -> Matita_datatypes_bool.True)
 876
 877  | XA ->
 878 (match e2 with
 879    X0 -> Matita_datatypes_bool.False
 880  | X1 -> Matita_datatypes_bool.False
 881  | X2 -> Matita_datatypes_bool.False
 882  | X3 -> Matita_datatypes_bool.False
 883  | X4 -> Matita_datatypes_bool.False
 884  | X5 -> Matita_datatypes_bool.False
 885  | X6 -> Matita_datatypes_bool.False
 886  | X7 -> Matita_datatypes_bool.False
 887  | X8 -> Matita_datatypes_bool.False
 888  | X9 -> Matita_datatypes_bool.False
 889  | XA -> Matita_datatypes_bool.True
 890  | XB -> Matita_datatypes_bool.True
 891  | XC -> Matita_datatypes_bool.True
 892  | XD -> Matita_datatypes_bool.True
 893  | XE -> Matita_datatypes_bool.True
 894  | XF -> Matita_datatypes_bool.True)
 895
 896  | XB ->
 897 (match e2 with
 898    X0 -> Matita_datatypes_bool.False
 899  | X1 -> Matita_datatypes_bool.False
 900  | X2 -> Matita_datatypes_bool.False
 901  | X3 -> Matita_datatypes_bool.False
 902  | X4 -> Matita_datatypes_bool.False
 903  | X5 -> Matita_datatypes_bool.False
 904  | X6 -> Matita_datatypes_bool.False
 905  | X7 -> Matita_datatypes_bool.False
 906  | X8 -> Matita_datatypes_bool.False
 907  | X9 -> Matita_datatypes_bool.False
 908  | XA -> Matita_datatypes_bool.False
 909  | XB -> Matita_datatypes_bool.True
 910  | XC -> Matita_datatypes_bool.True
 911  | XD -> Matita_datatypes_bool.True
 912  | XE -> Matita_datatypes_bool.True
 913  | XF -> Matita_datatypes_bool.True)
 914
 915  | XC ->
 916 (match e2 with
 917    X0 -> Matita_datatypes_bool.False
 918  | X1 -> Matita_datatypes_bool.False
 919  | X2 -> Matita_datatypes_bool.False
 920  | X3 -> Matita_datatypes_bool.False
 921  | X4 -> Matita_datatypes_bool.False
 922  | X5 -> Matita_datatypes_bool.False
 923  | X6 -> Matita_datatypes_bool.False
 924  | X7 -> Matita_datatypes_bool.False
 925  | X8 -> Matita_datatypes_bool.False
 926  | X9 -> Matita_datatypes_bool.False
 927  | XA -> Matita_datatypes_bool.False
 928  | XB -> Matita_datatypes_bool.False
 929  | XC -> Matita_datatypes_bool.True
 930  | XD -> Matita_datatypes_bool.True
 931  | XE -> Matita_datatypes_bool.True
 932  | XF -> Matita_datatypes_bool.True)
 933
 934  | XD ->
 935 (match e2 with
 936    X0 -> Matita_datatypes_bool.False
 937  | X1 -> Matita_datatypes_bool.False
 938  | X2 -> Matita_datatypes_bool.False
 939  | X3 -> Matita_datatypes_bool.False
 940  | X4 -> Matita_datatypes_bool.False
 941  | X5 -> Matita_datatypes_bool.False
 942  | X6 -> Matita_datatypes_bool.False
 943  | X7 -> Matita_datatypes_bool.False
 944  | X8 -> Matita_datatypes_bool.False
 945  | X9 -> Matita_datatypes_bool.False
 946  | XA -> Matita_datatypes_bool.False
 947  | XB -> Matita_datatypes_bool.False
 948  | XC -> Matita_datatypes_bool.False
 949  | XD -> Matita_datatypes_bool.True
 950  | XE -> Matita_datatypes_bool.True
 951  | XF -> Matita_datatypes_bool.True)
 952
 953  | XE ->
 954 (match e2 with
 955    X0 -> Matita_datatypes_bool.False
 956  | X1 -> Matita_datatypes_bool.False
 957  | X2 -> Matita_datatypes_bool.False
 958  | X3 -> Matita_datatypes_bool.False
 959  | X4 -> Matita_datatypes_bool.False
 960  | X5 -> Matita_datatypes_bool.False
 961  | X6 -> Matita_datatypes_bool.False
 962  | X7 -> Matita_datatypes_bool.False
 963  | X8 -> Matita_datatypes_bool.False
 964  | X9 -> Matita_datatypes_bool.False
 965  | XA -> Matita_datatypes_bool.False
 966  | XB -> Matita_datatypes_bool.False
 967  | XC -> Matita_datatypes_bool.False
 968  | XD -> Matita_datatypes_bool.False
 969  | XE -> Matita_datatypes_bool.True
 970  | XF -> Matita_datatypes_bool.True)
 971
 972  | XF ->
 973 (match e2 with
 974    X0 -> Matita_datatypes_bool.False
 975  | X1 -> Matita_datatypes_bool.False
 976  | X2 -> Matita_datatypes_bool.False
 977  | X3 -> Matita_datatypes_bool.False
 978  | X4 -> Matita_datatypes_bool.False
 979  | X5 -> Matita_datatypes_bool.False
 980  | X6 -> Matita_datatypes_bool.False
 981  | X7 -> Matita_datatypes_bool.False
 982  | X8 -> Matita_datatypes_bool.False
 983  | X9 -> Matita_datatypes_bool.False
 984  | XA -> Matita_datatypes_bool.False
 985  | XB -> Matita_datatypes_bool.False
 986  | XC -> Matita_datatypes_bool.False
 987  | XD -> Matita_datatypes_bool.False
 988  | XE -> Matita_datatypes_bool.False
 989  | XF -> Matita_datatypes_bool.True)
 990 )
 991 ))
 992 ;;
 993
 994 let gt_ex =
 995 (function e1 -> (function e2 ->
 996 (match e1 with
 997    X0 ->
 998 (match e2 with
 999    X0 -> Matita_datatypes_bool.False
1000  | X1 -> Matita_datatypes_bool.False
1001  | X2 -> Matita_datatypes_bool.False
1002  | X3 -> Matita_datatypes_bool.False
1003  | X4 -> Matita_datatypes_bool.False
1004  | X5 -> Matita_datatypes_bool.False
1005  | X6 -> Matita_datatypes_bool.False
1006  | X7 -> Matita_datatypes_bool.False
1007  | X8 -> Matita_datatypes_bool.False
1008  | X9 -> Matita_datatypes_bool.False
1009  | XA -> Matita_datatypes_bool.False
1010  | XB -> Matita_datatypes_bool.False
1011  | XC -> Matita_datatypes_bool.False
1012  | XD -> Matita_datatypes_bool.False
1013  | XE -> Matita_datatypes_bool.False
1014  | XF -> Matita_datatypes_bool.False)
1015
1016  | X1 ->
1017 (match e2 with
1018    X0 -> Matita_datatypes_bool.True
1019  | X1 -> Matita_datatypes_bool.False
1020  | X2 -> Matita_datatypes_bool.False
1021  | X3 -> Matita_datatypes_bool.False
1022  | X4 -> Matita_datatypes_bool.False
1023  | X5 -> Matita_datatypes_bool.False
1024  | X6 -> Matita_datatypes_bool.False
1025  | X7 -> Matita_datatypes_bool.False
1026  | X8 -> Matita_datatypes_bool.False
1027  | X9 -> Matita_datatypes_bool.False
1028  | XA -> Matita_datatypes_bool.False
1029  | XB -> Matita_datatypes_bool.False
1030  | XC -> Matita_datatypes_bool.False
1031  | XD -> Matita_datatypes_bool.False
1032  | XE -> Matita_datatypes_bool.False
1033  | XF -> Matita_datatypes_bool.False)
1034
1035  | X2 ->
1036 (match e2 with
1037    X0 -> Matita_datatypes_bool.True
1038  | X1 -> Matita_datatypes_bool.True
1039  | X2 -> Matita_datatypes_bool.False
1040  | X3 -> Matita_datatypes_bool.False
1041  | X4 -> Matita_datatypes_bool.False
1042  | X5 -> Matita_datatypes_bool.False
1043  | X6 -> Matita_datatypes_bool.False
1044  | X7 -> Matita_datatypes_bool.False
1045  | X8 -> Matita_datatypes_bool.False
1046  | X9 -> Matita_datatypes_bool.False
1047  | XA -> Matita_datatypes_bool.False
1048  | XB -> Matita_datatypes_bool.False
1049  | XC -> Matita_datatypes_bool.False
1050  | XD -> Matita_datatypes_bool.False
1051  | XE -> Matita_datatypes_bool.False
1052  | XF -> Matita_datatypes_bool.False)
1053
1054  | X3 ->
1055 (match e2 with
1056    X0 -> Matita_datatypes_bool.True
1057  | X1 -> Matita_datatypes_bool.True
1058  | X2 -> Matita_datatypes_bool.True
1059  | X3 -> Matita_datatypes_bool.False
1060  | X4 -> Matita_datatypes_bool.False
1061  | X5 -> Matita_datatypes_bool.False
1062  | X6 -> Matita_datatypes_bool.False
1063  | X7 -> Matita_datatypes_bool.False
1064  | X8 -> Matita_datatypes_bool.False
1065  | X9 -> Matita_datatypes_bool.False
1066  | XA -> Matita_datatypes_bool.False
1067  | XB -> Matita_datatypes_bool.False
1068  | XC -> Matita_datatypes_bool.False
1069  | XD -> Matita_datatypes_bool.False
1070  | XE -> Matita_datatypes_bool.False
1071  | XF -> Matita_datatypes_bool.False)
1072
1073  | X4 ->
1074 (match e2 with
1075    X0 -> Matita_datatypes_bool.True
1076  | X1 -> Matita_datatypes_bool.True
1077  | X2 -> Matita_datatypes_bool.True
1078  | X3 -> Matita_datatypes_bool.True
1079  | X4 -> Matita_datatypes_bool.False
1080  | X5 -> Matita_datatypes_bool.False
1081  | X6 -> Matita_datatypes_bool.False
1082  | X7 -> Matita_datatypes_bool.False
1083  | X8 -> Matita_datatypes_bool.False
1084  | X9 -> Matita_datatypes_bool.False
1085  | XA -> Matita_datatypes_bool.False
1086  | XB -> Matita_datatypes_bool.False
1087  | XC -> Matita_datatypes_bool.False
1088  | XD -> Matita_datatypes_bool.False
1089  | XE -> Matita_datatypes_bool.False
1090  | XF -> Matita_datatypes_bool.False)
1091
1092  | X5 ->
1093 (match e2 with
1094    X0 -> Matita_datatypes_bool.True
1095  | X1 -> Matita_datatypes_bool.True
1096  | X2 -> Matita_datatypes_bool.True
1097  | X3 -> Matita_datatypes_bool.True
1098  | X4 -> Matita_datatypes_bool.True
1099  | X5 -> Matita_datatypes_bool.False
1100  | X6 -> Matita_datatypes_bool.False
1101  | X7 -> Matita_datatypes_bool.False
1102  | X8 -> Matita_datatypes_bool.False
1103  | X9 -> Matita_datatypes_bool.False
1104  | XA -> Matita_datatypes_bool.False
1105  | XB -> Matita_datatypes_bool.False
1106  | XC -> Matita_datatypes_bool.False
1107  | XD -> Matita_datatypes_bool.False
1108  | XE -> Matita_datatypes_bool.False
1109  | XF -> Matita_datatypes_bool.False)
1110
1111  | X6 ->
1112 (match e2 with
1113    X0 -> Matita_datatypes_bool.True
1114  | X1 -> Matita_datatypes_bool.True
1115  | X2 -> Matita_datatypes_bool.True
1116  | X3 -> Matita_datatypes_bool.True
1117  | X4 -> Matita_datatypes_bool.True
1118  | X5 -> Matita_datatypes_bool.True
1119  | X6 -> Matita_datatypes_bool.False
1120  | X7 -> Matita_datatypes_bool.False
1121  | X8 -> Matita_datatypes_bool.False
1122  | X9 -> Matita_datatypes_bool.False
1123  | XA -> Matita_datatypes_bool.False
1124  | XB -> Matita_datatypes_bool.False
1125  | XC -> Matita_datatypes_bool.False
1126  | XD -> Matita_datatypes_bool.False
1127  | XE -> Matita_datatypes_bool.False
1128  | XF -> Matita_datatypes_bool.False)
1129
1130  | X7 ->
1131 (match e2 with
1132    X0 -> Matita_datatypes_bool.True
1133  | X1 -> Matita_datatypes_bool.True
1134  | X2 -> Matita_datatypes_bool.True
1135  | X3 -> Matita_datatypes_bool.True
1136  | X4 -> Matita_datatypes_bool.True
1137  | X5 -> Matita_datatypes_bool.True
1138  | X6 -> Matita_datatypes_bool.True
1139  | X7 -> Matita_datatypes_bool.False
1140  | X8 -> Matita_datatypes_bool.False
1141  | X9 -> Matita_datatypes_bool.False
1142  | XA -> Matita_datatypes_bool.False
1143  | XB -> Matita_datatypes_bool.False
1144  | XC -> Matita_datatypes_bool.False
1145  | XD -> Matita_datatypes_bool.False
1146  | XE -> Matita_datatypes_bool.False
1147  | XF -> Matita_datatypes_bool.False)
1148
1149  | X8 ->
1150 (match e2 with
1151    X0 -> Matita_datatypes_bool.True
1152  | X1 -> Matita_datatypes_bool.True
1153  | X2 -> Matita_datatypes_bool.True
1154  | X3 -> Matita_datatypes_bool.True
1155  | X4 -> Matita_datatypes_bool.True
1156  | X5 -> Matita_datatypes_bool.True
1157  | X6 -> Matita_datatypes_bool.True
1158  | X7 -> Matita_datatypes_bool.True
1159  | X8 -> Matita_datatypes_bool.False
1160  | X9 -> Matita_datatypes_bool.False
1161  | XA -> Matita_datatypes_bool.False
1162  | XB -> Matita_datatypes_bool.False
1163  | XC -> Matita_datatypes_bool.False
1164  | XD -> Matita_datatypes_bool.False
1165  | XE -> Matita_datatypes_bool.False
1166  | XF -> Matita_datatypes_bool.False)
1167
1168  | X9 ->
1169 (match e2 with
1170    X0 -> Matita_datatypes_bool.True
1171  | X1 -> Matita_datatypes_bool.True
1172  | X2 -> Matita_datatypes_bool.True
1173  | X3 -> Matita_datatypes_bool.True
1174  | X4 -> Matita_datatypes_bool.True
1175  | X5 -> Matita_datatypes_bool.True
1176  | X6 -> Matita_datatypes_bool.True
1177  | X7 -> Matita_datatypes_bool.True
1178  | X8 -> Matita_datatypes_bool.True
1179  | X9 -> Matita_datatypes_bool.False
1180  | XA -> Matita_datatypes_bool.False
1181  | XB -> Matita_datatypes_bool.False
1182  | XC -> Matita_datatypes_bool.False
1183  | XD -> Matita_datatypes_bool.False
1184  | XE -> Matita_datatypes_bool.False
1185  | XF -> Matita_datatypes_bool.False)
1186
1187  | XA ->
1188 (match e2 with
1189    X0 -> Matita_datatypes_bool.True
1190  | X1 -> Matita_datatypes_bool.True
1191  | X2 -> Matita_datatypes_bool.True
1192  | X3 -> Matita_datatypes_bool.True
1193  | X4 -> Matita_datatypes_bool.True
1194  | X5 -> Matita_datatypes_bool.True
1195  | X6 -> Matita_datatypes_bool.True
1196  | X7 -> Matita_datatypes_bool.True
1197  | X8 -> Matita_datatypes_bool.True
1198  | X9 -> Matita_datatypes_bool.True
1199  | XA -> Matita_datatypes_bool.False
1200  | XB -> Matita_datatypes_bool.False
1201  | XC -> Matita_datatypes_bool.False
1202  | XD -> Matita_datatypes_bool.False
1203  | XE -> Matita_datatypes_bool.False
1204  | XF -> Matita_datatypes_bool.False)
1205
1206  | XB ->
1207 (match e2 with
1208    X0 -> Matita_datatypes_bool.True
1209  | X1 -> Matita_datatypes_bool.True
1210  | X2 -> Matita_datatypes_bool.True
1211  | X3 -> Matita_datatypes_bool.True
1212  | X4 -> Matita_datatypes_bool.True
1213  | X5 -> Matita_datatypes_bool.True
1214  | X6 -> Matita_datatypes_bool.True
1215  | X7 -> Matita_datatypes_bool.True
1216  | X8 -> Matita_datatypes_bool.True
1217  | X9 -> Matita_datatypes_bool.True
1218  | XA -> Matita_datatypes_bool.True
1219  | XB -> Matita_datatypes_bool.False
1220  | XC -> Matita_datatypes_bool.False
1221  | XD -> Matita_datatypes_bool.False
1222  | XE -> Matita_datatypes_bool.False
1223  | XF -> Matita_datatypes_bool.False)
1224
1225  | XC ->
1226 (match e2 with
1227    X0 -> Matita_datatypes_bool.True
1228  | X1 -> Matita_datatypes_bool.True
1229  | X2 -> Matita_datatypes_bool.True
1230  | X3 -> Matita_datatypes_bool.True
1231  | X4 -> Matita_datatypes_bool.True
1232  | X5 -> Matita_datatypes_bool.True
1233  | X6 -> Matita_datatypes_bool.True
1234  | X7 -> Matita_datatypes_bool.True
1235  | X8 -> Matita_datatypes_bool.True
1236  | X9 -> Matita_datatypes_bool.True
1237  | XA -> Matita_datatypes_bool.True
1238  | XB -> Matita_datatypes_bool.True
1239  | XC -> Matita_datatypes_bool.False
1240  | XD -> Matita_datatypes_bool.False
1241  | XE -> Matita_datatypes_bool.False
1242  | XF -> Matita_datatypes_bool.False)
1243
1244  | XD ->
1245 (match e2 with
1246    X0 -> Matita_datatypes_bool.True
1247  | X1 -> Matita_datatypes_bool.True
1248  | X2 -> Matita_datatypes_bool.True
1249  | X3 -> Matita_datatypes_bool.True
1250  | X4 -> Matita_datatypes_bool.True
1251  | X5 -> Matita_datatypes_bool.True
1252  | X6 -> Matita_datatypes_bool.True
1253  | X7 -> Matita_datatypes_bool.True
1254  | X8 -> Matita_datatypes_bool.True
1255  | X9 -> Matita_datatypes_bool.True
1256  | XA -> Matita_datatypes_bool.True
1257  | XB -> Matita_datatypes_bool.True
1258  | XC -> Matita_datatypes_bool.True
1259  | XD -> Matita_datatypes_bool.False
1260  | XE -> Matita_datatypes_bool.False
1261  | XF -> Matita_datatypes_bool.False)
1262
1263  | XE ->
1264 (match e2 with
1265    X0 -> Matita_datatypes_bool.True
1266  | X1 -> Matita_datatypes_bool.True
1267  | X2 -> Matita_datatypes_bool.True
1268  | X3 -> Matita_datatypes_bool.True
1269  | X4 -> Matita_datatypes_bool.True
1270  | X5 -> Matita_datatypes_bool.True
1271  | X6 -> Matita_datatypes_bool.True
1272  | X7 -> Matita_datatypes_bool.True
1273  | X8 -> Matita_datatypes_bool.True
1274  | X9 -> Matita_datatypes_bool.True
1275  | XA -> Matita_datatypes_bool.True
1276  | XB -> Matita_datatypes_bool.True
1277  | XC -> Matita_datatypes_bool.True
1278  | XD -> Matita_datatypes_bool.True
1279  | XE -> Matita_datatypes_bool.False
1280  | XF -> Matita_datatypes_bool.False)
1281
1282  | XF ->
1283 (match e2 with
1284    X0 -> Matita_datatypes_bool.True
1285  | X1 -> Matita_datatypes_bool.True
1286  | X2 -> Matita_datatypes_bool.True
1287  | X3 -> Matita_datatypes_bool.True
1288  | X4 -> Matita_datatypes_bool.True
1289  | X5 -> Matita_datatypes_bool.True
1290  | X6 -> Matita_datatypes_bool.True
1291  | X7 -> Matita_datatypes_bool.True
1292  | X8 -> Matita_datatypes_bool.True
1293  | X9 -> Matita_datatypes_bool.True
1294  | XA -> Matita_datatypes_bool.True
1295  | XB -> Matita_datatypes_bool.True
1296  | XC -> Matita_datatypes_bool.True
1297  | XD -> Matita_datatypes_bool.True
1298  | XE -> Matita_datatypes_bool.True
1299  | XF -> Matita_datatypes_bool.False)
1300 )
1301 ))
1302 ;;
1303
1304 let ge_ex =
1305 (function e1 -> (function e2 ->
1306 (match e1 with
1307    X0 ->
1308 (match e2 with
1309    X0 -> Matita_datatypes_bool.True
1310  | X1 -> Matita_datatypes_bool.False
1311  | X2 -> Matita_datatypes_bool.False
1312  | X3 -> Matita_datatypes_bool.False
1313  | X4 -> Matita_datatypes_bool.False
1314  | X5 -> Matita_datatypes_bool.False
1315  | X6 -> Matita_datatypes_bool.False
1316  | X7 -> Matita_datatypes_bool.False
1317  | X8 -> Matita_datatypes_bool.False
1318  | X9 -> Matita_datatypes_bool.False
1319  | XA -> Matita_datatypes_bool.False
1320  | XB -> Matita_datatypes_bool.False
1321  | XC -> Matita_datatypes_bool.False
1322  | XD -> Matita_datatypes_bool.False
1323  | XE -> Matita_datatypes_bool.False
1324  | XF -> Matita_datatypes_bool.False)
1325
1326  | X1 ->
1327 (match e2 with
1328    X0 -> Matita_datatypes_bool.True
1329  | X1 -> Matita_datatypes_bool.True
1330  | X2 -> Matita_datatypes_bool.False
1331  | X3 -> Matita_datatypes_bool.False
1332  | X4 -> Matita_datatypes_bool.False
1333  | X5 -> Matita_datatypes_bool.False
1334  | X6 -> Matita_datatypes_bool.False
1335  | X7 -> Matita_datatypes_bool.False
1336  | X8 -> Matita_datatypes_bool.False
1337  | X9 -> Matita_datatypes_bool.False
1338  | XA -> Matita_datatypes_bool.False
1339  | XB -> Matita_datatypes_bool.False
1340  | XC -> Matita_datatypes_bool.False
1341  | XD -> Matita_datatypes_bool.False
1342  | XE -> Matita_datatypes_bool.False
1343  | XF -> Matita_datatypes_bool.False)
1344
1345  | X2 ->
1346 (match e2 with
1347    X0 -> Matita_datatypes_bool.True
1348  | X1 -> Matita_datatypes_bool.True
1349  | X2 -> Matita_datatypes_bool.True
1350  | X3 -> Matita_datatypes_bool.False
1351  | X4 -> Matita_datatypes_bool.False
1352  | X5 -> Matita_datatypes_bool.False
1353  | X6 -> Matita_datatypes_bool.False
1354  | X7 -> Matita_datatypes_bool.False
1355  | X8 -> Matita_datatypes_bool.False
1356  | X9 -> Matita_datatypes_bool.False
1357  | XA -> Matita_datatypes_bool.False
1358  | XB -> Matita_datatypes_bool.False
1359  | XC -> Matita_datatypes_bool.False
1360  | XD -> Matita_datatypes_bool.False
1361  | XE -> Matita_datatypes_bool.False
1362  | XF -> Matita_datatypes_bool.False)
1363
1364  | X3 ->
1365 (match e2 with
1366    X0 -> Matita_datatypes_bool.True
1367  | X1 -> Matita_datatypes_bool.True
1368  | X2 -> Matita_datatypes_bool.True
1369  | X3 -> Matita_datatypes_bool.True
1370  | X4 -> Matita_datatypes_bool.False
1371  | X5 -> Matita_datatypes_bool.False
1372  | X6 -> Matita_datatypes_bool.False
1373  | X7 -> Matita_datatypes_bool.False
1374  | X8 -> Matita_datatypes_bool.False
1375  | X9 -> Matita_datatypes_bool.False
1376  | XA -> Matita_datatypes_bool.False
1377  | XB -> Matita_datatypes_bool.False
1378  | XC -> Matita_datatypes_bool.False
1379  | XD -> Matita_datatypes_bool.False
1380  | XE -> Matita_datatypes_bool.False
1381  | XF -> Matita_datatypes_bool.False)
1382
1383  | X4 ->
1384 (match e2 with
1385    X0 -> Matita_datatypes_bool.True
1386  | X1 -> Matita_datatypes_bool.True
1387  | X2 -> Matita_datatypes_bool.True
1388  | X3 -> Matita_datatypes_bool.True
1389  | X4 -> Matita_datatypes_bool.True
1390  | X5 -> Matita_datatypes_bool.False
1391  | X6 -> Matita_datatypes_bool.False
1392  | X7 -> Matita_datatypes_bool.False
1393  | X8 -> Matita_datatypes_bool.False
1394  | X9 -> Matita_datatypes_bool.False
1395  | XA -> Matita_datatypes_bool.False
1396  | XB -> Matita_datatypes_bool.False
1397  | XC -> Matita_datatypes_bool.False
1398  | XD -> Matita_datatypes_bool.False
1399  | XE -> Matita_datatypes_bool.False
1400  | XF -> Matita_datatypes_bool.False)
1401
1402  | X5 ->
1403 (match e2 with
1404    X0 -> Matita_datatypes_bool.True
1405  | X1 -> Matita_datatypes_bool.True
1406  | X2 -> Matita_datatypes_bool.True
1407  | X3 -> Matita_datatypes_bool.True
1408  | X4 -> Matita_datatypes_bool.True
1409  | X5 -> Matita_datatypes_bool.True
1410  | X6 -> Matita_datatypes_bool.False
1411  | X7 -> Matita_datatypes_bool.False
1412  | X8 -> Matita_datatypes_bool.False
1413  | X9 -> Matita_datatypes_bool.False
1414  | XA -> Matita_datatypes_bool.False
1415  | XB -> Matita_datatypes_bool.False
1416  | XC -> Matita_datatypes_bool.False
1417  | XD -> Matita_datatypes_bool.False
1418  | XE -> Matita_datatypes_bool.False
1419  | XF -> Matita_datatypes_bool.False)
1420
1421  | X6 ->
1422 (match e2 with
1423    X0 -> Matita_datatypes_bool.True
1424  | X1 -> Matita_datatypes_bool.True
1425  | X2 -> Matita_datatypes_bool.True
1426  | X3 -> Matita_datatypes_bool.True
1427  | X4 -> Matita_datatypes_bool.True
1428  | X5 -> Matita_datatypes_bool.True
1429  | X6 -> Matita_datatypes_bool.True
1430  | X7 -> Matita_datatypes_bool.False
1431  | X8 -> Matita_datatypes_bool.False
1432  | X9 -> Matita_datatypes_bool.False
1433  | XA -> Matita_datatypes_bool.False
1434  | XB -> Matita_datatypes_bool.False
1435  | XC -> Matita_datatypes_bool.False
1436  | XD -> Matita_datatypes_bool.False
1437  | XE -> Matita_datatypes_bool.False
1438  | XF -> Matita_datatypes_bool.False)
1439
1440  | X7 ->
1441 (match e2 with
1442    X0 -> Matita_datatypes_bool.True
1443  | X1 -> Matita_datatypes_bool.True
1444  | X2 -> Matita_datatypes_bool.True
1445  | X3 -> Matita_datatypes_bool.True
1446  | X4 -> Matita_datatypes_bool.True
1447  | X5 -> Matita_datatypes_bool.True
1448  | X6 -> Matita_datatypes_bool.True
1449  | X7 -> Matita_datatypes_bool.True
1450  | X8 -> Matita_datatypes_bool.False
1451  | X9 -> Matita_datatypes_bool.False
1452  | XA -> Matita_datatypes_bool.False
1453  | XB -> Matita_datatypes_bool.False
1454  | XC -> Matita_datatypes_bool.False
1455  | XD -> Matita_datatypes_bool.False
1456  | XE -> Matita_datatypes_bool.False
1457  | XF -> Matita_datatypes_bool.False)
1458
1459  | X8 ->
1460 (match e2 with
1461    X0 -> Matita_datatypes_bool.True
1462  | X1 -> Matita_datatypes_bool.True
1463  | X2 -> Matita_datatypes_bool.True
1464  | X3 -> Matita_datatypes_bool.True
1465  | X4 -> Matita_datatypes_bool.True
1466  | X5 -> Matita_datatypes_bool.True
1467  | X6 -> Matita_datatypes_bool.True
1468  | X7 -> Matita_datatypes_bool.True
1469  | X8 -> Matita_datatypes_bool.True
1470  | X9 -> Matita_datatypes_bool.False
1471  | XA -> Matita_datatypes_bool.False
1472  | XB -> Matita_datatypes_bool.False
1473  | XC -> Matita_datatypes_bool.False
1474  | XD -> Matita_datatypes_bool.False
1475  | XE -> Matita_datatypes_bool.False
1476  | XF -> Matita_datatypes_bool.False)
1477
1478  | X9 ->
1479 (match e2 with
1480    X0 -> Matita_datatypes_bool.True
1481  | X1 -> Matita_datatypes_bool.True
1482  | X2 -> Matita_datatypes_bool.True
1483  | X3 -> Matita_datatypes_bool.True
1484  | X4 -> Matita_datatypes_bool.True
1485  | X5 -> Matita_datatypes_bool.True
1486  | X6 -> Matita_datatypes_bool.True
1487  | X7 -> Matita_datatypes_bool.True
1488  | X8 -> Matita_datatypes_bool.True
1489  | X9 -> Matita_datatypes_bool.True
1490  | XA -> Matita_datatypes_bool.False
1491  | XB -> Matita_datatypes_bool.False
1492  | XC -> Matita_datatypes_bool.False
1493  | XD -> Matita_datatypes_bool.False
1494  | XE -> Matita_datatypes_bool.False
1495  | XF -> Matita_datatypes_bool.False)
1496
1497  | XA ->
1498 (match e2 with
1499    X0 -> Matita_datatypes_bool.True
1500  | X1 -> Matita_datatypes_bool.True
1501  | X2 -> Matita_datatypes_bool.True
1502  | X3 -> Matita_datatypes_bool.True
1503  | X4 -> Matita_datatypes_bool.True
1504  | X5 -> Matita_datatypes_bool.True
1505  | X6 -> Matita_datatypes_bool.True
1506  | X7 -> Matita_datatypes_bool.True
1507  | X8 -> Matita_datatypes_bool.True
1508  | X9 -> Matita_datatypes_bool.True
1509  | XA -> Matita_datatypes_bool.True
1510  | XB -> Matita_datatypes_bool.False
1511  | XC -> Matita_datatypes_bool.False
1512  | XD -> Matita_datatypes_bool.False
1513  | XE -> Matita_datatypes_bool.False
1514  | XF -> Matita_datatypes_bool.False)
1515
1516  | XB ->
1517 (match e2 with
1518    X0 -> Matita_datatypes_bool.True
1519  | X1 -> Matita_datatypes_bool.True
1520  | X2 -> Matita_datatypes_bool.True
1521  | X3 -> Matita_datatypes_bool.True
1522  | X4 -> Matita_datatypes_bool.True
1523  | X5 -> Matita_datatypes_bool.True
1524  | X6 -> Matita_datatypes_bool.True
1525  | X7 -> Matita_datatypes_bool.True
1526  | X8 -> Matita_datatypes_bool.True
1527  | X9 -> Matita_datatypes_bool.True
1528  | XA -> Matita_datatypes_bool.True
1529  | XB -> Matita_datatypes_bool.True
1530  | XC -> Matita_datatypes_bool.False
1531  | XD -> Matita_datatypes_bool.False
1532  | XE -> Matita_datatypes_bool.False
1533  | XF -> Matita_datatypes_bool.False)
1534
1535  | XC ->
1536 (match e2 with
1537    X0 -> Matita_datatypes_bool.True
1538  | X1 -> Matita_datatypes_bool.True
1539  | X2 -> Matita_datatypes_bool.True
1540  | X3 -> Matita_datatypes_bool.True
1541  | X4 -> Matita_datatypes_bool.True
1542  | X5 -> Matita_datatypes_bool.True
1543  | X6 -> Matita_datatypes_bool.True
1544  | X7 -> Matita_datatypes_bool.True
1545  | X8 -> Matita_datatypes_bool.True
1546  | X9 -> Matita_datatypes_bool.True
1547  | XA -> Matita_datatypes_bool.True
1548  | XB -> Matita_datatypes_bool.True
1549  | XC -> Matita_datatypes_bool.True
1550  | XD -> Matita_datatypes_bool.False
1551  | XE -> Matita_datatypes_bool.False
1552  | XF -> Matita_datatypes_bool.False)
1553
1554  | XD ->
1555 (match e2 with
1556    X0 -> Matita_datatypes_bool.True
1557  | X1 -> Matita_datatypes_bool.True
1558  | X2 -> Matita_datatypes_bool.True
1559  | X3 -> Matita_datatypes_bool.True
1560  | X4 -> Matita_datatypes_bool.True
1561  | X5 -> Matita_datatypes_bool.True
1562  | X6 -> Matita_datatypes_bool.True
1563  | X7 -> Matita_datatypes_bool.True
1564  | X8 -> Matita_datatypes_bool.True
1565  | X9 -> Matita_datatypes_bool.True
1566  | XA -> Matita_datatypes_bool.True
1567  | XB -> Matita_datatypes_bool.True
1568  | XC -> Matita_datatypes_bool.True
1569  | XD -> Matita_datatypes_bool.True
1570  | XE -> Matita_datatypes_bool.False
1571  | XF -> Matita_datatypes_bool.False)
1572
1573  | XE ->
1574 (match e2 with
1575    X0 -> Matita_datatypes_bool.True
1576  | X1 -> Matita_datatypes_bool.True
1577  | X2 -> Matita_datatypes_bool.True
1578  | X3 -> Matita_datatypes_bool.True
1579  | X4 -> Matita_datatypes_bool.True
1580  | X5 -> Matita_datatypes_bool.True
1581  | X6 -> Matita_datatypes_bool.True
1582  | X7 -> Matita_datatypes_bool.True
1583  | X8 -> Matita_datatypes_bool.True
1584  | X9 -> Matita_datatypes_bool.True
1585  | XA -> Matita_datatypes_bool.True
1586  | XB -> Matita_datatypes_bool.True
1587  | XC -> Matita_datatypes_bool.True
1588  | XD -> Matita_datatypes_bool.True
1589  | XE -> Matita_datatypes_bool.True
1590  | XF -> Matita_datatypes_bool.False)
1591
1592  | XF ->
1593 (match e2 with
1594    X0 -> Matita_datatypes_bool.True
1595  | X1 -> Matita_datatypes_bool.True
1596  | X2 -> Matita_datatypes_bool.True
1597  | X3 -> Matita_datatypes_bool.True
1598  | X4 -> Matita_datatypes_bool.True
1599  | X5 -> Matita_datatypes_bool.True
1600  | X6 -> Matita_datatypes_bool.True
1601  | X7 -> Matita_datatypes_bool.True
1602  | X8 -> Matita_datatypes_bool.True
1603  | X9 -> Matita_datatypes_bool.True
1604  | XA -> Matita_datatypes_bool.True
1605  | XB -> Matita_datatypes_bool.True
1606  | XC -> Matita_datatypes_bool.True
1607  | XD -> Matita_datatypes_bool.True
1608  | XE -> Matita_datatypes_bool.True
1609  | XF -> Matita_datatypes_bool.True)
1610 )
1611 ))
1612 ;;
1613
1614 let and_ex =
1615 (function e1 -> (function e2 ->
1616 (match e1 with
1617    X0 ->
1618 (match e2 with
1619    X0 -> X0
1620  | X1 -> X0
1621  | X2 -> X0
1622  | X3 -> X0
1623  | X4 -> X0
1624  | X5 -> X0
1625  | X6 -> X0
1626  | X7 -> X0
1627  | X8 -> X0
1628  | X9 -> X0
1629  | XA -> X0
1630  | XB -> X0
1631  | XC -> X0
1632  | XD -> X0
1633  | XE -> X0
1634  | XF -> X0)
1635
1636  | X1 ->
1637 (match e2 with
1638    X0 -> X0
1639  | X1 -> X1
1640  | X2 -> X0
1641  | X3 -> X1
1642  | X4 -> X0
1643  | X5 -> X1
1644  | X6 -> X0
1645  | X7 -> X1
1646  | X8 -> X0
1647  | X9 -> X1
1648  | XA -> X0
1649  | XB -> X1
1650  | XC -> X0
1651  | XD -> X1
1652  | XE -> X0
1653  | XF -> X1)
1654
1655  | X2 ->
1656 (match e2 with
1657    X0 -> X0
1658  | X1 -> X0
1659  | X2 -> X2
1660  | X3 -> X2
1661  | X4 -> X0
1662  | X5 -> X0
1663  | X6 -> X2
1664  | X7 -> X2
1665  | X8 -> X0
1666  | X9 -> X0
1667  | XA -> X2
1668  | XB -> X2
1669  | XC -> X0
1670  | XD -> X0
1671  | XE -> X2
1672  | XF -> X2)
1673
1674  | X3 ->
1675 (match e2 with
1676    X0 -> X0
1677  | X1 -> X1
1678  | X2 -> X2
1679  | X3 -> X3
1680  | X4 -> X0
1681  | X5 -> X1
1682  | X6 -> X2
1683  | X7 -> X3
1684  | X8 -> X0
1685  | X9 -> X1
1686  | XA -> X2
1687  | XB -> X3
1688  | XC -> X0
1689  | XD -> X1
1690  | XE -> X2
1691  | XF -> X3)
1692
1693  | X4 ->
1694 (match e2 with
1695    X0 -> X0
1696  | X1 -> X0
1697  | X2 -> X0
1698  | X3 -> X0
1699  | X4 -> X4
1700  | X5 -> X4
1701  | X6 -> X4
1702  | X7 -> X4
1703  | X8 -> X0
1704  | X9 -> X0
1705  | XA -> X0
1706  | XB -> X0
1707  | XC -> X4
1708  | XD -> X4
1709  | XE -> X4
1710  | XF -> X4)
1711
1712  | X5 ->
1713 (match e2 with
1714    X0 -> X0
1715  | X1 -> X1
1716  | X2 -> X0
1717  | X3 -> X1
1718  | X4 -> X4
1719  | X5 -> X5
1720  | X6 -> X4
1721  | X7 -> X5
1722  | X8 -> X0
1723  | X9 -> X1
1724  | XA -> X0
1725  | XB -> X1
1726  | XC -> X4
1727  | XD -> X5
1728  | XE -> X4
1729  | XF -> X5)
1730
1731  | X6 ->
1732 (match e2 with
1733    X0 -> X0
1734  | X1 -> X0
1735  | X2 -> X2
1736  | X3 -> X2
1737  | X4 -> X4
1738  | X5 -> X4
1739  | X6 -> X6
1740  | X7 -> X6
1741  | X8 -> X0
1742  | X9 -> X0
1743  | XA -> X2
1744  | XB -> X2
1745  | XC -> X4
1746  | XD -> X4
1747  | XE -> X6
1748  | XF -> X6)
1749
1750  | X7 ->
1751 (match e2 with
1752    X0 -> X0
1753  | X1 -> X1
1754  | X2 -> X2
1755  | X3 -> X3
1756  | X4 -> X4
1757  | X5 -> X5
1758  | X6 -> X6
1759  | X7 -> X7
1760  | X8 -> X0
1761  | X9 -> X1
1762  | XA -> X2
1763  | XB -> X3
1764  | XC -> X4
1765  | XD -> X5
1766  | XE -> X6
1767  | XF -> X7)
1768
1769  | X8 ->
1770 (match e2 with
1771    X0 -> X0
1772  | X1 -> X0
1773  | X2 -> X0
1774  | X3 -> X0
1775  | X4 -> X0
1776  | X5 -> X0
1777  | X6 -> X0
1778  | X7 -> X0
1779  | X8 -> X8
1780  | X9 -> X8
1781  | XA -> X8
1782  | XB -> X8
1783  | XC -> X8
1784  | XD -> X8
1785  | XE -> X8
1786  | XF -> X8)
1787
1788  | X9 ->
1789 (match e2 with
1790    X0 -> X0
1791  | X1 -> X1
1792  | X2 -> X0
1793  | X3 -> X1
1794  | X4 -> X0
1795  | X5 -> X1
1796  | X6 -> X0
1797  | X7 -> X1
1798  | X8 -> X8
1799  | X9 -> X9
1800  | XA -> X8
1801  | XB -> X9
1802  | XC -> X8
1803  | XD -> X9
1804  | XE -> X8
1805  | XF -> X9)
1806
1807  | XA ->
1808 (match e2 with
1809    X0 -> X0
1810  | X1 -> X0
1811  | X2 -> X2
1812  | X3 -> X2
1813  | X4 -> X0
1814  | X5 -> X0
1815  | X6 -> X2
1816  | X7 -> X2
1817  | X8 -> X8
1818  | X9 -> X8
1819  | XA -> XA
1820  | XB -> XA
1821  | XC -> X8
1822  | XD -> X8
1823  | XE -> XA
1824  | XF -> XA)
1825
1826  | XB ->
1827 (match e2 with
1828    X0 -> X0
1829  | X1 -> X1
1830  | X2 -> X2
1831  | X3 -> X3
1832  | X4 -> X0
1833  | X5 -> X1
1834  | X6 -> X2
1835  | X7 -> X3
1836  | X8 -> X8
1837  | X9 -> X9
1838  | XA -> XA
1839  | XB -> XB
1840  | XC -> X8
1841  | XD -> X9
1842  | XE -> XA
1843  | XF -> XB)
1844
1845  | XC ->
1846 (match e2 with
1847    X0 -> X0
1848  | X1 -> X0
1849  | X2 -> X0
1850  | X3 -> X0
1851  | X4 -> X4
1852  | X5 -> X4
1853  | X6 -> X4
1854  | X7 -> X4
1855  | X8 -> X8
1856  | X9 -> X8
1857  | XA -> X8
1858  | XB -> X8
1859  | XC -> XC
1860  | XD -> XC
1861  | XE -> XC
1862  | XF -> XC)
1863
1864  | XD ->
1865 (match e2 with
1866    X0 -> X0
1867  | X1 -> X1
1868  | X2 -> X0
1869  | X3 -> X1
1870  | X4 -> X4
1871  | X5 -> X5
1872  | X6 -> X4
1873  | X7 -> X5
1874  | X8 -> X8
1875  | X9 -> X9
1876  | XA -> X8
1877  | XB -> X9
1878  | XC -> XC
1879  | XD -> XD
1880  | XE -> XC
1881  | XF -> XD)
1882
1883  | XE ->
1884 (match e2 with
1885    X0 -> X0
1886  | X1 -> X0
1887  | X2 -> X2
1888  | X3 -> X2
1889  | X4 -> X4
1890  | X5 -> X4
1891  | X6 -> X6
1892  | X7 -> X6
1893  | X8 -> X8
1894  | X9 -> X8
1895  | XA -> XA
1896  | XB -> XA
1897  | XC -> XC
1898  | XD -> XC
1899  | XE -> XE
1900  | XF -> XE)
1901
1902  | XF ->
1903 (match e2 with
1904    X0 -> X0
1905  | X1 -> X1
1906  | X2 -> X2
1907  | X3 -> X3
1908  | X4 -> X4
1909  | X5 -> X5
1910  | X6 -> X6
1911  | X7 -> X7
1912  | X8 -> X8
1913  | X9 -> X9
1914  | XA -> XA
1915  | XB -> XB
1916  | XC -> XC
1917  | XD -> XD
1918  | XE -> XE
1919  | XF -> XF)
1920 )
1921 ))
1922 ;;
1923
1924 let or_ex =
1925 (function e1 -> (function e2 ->
1926 (match e1 with
1927    X0 ->
1928 (match e2 with
1929    X0 -> X0
1930  | X1 -> X1
1931  | X2 -> X2
1932  | X3 -> X3
1933  | X4 -> X4
1934  | X5 -> X5
1935  | X6 -> X6
1936  | X7 -> X7
1937  | X8 -> X8
1938  | X9 -> X9
1939  | XA -> XA
1940  | XB -> XB
1941  | XC -> XC
1942  | XD -> XD
1943  | XE -> XE
1944  | XF -> XF)
1945
1946  | X1 ->
1947 (match e2 with
1948    X0 -> X1
1949  | X1 -> X1
1950  | X2 -> X3
1951  | X3 -> X3
1952  | X4 -> X5
1953  | X5 -> X5
1954  | X6 -> X7
1955  | X7 -> X7
1956  | X8 -> X9
1957  | X9 -> X9
1958  | XA -> XB
1959  | XB -> XB
1960  | XC -> XD
1961  | XD -> XD
1962  | XE -> XF
1963  | XF -> XF)
1964
1965  | X2 ->
1966 (match e2 with
1967    X0 -> X2
1968  | X1 -> X3
1969  | X2 -> X2
1970  | X3 -> X3
1971  | X4 -> X6
1972  | X5 -> X7
1973  | X6 -> X6
1974  | X7 -> X7
1975  | X8 -> XA
1976  | X9 -> XB
1977  | XA -> XA
1978  | XB -> XB
1979  | XC -> XE
1980  | XD -> XF
1981  | XE -> XE
1982  | XF -> XF)
1983
1984  | X3 ->
1985 (match e2 with
1986    X0 -> X3
1987  | X1 -> X3
1988  | X2 -> X3
1989  | X3 -> X3
1990  | X4 -> X7
1991  | X5 -> X7
1992  | X6 -> X7
1993  | X7 -> X7
1994  | X8 -> XB
1995  | X9 -> XB
1996  | XA -> XB
1997  | XB -> XB
1998  | XC -> XF
1999  | XD -> XF
2000  | XE -> XF
2001  | XF -> XF)
2002
2003  | X4 ->
2004 (match e2 with
2005    X0 -> X4
2006  | X1 -> X5
2007  | X2 -> X6
2008  | X3 -> X7
2009  | X4 -> X4
2010  | X5 -> X5
2011  | X6 -> X6
2012  | X7 -> X7
2013  | X8 -> XC
2014  | X9 -> XD
2015  | XA -> XE
2016  | XB -> XF
2017  | XC -> XC
2018  | XD -> XD
2019  | XE -> XE
2020  | XF -> XF)
2021
2022  | X5 ->
2023 (match e2 with
2024    X0 -> X5
2025  | X1 -> X5
2026  | X2 -> X7
2027  | X3 -> X7
2028  | X4 -> X5
2029  | X5 -> X5
2030  | X6 -> X7
2031  | X7 -> X7
2032  | X8 -> XD
2033  | X9 -> XD
2034  | XA -> XF
2035  | XB -> XF
2036  | XC -> XD
2037  | XD -> XD
2038  | XE -> XF
2039  | XF -> XF)
2040
2041  | X6 ->
2042 (match e2 with
2043    X0 -> X6
2044  | X1 -> X7
2045  | X2 -> X6
2046  | X3 -> X7
2047  | X4 -> X6
2048  | X5 -> X7
2049  | X6 -> X6
2050  | X7 -> X7
2051  | X8 -> XE
2052  | X9 -> XF
2053  | XA -> XE
2054  | XB -> XF
2055  | XC -> XE
2056  | XD -> XF
2057  | XE -> XE
2058  | XF -> XF)
2059
2060  | X7 ->
2061 (match e2 with
2062    X0 -> X7
2063  | X1 -> X7
2064  | X2 -> X7
2065  | X3 -> X7
2066  | X4 -> X7
2067  | X5 -> X7
2068  | X6 -> X7
2069  | X7 -> X7
2070  | X8 -> XF
2071  | X9 -> XF
2072  | XA -> XF
2073  | XB -> XF
2074  | XC -> XF
2075  | XD -> XF
2076  | XE -> XF
2077  | XF -> XF)
2078
2079  | X8 ->
2080 (match e2 with
2081    X0 -> X8
2082  | X1 -> X9
2083  | X2 -> XA
2084  | X3 -> XB
2085  | X4 -> XC
2086  | X5 -> XD
2087  | X6 -> XE
2088  | X7 -> XF
2089  | X8 -> X8
2090  | X9 -> X9
2091  | XA -> XA
2092  | XB -> XB
2093  | XC -> XC
2094  | XD -> XD
2095  | XE -> XE
2096  | XF -> XF)
2097
2098  | X9 ->
2099 (match e2 with
2100    X0 -> X9
2101  | X1 -> X9
2102  | X2 -> XB
2103  | X3 -> XB
2104  | X4 -> XD
2105  | X5 -> XD
2106  | X6 -> XF
2107  | X7 -> XF
2108  | X8 -> X9
2109  | X9 -> X9
2110  | XA -> XB
2111  | XB -> XB
2112  | XC -> XD
2113  | XD -> XD
2114  | XE -> XF
2115  | XF -> XF)
2116
2117  | XA ->
2118 (match e2 with
2119    X0 -> XA
2120  | X1 -> XB
2121  | X2 -> XA
2122  | X3 -> XB
2123  | X4 -> XE
2124  | X5 -> XF
2125  | X6 -> XE
2126  | X7 -> XF
2127  | X8 -> XA
2128  | X9 -> XB
2129  | XA -> XA
2130  | XB -> XB
2131  | XC -> XE
2132  | XD -> XF
2133  | XE -> XE
2134  | XF -> XF)
2135
2136  | XB ->
2137 (match e2 with
2138    X0 -> XB
2139  | X1 -> XB
2140  | X2 -> XB
2141  | X3 -> XB
2142  | X4 -> XF
2143  | X5 -> XF
2144  | X6 -> XF
2145  | X7 -> XF
2146  | X8 -> XB
2147  | X9 -> XB
2148  | XA -> XB
2149  | XB -> XB
2150  | XC -> XF
2151  | XD -> XF
2152  | XE -> XF
2153  | XF -> XF)
2154
2155  | XC ->
2156 (match e2 with
2157    X0 -> XC
2158  | X1 -> XD
2159  | X2 -> XE
2160  | X3 -> XF
2161  | X4 -> XC
2162  | X5 -> XD
2163  | X6 -> XE
2164  | X7 -> XF
2165  | X8 -> XC
2166  | X9 -> XD
2167  | XA -> XE
2168  | XB -> XF
2169  | XC -> XC
2170  | XD -> XD
2171  | XE -> XE
2172  | XF -> XF)
2173
2174  | XD ->
2175 (match e2 with
2176    X0 -> XD
2177  | X1 -> XD
2178  | X2 -> XF
2179  | X3 -> XF
2180  | X4 -> XD
2181  | X5 -> XD
2182  | X6 -> XF
2183  | X7 -> XF
2184  | X8 -> XD
2185  | X9 -> XD
2186  | XA -> XF
2187  | XB -> XF
2188  | XC -> XD
2189  | XD -> XD
2190  | XE -> XF
2191  | XF -> XF)
2192
2193  | XE ->
2194 (match e2 with
2195    X0 -> XE
2196  | X1 -> XF
2197  | X2 -> XE
2198  | X3 -> XF
2199  | X4 -> XE
2200  | X5 -> XF
2201  | X6 -> XE
2202  | X7 -> XF
2203  | X8 -> XE
2204  | X9 -> XF
2205  | XA -> XE
2206  | XB -> XF
2207  | XC -> XE
2208  | XD -> XF
2209  | XE -> XE
2210  | XF -> XF)
2211
2212  | XF ->
2213 (match e2 with
2214    X0 -> XF
2215  | X1 -> XF
2216  | X2 -> XF
2217  | X3 -> XF
2218  | X4 -> XF
2219  | X5 -> XF
2220  | X6 -> XF
2221  | X7 -> XF
2222  | X8 -> XF
2223  | X9 -> XF
2224  | XA -> XF
2225  | XB -> XF
2226  | XC -> XF
2227  | XD -> XF
2228  | XE -> XF
2229  | XF -> XF)
2230 )
2231 ))
2232 ;;
2233
2234 let xor_ex =
2235 (function e1 -> (function e2 ->
2236 (match e1 with
2237    X0 ->
2238 (match e2 with
2239    X0 -> X0
2240  | X1 -> X1
2241  | X2 -> X2
2242  | X3 -> X3
2243  | X4 -> X4
2244  | X5 -> X5
2245  | X6 -> X6
2246  | X7 -> X7
2247  | X8 -> X8
2248  | X9 -> X9
2249  | XA -> XA
2250  | XB -> XB
2251  | XC -> XC
2252  | XD -> XD
2253  | XE -> XE
2254  | XF -> XF)
2255
2256  | X1 ->
2257 (match e2 with
2258    X0 -> X1
2259  | X1 -> X0
2260  | X2 -> X3
2261  | X3 -> X2
2262  | X4 -> X5
2263  | X5 -> X4
2264  | X6 -> X7
2265  | X7 -> X6
2266  | X8 -> X9
2267  | X9 -> X8
2268  | XA -> XB
2269  | XB -> XA
2270  | XC -> XD
2271  | XD -> XC
2272  | XE -> XF
2273  | XF -> XE)
2274
2275  | X2 ->
2276 (match e2 with
2277    X0 -> X2
2278  | X1 -> X3
2279  | X2 -> X0
2280  | X3 -> X1
2281  | X4 -> X6
2282  | X5 -> X7
2283  | X6 -> X4
2284  | X7 -> X5
2285  | X8 -> XA
2286  | X9 -> XB
2287  | XA -> X8
2288  | XB -> X9
2289  | XC -> XE
2290  | XD -> XF
2291  | XE -> XC
2292  | XF -> XD)
2293
2294  | X3 ->
2295 (match e2 with
2296    X0 -> X3
2297  | X1 -> X2
2298  | X2 -> X1
2299  | X3 -> X0
2300  | X4 -> X7
2301  | X5 -> X6
2302  | X6 -> X5
2303  | X7 -> X4
2304  | X8 -> XB
2305  | X9 -> XA
2306  | XA -> X9
2307  | XB -> X8
2308  | XC -> XF
2309  | XD -> XE
2310  | XE -> XD
2311  | XF -> XC)
2312
2313  | X4 ->
2314 (match e2 with
2315    X0 -> X4
2316  | X1 -> X5
2317  | X2 -> X6
2318  | X3 -> X7
2319  | X4 -> X0
2320  | X5 -> X1
2321  | X6 -> X2
2322  | X7 -> X3
2323  | X8 -> XC
2324  | X9 -> XD
2325  | XA -> XE
2326  | XB -> XF
2327  | XC -> X8
2328  | XD -> X9
2329  | XE -> XA
2330  | XF -> XB)
2331
2332  | X5 ->
2333 (match e2 with
2334    X0 -> X5
2335  | X1 -> X4
2336  | X2 -> X7
2337  | X3 -> X6
2338  | X4 -> X1
2339  | X5 -> X0
2340  | X6 -> X3
2341  | X7 -> X2
2342  | X8 -> XD
2343  | X9 -> XC
2344  | XA -> XF
2345  | XB -> XE
2346  | XC -> X9
2347  | XD -> X8
2348  | XE -> XB
2349  | XF -> XA)
2350
2351  | X6 ->
2352 (match e2 with
2353    X0 -> X6
2354  | X1 -> X7
2355  | X2 -> X4
2356  | X3 -> X5
2357  | X4 -> X2
2358  | X5 -> X3
2359  | X6 -> X0
2360  | X7 -> X1
2361  | X8 -> XE
2362  | X9 -> XF
2363  | XA -> XC
2364  | XB -> XD
2365  | XC -> XA
2366  | XD -> XB
2367  | XE -> X8
2368  | XF -> X9)
2369
2370  | X7 ->
2371 (match e2 with
2372    X0 -> X7
2373  | X1 -> X6
2374  | X2 -> X5
2375  | X3 -> X4
2376  | X4 -> X3
2377  | X5 -> X2
2378  | X6 -> X1
2379  | X7 -> X0
2380  | X8 -> XF
2381  | X9 -> XE
2382  | XA -> XD
2383  | XB -> XC
2384  | XC -> XB
2385  | XD -> XA
2386  | XE -> X9
2387  | XF -> X8)
2388
2389  | X8 ->
2390 (match e2 with
2391    X0 -> X8
2392  | X1 -> X9
2393  | X2 -> XA
2394  | X3 -> XB
2395  | X4 -> XC
2396  | X5 -> XD
2397  | X6 -> XE
2398  | X7 -> XF
2399  | X8 -> X0
2400  | X9 -> X1
2401  | XA -> X2
2402  | XB -> X3
2403  | XC -> X4
2404  | XD -> X5
2405  | XE -> X6
2406  | XF -> X7)
2407
2408  | X9 ->
2409 (match e2 with
2410    X0 -> X9
2411  | X1 -> X8
2412  | X2 -> XB
2413  | X3 -> XA
2414  | X4 -> XD
2415  | X5 -> XC
2416  | X6 -> XF
2417  | X7 -> XE
2418  | X8 -> X1
2419  | X9 -> X0
2420  | XA -> X3
2421  | XB -> X2
2422  | XC -> X5
2423  | XD -> X4
2424  | XE -> X7
2425  | XF -> X6)
2426
2427  | XA ->
2428 (match e2 with
2429    X0 -> XA
2430  | X1 -> XB
2431  | X2 -> X8
2432  | X3 -> X9
2433  | X4 -> XE
2434  | X5 -> XF
2435  | X6 -> XC
2436  | X7 -> XD
2437  | X8 -> X2
2438  | X9 -> X3
2439  | XA -> X0
2440  | XB -> X1
2441  | XC -> X6
2442  | XD -> X7
2443  | XE -> X4
2444  | XF -> X5)
2445
2446  | XB ->
2447 (match e2 with
2448    X0 -> XB
2449  | X1 -> XA
2450  | X2 -> X9
2451  | X3 -> X8
2452  | X4 -> XF
2453  | X5 -> XE
2454  | X6 -> XD
2455  | X7 -> XC
2456  | X8 -> X3
2457  | X9 -> X2
2458  | XA -> X1
2459  | XB -> X0
2460  | XC -> X7
2461  | XD -> X6
2462  | XE -> X5
2463  | XF -> X4)
2464
2465  | XC ->
2466 (match e2 with
2467    X0 -> XC
2468  | X1 -> XD
2469  | X2 -> XE
2470  | X3 -> XF
2471  | X4 -> X8
2472  | X5 -> X9
2473  | X6 -> XA
2474  | X7 -> XB
2475  | X8 -> X4
2476  | X9 -> X5
2477  | XA -> X6
2478  | XB -> X7
2479  | XC -> X0
2480  | XD -> X1
2481  | XE -> X2
2482  | XF -> X3)
2483
2484  | XD ->
2485 (match e2 with
2486    X0 -> XD
2487  | X1 -> XC
2488  | X2 -> XF
2489  | X3 -> XE
2490  | X4 -> X9
2491  | X5 -> X8
2492  | X6 -> XB
2493  | X7 -> XA
2494  | X8 -> X5
2495  | X9 -> X4
2496  | XA -> X7
2497  | XB -> X6
2498  | XC -> X1
2499  | XD -> X0
2500  | XE -> X3
2501  | XF -> X2)
2502
2503  | XE ->
2504 (match e2 with
2505    X0 -> XE
2506  | X1 -> XF
2507  | X2 -> XC
2508  | X3 -> XD
2509  | X4 -> XA
2510  | X5 -> XB
2511  | X6 -> X8
2512  | X7 -> X9
2513  | X8 -> X6
2514  | X9 -> X7
2515  | XA -> X4
2516  | XB -> X5
2517  | XC -> X2
2518  | XD -> X3
2519  | XE -> X0
2520  | XF -> X1)
2521
2522  | XF ->
2523 (match e2 with
2524    X0 -> XF
2525  | X1 -> XE
2526  | X2 -> XD
2527  | X3 -> XC
2528  | X4 -> XB
2529  | X5 -> XA
2530  | X6 -> X9
2531  | X7 -> X8
2532  | X8 -> X7
2533  | X9 -> X6
2534  | XA -> X5
2535  | XB -> X4
2536  | XC -> X3
2537  | XD -> X2
2538  | XE -> X1
2539  | XF -> X0)
2540 )
2541 ))
2542 ;;
2543
2544 let rcr_ex =
2545 (function e -> (function c ->
2546 (match c with
2547    Matita_datatypes_bool.True ->
2548 (match e with
2549    X0 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2550  | X1 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
2551  | X2 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2552  | X3 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
2553  | X4 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2554  | X5 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
2555  | X6 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2556  | X7 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
2557  | X8 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2558  | X9 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
2559  | XA -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2560  | XB -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True))
2561  | XC -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2562  | XD -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.True))
2563  | XE -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2564  | XF -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.True)))
2565
2566  | Matita_datatypes_bool.False ->
2567 (match e with
2568    X0 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.False))
2569  | X1 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2570  | X2 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.False))
2571  | X3 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2572  | X4 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
2573  | X5 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2574  | X6 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
2575  | X7 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2576  | X8 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2577  | X9 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2578  | XA -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2579  | XB -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2580  | XC -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2581  | XD -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2582  | XE -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2583  | XF -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True)))
2584 )
2585 ))
2586 ;;
2587
2588 let shr_ex =
2589 (function e ->
2590 (match e with
2591    X0 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.False))
2592  | X1 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2593  | X2 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.False))
2594  | X3 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2595  | X4 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
2596  | X5 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2597  | X6 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
2598  | X7 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2599  | X8 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2600  | X9 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2601  | XA -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2602  | XB -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2603  | XC -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2604  | XD -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2605  | XE -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2606  | XF -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True)))
2607 )
2608 ;;
2609
2610 let ror_ex =
2611 (function e ->
2612 (match e with
2613    X0 -> X0
2614  | X1 -> X8
2615  | X2 -> X1
2616  | X3 -> X9
2617  | X4 -> X2
2618  | X5 -> XA
2619  | X6 -> X3
2620  | X7 -> XB
2621  | X8 -> X4
2622  | X9 -> XC
2623  | XA -> X5
2624  | XB -> XD
2625  | XC -> X6
2626  | XD -> XE
2627  | XE -> X7
2628  | XF -> XF)
2629 )
2630 ;;
2631
2632 let ror_ex_n =
2633 let rec ror_ex_n =
2634 (function e -> (function n ->
2635 (match n with
2636    Matita_nat_nat.O -> e
2637  | Matita_nat_nat.S(n') -> (ror_ex_n (ror_ex e) n'))
2638 )) in ror_ex_n
2639 ;;
2640
2641 let rcl_ex =
2642 (function e -> (function c ->
2643 (match c with
2644    Matita_datatypes_bool.True ->
2645 (match e with
2646    X0 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.False))
2647  | X1 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
2648  | X2 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2649  | X3 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2650  | X4 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2651  | X5 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2652  | X6 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2653  | X7 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2654  | X8 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2655  | X9 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2656  | XA -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2657  | XB -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
2658  | XC -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
2659  | XD -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
2660  | XE -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True))
2661  | XF -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.True)))
2662
2663  | Matita_datatypes_bool.False ->
2664 (match e with
2665    X0 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.False))
2666  | X1 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
2667  | X2 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2668  | X3 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2669  | X4 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2670  | X5 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2671  | X6 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2672  | X7 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2673  | X8 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2674  | X9 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2675  | XA -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2676  | XB -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2677  | XC -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
2678  | XD -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
2679  | XE -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
2680  | XF -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.True)))
2681 )
2682 ))
2683 ;;
2684
2685 let shl_ex =
2686 (function e ->
2687 (match e with
2688    X0 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.False))
2689  | X1 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
2690  | X2 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2691  | X3 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2692  | X4 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2693  | X5 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2694  | X6 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2695  | X7 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2696  | X8 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2697  | X9 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2698  | XA -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2699  | XB -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2700  | XC -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
2701  | XD -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
2702  | XE -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
2703  | XF -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.True)))
2704 )
2705 ;;
2706
2707 let rol_ex =
2708 (function e ->
2709 (match e with
2710    X0 -> X0
2711  | X1 -> X2
2712  | X2 -> X4
2713  | X3 -> X6
2714  | X4 -> X8
2715  | X5 -> XA
2716  | X6 -> XC
2717  | X7 -> XE
2718  | X8 -> X1
2719  | X9 -> X3
2720  | XA -> X5
2721  | XB -> X7
2722  | XC -> X9
2723  | XD -> XB
2724  | XE -> XD
2725  | XF -> XF)
2726 )
2727 ;;
2728
2729 let rol_ex_n =
2730 let rec rol_ex_n =
2731 (function e -> (function n ->
2732 (match n with
2733    Matita_nat_nat.O -> e
2734  | Matita_nat_nat.S(n') -> (rol_ex_n (rol_ex e) n'))
2735 )) in rol_ex_n
2736 ;;
2737
2738 let not_ex =
2739 (function e ->
2740 (match e with
2741    X0 -> XF
2742  | X1 -> XE
2743  | X2 -> XD
2744  | X3 -> XC
2745  | X4 -> XB
2746  | X5 -> XA
2747  | X6 -> X9
2748  | X7 -> X8
2749  | X8 -> X7
2750  | X9 -> X6
2751  | XA -> X5
2752  | XB -> X4
2753  | XC -> X3
2754  | XD -> X2
2755  | XE -> X1
2756  | XF -> X0)
2757 )
2758 ;;
2759
2760 let plus_ex =
2761 (function e1 -> (function e2 -> (function c ->
2762 (match c with
2763    Matita_datatypes_bool.True ->
2764 (match e1 with
2765    X0 ->
2766 (match e2 with
2767    X0 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.False))
2768  | X1 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
2769  | X2 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
2770  | X3 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2771  | X4 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2772  | X5 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2773  | X6 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2774  | X7 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2775  | X8 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2776  | X9 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2777  | XA -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2778  | XB -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2779  | XC -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2780  | XD -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2781  | XE -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2782  | XF -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True)))
2783
2784  | X1 ->
2785 (match e2 with
2786    X0 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
2787  | X1 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
2788  | X2 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2789  | X3 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2790  | X4 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2791  | X5 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2792  | X6 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2793  | X7 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2794  | X8 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2795  | X9 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2796  | XA -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2797  | XB -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2798  | XC -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2799  | XD -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2800  | XE -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2801  | XF -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True)))
2802
2803  | X2 ->
2804 (match e2 with
2805    X0 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
2806  | X1 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2807  | X2 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2808  | X3 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2809  | X4 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2810  | X5 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2811  | X6 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2812  | X7 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2813  | X8 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2814  | X9 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2815  | XA -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2816  | XB -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2817  | XC -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2818  | XD -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2819  | XE -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2820  | XF -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True)))
2821
2822  | X3 ->
2823 (match e2 with
2824    X0 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
2825  | X1 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2826  | X2 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2827  | X3 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2828  | X4 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2829  | X5 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2830  | X6 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2831  | X7 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2832  | X8 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2833  | X9 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2834  | XA -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2835  | XB -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2836  | XC -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2837  | XD -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2838  | XE -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2839  | XF -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True)))
2840
2841  | X4 ->
2842 (match e2 with
2843    X0 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
2844  | X1 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2845  | X2 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2846  | X3 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2847  | X4 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2848  | X5 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2849  | X6 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2850  | X7 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2851  | X8 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2852  | X9 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2853  | XA -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2854  | XB -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2855  | XC -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2856  | XD -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2857  | XE -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2858  | XF -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True)))
2859
2860  | X5 ->
2861 (match e2 with
2862    X0 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
2863  | X1 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2864  | X2 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2865  | X3 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2866  | X4 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2867  | X5 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2868  | X6 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2869  | X7 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2870  | X8 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2871  | X9 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2872  | XA -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2873  | XB -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2874  | XC -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2875  | XD -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2876  | XE -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2877  | XF -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True)))
2878
2879  | X6 ->
2880 (match e2 with
2881    X0 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
2882  | X1 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2883  | X2 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2884  | X3 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2885  | X4 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2886  | X5 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2887  | X6 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2888  | X7 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2889  | X8 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2890  | X9 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2891  | XA -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2892  | XB -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2893  | XC -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2894  | XD -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2895  | XE -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2896  | XF -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True)))
2897
2898  | X7 ->
2899 (match e2 with
2900    X0 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
2901  | X1 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2902  | X2 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2903  | X3 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2904  | X4 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2905  | X5 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2906  | X6 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2907  | X7 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2908  | X8 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2909  | X9 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2910  | XA -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2911  | XB -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2912  | XC -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2913  | XD -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2914  | XE -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2915  | XF -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True)))
2916
2917  | X8 ->
2918 (match e2 with
2919    X0 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
2920  | X1 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2921  | X2 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2922  | X3 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2923  | X4 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2924  | X5 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2925  | X6 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2926  | X7 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2927  | X8 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2928  | X9 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2929  | XA -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2930  | XB -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2931  | XC -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2932  | XD -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2933  | XE -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
2934  | XF -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True)))
2935
2936  | X9 ->
2937 (match e2 with
2938    X0 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
2939  | X1 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2940  | X2 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2941  | X3 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2942  | X4 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2943  | X5 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2944  | X6 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2945  | X7 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2946  | X8 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2947  | X9 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2948  | XA -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2949  | XB -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2950  | XC -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2951  | XD -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
2952  | XE -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
2953  | XF -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True)))
2954
2955  | XA ->
2956 (match e2 with
2957    X0 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
2958  | X1 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2959  | X2 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2960  | X3 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2961  | X4 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2962  | X5 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2963  | X6 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2964  | X7 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2965  | X8 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2966  | X9 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2967  | XA -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2968  | XB -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2969  | XC -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
2970  | XD -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
2971  | XE -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
2972  | XF -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True)))
2973
2974  | XB ->
2975 (match e2 with
2976    X0 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
2977  | X1 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2978  | X2 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2979  | X3 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2980  | X4 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2981  | X5 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
2982  | X6 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
2983  | X7 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
2984  | X8 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
2985  | X9 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
2986  | XA -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
2987  | XB -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
2988  | XC -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
2989  | XD -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
2990  | XE -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
2991  | XF -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True)))
2992
2993  | XC ->
2994 (match e2 with
2995    X0 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
2996  | X1 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
2997  | X2 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
2998  | X3 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
2999  | X4 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3000  | X5 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3001  | X6 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3002  | X7 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3003  | X8 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3004  | X9 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3005  | XA -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3006  | XB -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3007  | XC -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3008  | XD -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3009  | XE -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3010  | XF -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True)))
3011
3012  | XD ->
3013 (match e2 with
3014    X0 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3015  | X1 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3016  | X2 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3017  | X3 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3018  | X4 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3019  | X5 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3020  | X6 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3021  | X7 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3022  | X8 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3023  | X9 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3024  | XA -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3025  | XB -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3026  | XC -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3027  | XD -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3028  | XE -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
3029  | XF -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True)))
3030
3031  | XE ->
3032 (match e2 with
3033    X0 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3034  | X1 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3035  | X2 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3036  | X3 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3037  | X4 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3038  | X5 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3039  | X6 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3040  | X7 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3041  | X8 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3042  | X9 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3043  | XA -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3044  | XB -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3045  | XC -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3046  | XD -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
3047  | XE -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True))
3048  | XF -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.True)))
3049
3050  | XF ->
3051 (match e2 with
3052    X0 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3053  | X1 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3054  | X2 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3055  | X3 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3056  | X4 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3057  | X5 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3058  | X6 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3059  | X7 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3060  | X8 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3061  | X9 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3062  | XA -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3063  | XB -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3064  | XC -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
3065  | XD -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True))
3066  | XE -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.True))
3067  | XF -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.True)))
3068 )
3069
3070  | Matita_datatypes_bool.False ->
3071 (match e1 with
3072    X0 ->
3073 (match e2 with
3074    X0 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.False))
3075  | X1 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.False))
3076  | X2 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
3077  | X3 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
3078  | X4 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
3079  | X5 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
3080  | X6 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3081  | X7 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3082  | X8 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3083  | X9 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3084  | XA -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3085  | XB -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3086  | XC -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3087  | XD -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3088  | XE -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3089  | XF -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False)))
3090
3091  | X1 ->
3092 (match e2 with
3093    X0 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.False))
3094  | X1 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
3095  | X2 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
3096  | X3 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
3097  | X4 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
3098  | X5 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3099  | X6 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3100  | X7 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3101  | X8 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3102  | X9 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3103  | XA -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3104  | XB -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3105  | XC -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3106  | XD -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3107  | XE -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3108  | XF -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True)))
3109
3110  | X2 ->
3111 (match e2 with
3112    X0 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.False))
3113  | X1 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
3114  | X2 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
3115  | X3 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
3116  | X4 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3117  | X5 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3118  | X6 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3119  | X7 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3120  | X8 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3121  | X9 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3122  | XA -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3123  | XB -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3124  | XC -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3125  | XD -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3126  | XE -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3127  | XF -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True)))
3128
3129  | X3 ->
3130 (match e2 with
3131    X0 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.False))
3132  | X1 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
3133  | X2 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
3134  | X3 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3135  | X4 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3136  | X5 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3137  | X6 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3138  | X7 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3139  | X8 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3140  | X9 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3141  | XA -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3142  | XB -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3143  | XC -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3144  | XD -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3145  | XE -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3146  | XF -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True)))
3147
3148  | X4 ->
3149 (match e2 with
3150    X0 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.False))
3151  | X1 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
3152  | X2 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3153  | X3 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3154  | X4 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3155  | X5 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3156  | X6 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3157  | X7 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3158  | X8 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3159  | X9 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3160  | XA -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3161  | XB -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3162  | XC -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3163  | XD -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3164  | XE -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3165  | XF -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True)))
3166
3167  | X5 ->
3168 (match e2 with
3169    X0 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.False))
3170  | X1 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3171  | X2 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3172  | X3 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3173  | X4 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3174  | X5 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3175  | X6 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3176  | X7 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3177  | X8 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3178  | X9 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3179  | XA -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3180  | XB -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3181  | XC -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3182  | XD -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3183  | XE -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3184  | XF -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True)))
3185
3186  | X6 ->
3187 (match e2 with
3188    X0 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.False))
3189  | X1 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3190  | X2 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3191  | X3 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3192  | X4 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3193  | X5 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3194  | X6 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3195  | X7 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3196  | X8 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3197  | X9 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3198  | XA -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3199  | XB -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3200  | XC -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3201  | XD -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3202  | XE -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3203  | XF -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True)))
3204
3205  | X7 ->
3206 (match e2 with
3207    X0 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.False))
3208  | X1 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3209  | X2 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3210  | X3 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3211  | X4 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3212  | X5 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3213  | X6 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3214  | X7 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3215  | X8 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3216  | X9 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3217  | XA -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3218  | XB -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3219  | XC -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3220  | XD -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3221  | XE -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3222  | XF -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True)))
3223
3224  | X8 ->
3225 (match e2 with
3226    X0 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.False))
3227  | X1 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3228  | X2 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3229  | X3 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3230  | X4 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3231  | X5 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3232  | X6 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3233  | X7 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3234  | X8 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3235  | X9 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3236  | XA -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3237  | XB -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3238  | XC -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3239  | XD -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3240  | XE -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3241  | XF -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True)))
3242
3243  | X9 ->
3244 (match e2 with
3245    X0 -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.False))
3246  | X1 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3247  | X2 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3248  | X3 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3249  | X4 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3250  | X5 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3251  | X6 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3252  | X7 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3253  | X8 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3254  | X9 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3255  | XA -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3256  | XB -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3257  | XC -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3258  | XD -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3259  | XE -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3260  | XF -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True)))
3261
3262  | XA ->
3263 (match e2 with
3264    X0 -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.False))
3265  | X1 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3266  | X2 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3267  | X3 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3268  | X4 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3269  | X5 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3270  | X6 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3271  | X7 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3272  | X8 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3273  | X9 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3274  | XA -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3275  | XB -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3276  | XC -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3277  | XD -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3278  | XE -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3279  | XF -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True)))
3280
3281  | XB ->
3282 (match e2 with
3283    X0 -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.False))
3284  | X1 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3285  | X2 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3286  | X3 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3287  | X4 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3288  | X5 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3289  | X6 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3290  | X7 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3291  | X8 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3292  | X9 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3293  | XA -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3294  | XB -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3295  | XC -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3296  | XD -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3297  | XE -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3298  | XF -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True)))
3299
3300  | XC ->
3301 (match e2 with
3302    X0 -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.False))
3303  | X1 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3304  | X2 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3305  | X3 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3306  | X4 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3307  | X5 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3308  | X6 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3309  | X7 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3310  | X8 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3311  | X9 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3312  | XA -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3313  | XB -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3314  | XC -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3315  | XD -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3316  | XE -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3317  | XF -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True)))
3318
3319  | XD ->
3320 (match e2 with
3321    X0 -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.False))
3322  | X1 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3323  | X2 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3324  | X3 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3325  | X4 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3326  | X5 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3327  | X6 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3328  | X7 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3329  | X8 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3330  | X9 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3331  | XA -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3332  | XB -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3333  | XC -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3334  | XD -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3335  | XE -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3336  | XF -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True)))
3337
3338  | XE ->
3339 (match e2 with
3340    X0 -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.False))
3341  | X1 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3342  | X2 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3343  | X3 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3344  | X4 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3345  | X5 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3346  | X6 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3347  | X7 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3348  | X8 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3349  | X9 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3350  | XA -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3351  | XB -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3352  | XC -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3353  | XD -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3354  | XE -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
3355  | XF -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True)))
3356
3357  | XF ->
3358 (match e2 with
3359    X0 -> (Matita_datatypes_constructors.Pair(XF,Matita_datatypes_bool.False))
3360  | X1 -> (Matita_datatypes_constructors.Pair(X0,Matita_datatypes_bool.True))
3361  | X2 -> (Matita_datatypes_constructors.Pair(X1,Matita_datatypes_bool.True))
3362  | X3 -> (Matita_datatypes_constructors.Pair(X2,Matita_datatypes_bool.True))
3363  | X4 -> (Matita_datatypes_constructors.Pair(X3,Matita_datatypes_bool.True))
3364  | X5 -> (Matita_datatypes_constructors.Pair(X4,Matita_datatypes_bool.True))
3365  | X6 -> (Matita_datatypes_constructors.Pair(X5,Matita_datatypes_bool.True))
3366  | X7 -> (Matita_datatypes_constructors.Pair(X6,Matita_datatypes_bool.True))
3367  | X8 -> (Matita_datatypes_constructors.Pair(X7,Matita_datatypes_bool.True))
3368  | X9 -> (Matita_datatypes_constructors.Pair(X8,Matita_datatypes_bool.True))
3369  | XA -> (Matita_datatypes_constructors.Pair(X9,Matita_datatypes_bool.True))
3370  | XB -> (Matita_datatypes_constructors.Pair(XA,Matita_datatypes_bool.True))
3371  | XC -> (Matita_datatypes_constructors.Pair(XB,Matita_datatypes_bool.True))
3372  | XD -> (Matita_datatypes_constructors.Pair(XC,Matita_datatypes_bool.True))
3373  | XE -> (Matita_datatypes_constructors.Pair(XD,Matita_datatypes_bool.True))
3374  | XF -> (Matita_datatypes_constructors.Pair(XE,Matita_datatypes_bool.True)))
3375 )
3376 )
3377 )))
3378 ;;
3379
3380 let plus_exnc =
3381 (function e1 -> (function e2 -> (Matita_datatypes_constructors.fst (plus_ex e1 e2 Matita_datatypes_bool.False))))
3382 ;;
3383
3384 let plus_exc =
3385 (function e1 -> (function e2 -> (Matita_datatypes_constructors.snd (plus_ex e1 e2 Matita_datatypes_bool.False))))
3386 ;;
3387
3388 let mSB_ex =
3389 (function e ->
3390 (match e with
3391    X0 -> Matita_datatypes_bool.False
3392  | X1 -> Matita_datatypes_bool.False
3393  | X2 -> Matita_datatypes_bool.False
3394  | X3 -> Matita_datatypes_bool.False
3395  | X4 -> Matita_datatypes_bool.False
3396  | X5 -> Matita_datatypes_bool.False
3397  | X6 -> Matita_datatypes_bool.False
3398  | X7 -> Matita_datatypes_bool.False
3399  | X8 -> Matita_datatypes_bool.True
3400  | X9 -> Matita_datatypes_bool.True
3401  | XA -> Matita_datatypes_bool.True
3402  | XB -> Matita_datatypes_bool.True
3403  | XC -> Matita_datatypes_bool.True
3404  | XD -> Matita_datatypes_bool.True
3405  | XE -> Matita_datatypes_bool.True
3406  | XF -> Matita_datatypes_bool.True)
3407 )
3408 ;;
3409
3410 let nat_of_exadecim =
3411 (function e ->
3412 (match e with
3413    X0 -> Matita_nat_nat.O
3414  | X1 -> (Matita_nat_nat.S(Matita_nat_nat.O))
3415  | X2 -> (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))
3416  | X3 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))
3417  | X4 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))
3418  | X5 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))
3419  | X6 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))
3420  | X7 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))
3421  | X8 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))
3422  | X9 -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))
3423  | XA -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))))
3424  | XB -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))))))
3425  | XC -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))))))))
3426  | XD -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))))))))))
3427  | XE -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))))))))))))
3428  | XF -> (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))
3429 )
3430 ;;
3431
3432 let exadecim_of_nat =
3433 let rec exadecim_of_nat =
3434 (function n ->
3435 (match n with
3436    Matita_nat_nat.O -> X0
3437  | Matita_nat_nat.S(n) ->
3438 (match n with
3439    Matita_nat_nat.O -> X1
3440  | Matita_nat_nat.S(n) ->
3441 (match n with
3442    Matita_nat_nat.O -> X2
3443  | Matita_nat_nat.S(n) ->
3444 (match n with
3445    Matita_nat_nat.O -> X3
3446  | Matita_nat_nat.S(n) ->
3447 (match n with
3448    Matita_nat_nat.O -> X4
3449  | Matita_nat_nat.S(n) ->
3450 (match n with
3451    Matita_nat_nat.O -> X5
3452  | Matita_nat_nat.S(n) ->
3453 (match n with
3454    Matita_nat_nat.O -> X6
3455  | Matita_nat_nat.S(n) ->
3456 (match n with
3457    Matita_nat_nat.O -> X7
3458  | Matita_nat_nat.S(n) ->
3459 (match n with
3460    Matita_nat_nat.O -> X8
3461  | Matita_nat_nat.S(n) ->
3462 (match n with
3463    Matita_nat_nat.O -> X9
3464  | Matita_nat_nat.S(n) ->
3465 (match n with
3466    Matita_nat_nat.O -> XA
3467  | Matita_nat_nat.S(n) ->
3468 (match n with
3469    Matita_nat_nat.O -> XB
3470  | Matita_nat_nat.S(n) ->
3471 (match n with
3472    Matita_nat_nat.O -> XC
3473  | Matita_nat_nat.S(n) ->
3474 (match n with
3475    Matita_nat_nat.O -> XD
3476  | Matita_nat_nat.S(n) ->
3477 (match n with
3478    Matita_nat_nat.O -> XE
3479  | Matita_nat_nat.S(n) ->
3480 (match n with
3481    Matita_nat_nat.O -> XF
3482  | Matita_nat_nat.S(n) -> (exadecim_of_nat n))
3483 )
3484 )
3485 )
3486 )
3487 )
3488 )
3489 )
3490 )
3491 )
3492 )
3493 )
3494 )
3495 )
3496 )
3497 )
3498 ) in exadecim_of_nat
3499 ;;
3500
3501 let pred_ex =
3502 (function e ->
3503 (match e with
3504    X0 -> XF
3505  | X1 -> X0
3506  | X2 -> X1
3507  | X3 -> X2
3508  | X4 -> X3
3509  | X5 -> X4
3510  | X6 -> X5
3511  | X7 -> X6
3512  | X8 -> X7
3513  | X9 -> X8
3514  | XA -> X9
3515  | XB -> XA
3516  | XC -> XB
3517  | XD -> XC
3518  | XE -> XD
3519  | XF -> XE)
3520 )
3521 ;;
3522
3523 let succ_ex =
3524 (function e ->
3525 (match e with
3526    X0 -> X1
3527  | X1 -> X2
3528  | X2 -> X3
3529  | X3 -> X4
3530  | X4 -> X5
3531  | X5 -> X6
3532  | X6 -> X7
3533  | X7 -> X8
3534  | X8 -> X9
3535  | X9 -> XA
3536  | XA -> XB
3537  | XB -> XC
3538  | XC -> XD
3539  | XD -> XE
3540  | XE -> XF
3541  | XF -> X0)
3542 )
3543 ;;
3544
3545 let compl_ex =
3546 (function e ->
3547 (match e with
3548    X0 -> X0
3549  | X1 -> XF
3550  | X2 -> XE
3551  | X3 -> XD
3552  | X4 -> XC
3553  | X5 -> XB
3554  | X6 -> XA
3555  | X7 -> X9
3556  | X8 -> X8
3557  | X9 -> X7
3558  | XA -> X6
3559  | XB -> X5
3560  | XC -> X4
3561  | XD -> X3
3562  | XE -> X2
3563  | XF -> X1)
3564 )
3565 ;;
3566
3567 let forall_exadecim =
3568 (function p -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (p X0) (p X1)) (p X2)) (p X3)) (p X4)) (p X5)) (p X6)) (p X7)) (p X8)) (p X9)) (p XA)) (p XB)) (p XC)) (p XD)) (p XE)) (p XF)))
3569 ;;
3570