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

   1 type mcu_type =
   2 HC05
   3  | HC08
   4  | HCS08
   5  | RS08
   6 ;;
   7
   8 let mcu_type_rec =
   9 (function p -> (function p1 -> (function p2 -> (function p3 -> (function m ->
  10 (match m with
  11    HC05 -> p
  12  | HC08 -> p1
  13  | HCS08 -> p2
  14  | RS08 -> p3)
  15 )))))
  16 ;;
  17
  18 let mcu_type_rect =
  19 (function p -> (function p1 -> (function p2 -> (function p3 -> (function m ->
  20 (match m with
  21    HC05 -> p
  22  | HC08 -> p1
  23  | HCS08 -> p2
  24  | RS08 -> p3)
  25 )))))
  26 ;;
  27
  28 type instr_mode =
  29 MODE_INH
  30  | MODE_INHA
  31  | MODE_INHX
  32  | MODE_INHH
  33  | MODE_INHX0ADD
  34  | MODE_INHX1ADD
  35  | MODE_INHX2ADD
  36  | MODE_IMM1
  37  | MODE_IMM1EXT
  38  | MODE_IMM2
  39  | MODE_DIR1
  40  | MODE_DIR2
  41  | MODE_IX0
  42  | MODE_IX1
  43  | MODE_IX2
  44  | MODE_SP1
  45  | MODE_SP2
  46  | MODE_DIR1_to_DIR1
  47  | MODE_IMM1_to_DIR1
  48  | MODE_IX0p_to_DIR1
  49  | MODE_DIR1_to_IX0p
  50  | MODE_INHA_and_IMM1
  51  | MODE_INHX_and_IMM1
  52  | MODE_IMM1_and_IMM1
  53  | MODE_DIR1_and_IMM1
  54  | MODE_IX0_and_IMM1
  55  | MODE_IX0p_and_IMM1
  56  | MODE_IX1_and_IMM1
  57  | MODE_IX1p_and_IMM1
  58  | MODE_SP1_and_IMM1
  59  | MODE_DIRn of Matita_freescale_aux_bases.oct
  60  | MODE_DIRn_and_IMM1 of Matita_freescale_aux_bases.oct
  61  | MODE_TNY of Matita_freescale_exadecim.exadecim
  62  | MODE_SRT of Matita_freescale_aux_bases.bitrigesim
  63 ;;
  64
  65 let instr_mode_rec =
  66 (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 p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function f -> (function f1 -> (function f2 -> (function f3 -> (function i ->
  67 (match i with
  68    MODE_INH -> p
  69  | MODE_INHA -> p1
  70  | MODE_INHX -> p2
  71  | MODE_INHH -> p3
  72  | MODE_INHX0ADD -> p4
  73  | MODE_INHX1ADD -> p5
  74  | MODE_INHX2ADD -> p6
  75  | MODE_IMM1 -> p7
  76  | MODE_IMM1EXT -> p8
  77  | MODE_IMM2 -> p9
  78  | MODE_DIR1 -> p10
  79  | MODE_DIR2 -> p11
  80  | MODE_IX0 -> p12
  81  | MODE_IX1 -> p13
  82  | MODE_IX2 -> p14
  83  | MODE_SP1 -> p15
  84  | MODE_SP2 -> p16
  85  | MODE_DIR1_to_DIR1 -> p17
  86  | MODE_IMM1_to_DIR1 -> p18
  87  | MODE_IX0p_to_DIR1 -> p19
  88  | MODE_DIR1_to_IX0p -> p20
  89  | MODE_INHA_and_IMM1 -> p21
  90  | MODE_INHX_and_IMM1 -> p22
  91  | MODE_IMM1_and_IMM1 -> p23
  92  | MODE_DIR1_and_IMM1 -> p24
  93  | MODE_IX0_and_IMM1 -> p25
  94  | MODE_IX0p_and_IMM1 -> p26
  95  | MODE_IX1_and_IMM1 -> p27
  96  | MODE_IX1p_and_IMM1 -> p28
  97  | MODE_SP1_and_IMM1 -> p29
  98  | MODE_DIRn(o) -> (f o)
  99  | MODE_DIRn_and_IMM1(o) -> (f1 o)
 100  | MODE_TNY(e) -> (f2 e)
 101  | MODE_SRT(b) -> (f3 b))
 102 )))))))))))))))))))))))))))))))))))
 103 ;;
 104
 105 let instr_mode_rect =
 106 (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 p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function f -> (function f1 -> (function f2 -> (function f3 -> (function i ->
 107 (match i with
 108    MODE_INH -> p
 109  | MODE_INHA -> p1
 110  | MODE_INHX -> p2
 111  | MODE_INHH -> p3
 112  | MODE_INHX0ADD -> p4
 113  | MODE_INHX1ADD -> p5
 114  | MODE_INHX2ADD -> p6
 115  | MODE_IMM1 -> p7
 116  | MODE_IMM1EXT -> p8
 117  | MODE_IMM2 -> p9
 118  | MODE_DIR1 -> p10
 119  | MODE_DIR2 -> p11
 120  | MODE_IX0 -> p12
 121  | MODE_IX1 -> p13
 122  | MODE_IX2 -> p14
 123  | MODE_SP1 -> p15
 124  | MODE_SP2 -> p16
 125  | MODE_DIR1_to_DIR1 -> p17
 126  | MODE_IMM1_to_DIR1 -> p18
 127  | MODE_IX0p_to_DIR1 -> p19
 128  | MODE_DIR1_to_IX0p -> p20
 129  | MODE_INHA_and_IMM1 -> p21
 130  | MODE_INHX_and_IMM1 -> p22
 131  | MODE_IMM1_and_IMM1 -> p23
 132  | MODE_DIR1_and_IMM1 -> p24
 133  | MODE_IX0_and_IMM1 -> p25
 134  | MODE_IX0p_and_IMM1 -> p26
 135  | MODE_IX1_and_IMM1 -> p27
 136  | MODE_IX1p_and_IMM1 -> p28
 137  | MODE_SP1_and_IMM1 -> p29
 138  | MODE_DIRn(o) -> (f o)
 139  | MODE_DIRn_and_IMM1(o) -> (f1 o)
 140  | MODE_TNY(e) -> (f2 e)
 141  | MODE_SRT(b) -> (f3 b))
 142 )))))))))))))))))))))))))))))))))))
 143 ;;
 144
 145 type opcode =
 146 ADC
 147  | ADD
 148  | AIS
 149  | AIX
 150  | AND
 151  | ASL
 152  | ASR
 153  | BCC
 154  | BCLRn
 155  | BCS
 156  | BEQ
 157  | BGE
 158  | BGND
 159  | BGT
 160  | BHCC
 161  | BHCS
 162  | BHI
 163  | BIH
 164  | BIL
 165  | BIT
 166  | BLE
 167  | BLS
 168  | BLT
 169  | BMC
 170  | BMI
 171  | BMS
 172  | BNE
 173  | BPL
 174  | BRA
 175  | BRCLRn
 176  | BRN
 177  | BRSETn
 178  | BSETn
 179  | BSR
 180  | CBEQA
 181  | CBEQX
 182  | CLC
 183  | CLI
 184  | CLR
 185  | CMP
 186  | COM
 187  | CPHX
 188  | CPX
 189  | DAA
 190  | DBNZ
 191  | DEC
 192  | DIV
 193  | EOR
 194  | INC
 195  | JMP
 196  | JSR
 197  | LDA
 198  | LDHX
 199  | LDX
 200  | LSR
 201  | MOV
 202  | MUL
 203  | NEG
 204  | NOP
 205  | NSA
 206  | ORA
 207  | PSHA
 208  | PSHH
 209  | PSHX
 210  | PULA
 211  | PULH
 212  | PULX
 213  | ROL
 214  | ROR
 215  | RSP
 216  | RTI
 217  | RTS
 218  | SBC
 219  | SEC
 220  | SEI
 221  | SHA
 222  | SLA
 223  | STA
 224  | STHX
 225  | STOP
 226  | STX
 227  | SUB
 228  | SWI
 229  | TAP
 230  | TAX
 231  | TPA
 232  | TST
 233  | TSX
 234  | TXA
 235  | TXS
 236  | WAIT
 237 ;;
 238
 239 let opcode_rec =
 240 (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 p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function p30 -> (function p31 -> (function p32 -> (function p33 -> (function p34 -> (function p35 -> (function p36 -> (function p37 -> (function p38 -> (function p39 -> (function p40 -> (function p41 -> (function p42 -> (function p43 -> (function p44 -> (function p45 -> (function p46 -> (function p47 -> (function p48 -> (function p49 -> (function p50 -> (function p51 -> (function p52 -> (function p53 -> (function p54 -> (function p55 -> (function p56 -> (function p57 -> (function p58 -> (function p59 -> (function p60 -> (function p61 -> (function p62 -> (function p63 -> (function p64 -> (function p65 -> (function p66 -> (function p67 -> (function p68 -> (function p69 -> (function p70 -> (function p71 -> (function p72 -> (function p73 -> (function p74 -> (function p75 -> (function p76 -> (function p77 -> (function p78 -> (function p79 -> (function p80 -> (function p81 -> (function p82 -> (function p83 -> (function p84 -> (function p85 -> (function p86 -> (function p87 -> (function p88 -> (function p89 -> (function p90 -> (function o ->
 241 (match o with
 242    ADC -> p
 243  | ADD -> p1
 244  | AIS -> p2
 245  | AIX -> p3
 246  | AND -> p4
 247  | ASL -> p5
 248  | ASR -> p6
 249  | BCC -> p7
 250  | BCLRn -> p8
 251  | BCS -> p9
 252  | BEQ -> p10
 253  | BGE -> p11
 254  | BGND -> p12
 255  | BGT -> p13
 256  | BHCC -> p14
 257  | BHCS -> p15
 258  | BHI -> p16
 259  | BIH -> p17
 260  | BIL -> p18
 261  | BIT -> p19
 262  | BLE -> p20
 263  | BLS -> p21
 264  | BLT -> p22
 265  | BMC -> p23
 266  | BMI -> p24
 267  | BMS -> p25
 268  | BNE -> p26
 269  | BPL -> p27
 270  | BRA -> p28
 271  | BRCLRn -> p29
 272  | BRN -> p30
 273  | BRSETn -> p31
 274  | BSETn -> p32
 275  | BSR -> p33
 276  | CBEQA -> p34
 277  | CBEQX -> p35
 278  | CLC -> p36
 279  | CLI -> p37
 280  | CLR -> p38
 281  | CMP -> p39
 282  | COM -> p40
 283  | CPHX -> p41
 284  | CPX -> p42
 285  | DAA -> p43
 286  | DBNZ -> p44
 287  | DEC -> p45
 288  | DIV -> p46
 289  | EOR -> p47
 290  | INC -> p48
 291  | JMP -> p49
 292  | JSR -> p50
 293  | LDA -> p51
 294  | LDHX -> p52
 295  | LDX -> p53
 296  | LSR -> p54
 297  | MOV -> p55
 298  | MUL -> p56
 299  | NEG -> p57
 300  | NOP -> p58
 301  | NSA -> p59
 302  | ORA -> p60
 303  | PSHA -> p61
 304  | PSHH -> p62
 305  | PSHX -> p63
 306  | PULA -> p64
 307  | PULH -> p65
 308  | PULX -> p66
 309  | ROL -> p67
 310  | ROR -> p68
 311  | RSP -> p69
 312  | RTI -> p70
 313  | RTS -> p71
 314  | SBC -> p72
 315  | SEC -> p73
 316  | SEI -> p74
 317  | SHA -> p75
 318  | SLA -> p76
 319  | STA -> p77
 320  | STHX -> p78
 321  | STOP -> p79
 322  | STX -> p80
 323  | SUB -> p81
 324  | SWI -> p82
 325  | TAP -> p83
 326  | TAX -> p84
 327  | TPA -> p85
 328  | TST -> p86
 329  | TSX -> p87
 330  | TXA -> p88
 331  | TXS -> p89
 332  | WAIT -> p90)
 333 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 334 ;;
 335
 336 let opcode_rect =
 337 (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 p16 -> (function p17 -> (function p18 -> (function p19 -> (function p20 -> (function p21 -> (function p22 -> (function p23 -> (function p24 -> (function p25 -> (function p26 -> (function p27 -> (function p28 -> (function p29 -> (function p30 -> (function p31 -> (function p32 -> (function p33 -> (function p34 -> (function p35 -> (function p36 -> (function p37 -> (function p38 -> (function p39 -> (function p40 -> (function p41 -> (function p42 -> (function p43 -> (function p44 -> (function p45 -> (function p46 -> (function p47 -> (function p48 -> (function p49 -> (function p50 -> (function p51 -> (function p52 -> (function p53 -> (function p54 -> (function p55 -> (function p56 -> (function p57 -> (function p58 -> (function p59 -> (function p60 -> (function p61 -> (function p62 -> (function p63 -> (function p64 -> (function p65 -> (function p66 -> (function p67 -> (function p68 -> (function p69 -> (function p70 -> (function p71 -> (function p72 -> (function p73 -> (function p74 -> (function p75 -> (function p76 -> (function p77 -> (function p78 -> (function p79 -> (function p80 -> (function p81 -> (function p82 -> (function p83 -> (function p84 -> (function p85 -> (function p86 -> (function p87 -> (function p88 -> (function p89 -> (function p90 -> (function o ->
 338 (match o with
 339    ADC -> p
 340  | ADD -> p1
 341  | AIS -> p2
 342  | AIX -> p3
 343  | AND -> p4
 344  | ASL -> p5
 345  | ASR -> p6
 346  | BCC -> p7
 347  | BCLRn -> p8
 348  | BCS -> p9
 349  | BEQ -> p10
 350  | BGE -> p11
 351  | BGND -> p12
 352  | BGT -> p13
 353  | BHCC -> p14
 354  | BHCS -> p15
 355  | BHI -> p16
 356  | BIH -> p17
 357  | BIL -> p18
 358  | BIT -> p19
 359  | BLE -> p20
 360  | BLS -> p21
 361  | BLT -> p22
 362  | BMC -> p23
 363  | BMI -> p24
 364  | BMS -> p25
 365  | BNE -> p26
 366  | BPL -> p27
 367  | BRA -> p28
 368  | BRCLRn -> p29
 369  | BRN -> p30
 370  | BRSETn -> p31
 371  | BSETn -> p32
 372  | BSR -> p33
 373  | CBEQA -> p34
 374  | CBEQX -> p35
 375  | CLC -> p36
 376  | CLI -> p37
 377  | CLR -> p38
 378  | CMP -> p39
 379  | COM -> p40
 380  | CPHX -> p41
 381  | CPX -> p42
 382  | DAA -> p43
 383  | DBNZ -> p44
 384  | DEC -> p45
 385  | DIV -> p46
 386  | EOR -> p47
 387  | INC -> p48
 388  | JMP -> p49
 389  | JSR -> p50
 390  | LDA -> p51
 391  | LDHX -> p52
 392  | LDX -> p53
 393  | LSR -> p54
 394  | MOV -> p55
 395  | MUL -> p56
 396  | NEG -> p57
 397  | NOP -> p58
 398  | NSA -> p59
 399  | ORA -> p60
 400  | PSHA -> p61
 401  | PSHH -> p62
 402  | PSHX -> p63
 403  | PULA -> p64
 404  | PULH -> p65
 405  | PULX -> p66
 406  | ROL -> p67
 407  | ROR -> p68
 408  | RSP -> p69
 409  | RTI -> p70
 410  | RTS -> p71
 411  | SBC -> p72
 412  | SEC -> p73
 413  | SEI -> p74
 414  | SHA -> p75
 415  | SLA -> p76
 416  | STA -> p77
 417  | STHX -> p78
 418  | STOP -> p79
 419  | STX -> p80
 420  | SUB -> p81
 421  | SWI -> p82
 422  | TAP -> p83
 423  | TAX -> p84
 424  | TPA -> p85
 425  | TST -> p86
 426  | TSX -> p87
 427  | TXA -> p88
 428  | TXS -> p89
 429  | WAIT -> p90)
 430 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 431 ;;
 432
 433 type any_opcode =
 434 AnyOP of opcode
 435 ;;
 436
 437 let any_opcode_rec =
 438 (function m -> (function f -> (function a ->
 439 (match a with
 440    AnyOP(o) -> (f o))
 441 )))
 442 ;;
 443
 444 let any_opcode_rect =
 445 (function m -> (function f -> (function a ->
 446 (match a with
 447    AnyOP(o) -> (f o))
 448 )))
 449 ;;
 450
 451 type byte8_or_word16 =
 452 Byte of Matita_freescale_byte8.byte8
 453  | Word of Matita_freescale_word16.word16
 454 ;;
 455
 456 let byte8_or_word16_rec =
 457 (function f -> (function f1 -> (function b ->
 458 (match b with
 459    Byte(b1) -> (f b1)
 460  | Word(w) -> (f1 w))
 461 )))
 462 ;;
 463
 464 let byte8_or_word16_rect =
 465 (function f -> (function f1 -> (function b ->
 466 (match b with
 467    Byte(b1) -> (f b1)
 468  | Word(w) -> (f1 w))
 469 )))
 470 ;;
 471
 472 let byte8_or_word16_OF_bitrigesim =
 473 (function a -> (Byte((Matita_freescale_aux_bases.byte8_of_bitrigesim a))))
 474 ;;
 475
 476 let magic_of_opcode =
 477 (function o ->
 478 (match o with
 479    ADC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 480  | ADD -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))
 481  | AIS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
 482  | AIX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
 483  | AND -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 484  | ASL -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
 485  | ASR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 486  | BCC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
 487  | BCLRn -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 488  | BCS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
 489  | BEQ -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 490  | BGE -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
 491  | BGND -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 492  | BGT -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
 493  | BHCC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 494  | BHCS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
 495  | BHI -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 496  | BIH -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1))
 497  | BIL -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 498  | BIT -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X3))
 499  | BLE -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 500  | BLS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
 501  | BLT -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
 502  | BMC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7))
 503  | BMI -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 504  | BMS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9))
 505  | BNE -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
 506  | BPL -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
 507  | BRA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 508  | BRCLRn -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XD))
 509  | BRN -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE))
 510  | BRSETn -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))
 511  | BSETn -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))
 512  | BSR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))
 513  | CBEQA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X2))
 514  | CBEQX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))
 515  | CLC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))
 516  | CLI -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X5))
 517  | CLR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X6))
 518  | CMP -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X7))
 519  | COM -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8))
 520  | CPHX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X9))
 521  | CPX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))
 522  | DAA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XB))
 523  | DBNZ -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC))
 524  | DEC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD))
 525  | DIV -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XE))
 526  | EOR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XF))
 527  | INC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))
 528  | JMP -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X1))
 529  | JSR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2))
 530  | LDA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X3))
 531  | LDHX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4))
 532  | LDX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X5))
 533  | LSR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X6))
 534  | MOV -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X7))
 535  | MUL -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8))
 536  | NEG -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X9))
 537  | NOP -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XA))
 538  | NSA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XB))
 539  | ORA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))
 540  | PSHA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XD))
 541  | PSHH -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XE))
 542  | PSHX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))
 543  | PULA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0))
 544  | PULH -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X1))
 545  | PULX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X2))
 546  | ROL -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X3))
 547  | ROR -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X4))
 548  | RSP -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5))
 549  | RTI -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6))
 550  | RTS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X7))
 551  | SBC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8))
 552  | SEC -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X9))
 553  | SEI -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XA))
 554  | SHA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB))
 555  | SLA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XC))
 556  | STA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XD))
 557  | STHX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XE))
 558  | STOP -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XF))
 559  | STX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0))
 560  | SUB -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X1))
 561  | SWI -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X2))
 562  | TAP -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X3))
 563  | TAX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4))
 564  | TPA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X5))
 565  | TST -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X6))
 566  | TSX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X7))
 567  | TXA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X8))
 568  | TXS -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X9))
 569  | WAIT -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA)))
 570 )
 571 ;;
 572
 573 let eqop =
 574 (function m -> (function o -> (function o' ->
 575 (match o with
 576    AnyOP(p) ->
 577 (match o' with
 578    AnyOP(p') -> (Matita_freescale_byte8.eq_b8 (magic_of_opcode p) (magic_of_opcode p')))
 579 )
 580 )))
 581 ;;
 582
 583 let magic_of_instr_mode =
 584 (function i ->
 585 (match i with
 586    MODE_INH -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))
 587  | MODE_INHA -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))
 588  | MODE_INHX -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
 589  | MODE_INHH -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))
 590  | MODE_INHX0ADD -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 591  | MODE_INHX1ADD -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))
 592  | MODE_INHX2ADD -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))
 593  | MODE_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))
 594  | MODE_IMM1EXT -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 595  | MODE_IMM2 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))
 596  | MODE_DIR1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))
 597  | MODE_DIR2 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB))
 598  | MODE_IX0 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))
 599  | MODE_IX1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))
 600  | MODE_IX2 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))
 601  | MODE_SP1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))
 602  | MODE_SP2 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 603  | MODE_DIR1_to_DIR1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1))
 604  | MODE_IMM1_to_DIR1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))
 605  | MODE_IX0p_to_DIR1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X3))
 606  | MODE_DIR1_to_IX0p -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4))
 607  | MODE_INHA_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5))
 608  | MODE_INHX_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6))
 609  | MODE_IMM1_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7))
 610  | MODE_DIR1_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))
 611  | MODE_IX0_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9))
 612  | MODE_IX0p_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))
 613  | MODE_IX1_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB))
 614  | MODE_IX1p_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))
 615  | MODE_SP1_and_IMM1 -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XD))
 616  | MODE_DIRn(o) -> (Matita_freescale_byte8.plus_b8nc (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,(Matita_freescale_aux_bases.exadecim_of_oct o))))
 617  | MODE_DIRn_and_IMM1(o) -> (Matita_freescale_byte8.plus_b8nc (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X6)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,(Matita_freescale_aux_bases.exadecim_of_oct o))))
 618  | MODE_TNY(e) -> (Matita_freescale_byte8.plus_b8nc (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XE)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,e)))
 619  | MODE_SRT(t) -> (Matita_freescale_byte8.plus_b8nc (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XE)) (Matita_freescale_aux_bases.byte8_of_bitrigesim t)))
 620 )
 621 ;;
 622
 623 let eqim =
 624 (function i -> (function i' -> (Matita_freescale_byte8.eq_b8 (magic_of_instr_mode i) (magic_of_instr_mode i'))))
 625 ;;
 626
 627 let get_byte_count =
 628 let rec get_byte_count =
 629 (function m -> (function b -> (function c -> (function l ->
 630 (match l with
 631    Matita_list_list.Nil -> c
 632  | Matita_list_list.Cons(hd,tl) ->
 633 (match (Matita_freescale_extra.thd4T hd) with
 634    Byte(b') ->
 635 (match (Matita_freescale_byte8.eq_b8 b b') with
 636    Matita_datatypes_bool.True -> (get_byte_count m b (Matita_nat_nat.S(c)) tl)
 637  | Matita_datatypes_bool.False -> (get_byte_count m b c tl))
 638
 639  | Word(_) -> (get_byte_count m b c tl))
 640 )
 641 )))) in get_byte_count
 642 ;;
 643
 644 let get_word_count =
 645 let rec get_word_count =
 646 (function m -> (function b -> (function c -> (function l ->
 647 (match l with
 648    Matita_list_list.Nil -> c
 649  | Matita_list_list.Cons(hd,tl) ->
 650 (match (Matita_freescale_extra.thd4T hd) with
 651    Byte(_) -> (get_word_count m b c tl)
 652  | Word(w) ->
 653 (match (Matita_freescale_word16.eq_w16 (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE)),b)) w) with
 654    Matita_datatypes_bool.True -> (get_word_count m b (Matita_nat_nat.S(c)) tl)
 655  | Matita_datatypes_bool.False -> (get_word_count m b c tl))
 656 )
 657 )
 658 )))) in get_word_count
 659 ;;
 660
 661 let get_pseudo_count =
 662 let rec get_pseudo_count =
 663 (function m -> (function o -> (function c -> (function l ->
 664 (match l with
 665    Matita_list_list.Nil -> c
 666  | Matita_list_list.Cons(hd,tl) ->
 667 (match (Matita_freescale_extra.fst4T hd) with
 668    AnyOP(o') ->
 669 (match (eqop m (AnyOP(o)) (AnyOP(o'))) with
 670    Matita_datatypes_bool.True -> (get_pseudo_count m o (Matita_nat_nat.S(c)) tl)
 671  | Matita_datatypes_bool.False -> (get_pseudo_count m o c tl))
 672 )
 673 )
 674 )))) in get_pseudo_count
 675 ;;
 676
 677 let get_mode_count =
 678 let rec get_mode_count =
 679 (function m -> (function i -> (function c -> (function l ->
 680 (match l with
 681    Matita_list_list.Nil -> c
 682  | Matita_list_list.Cons(hd,tl) ->
 683 (match (eqim (Matita_freescale_extra.snd4T hd) i) with
 684    Matita_datatypes_bool.True -> (get_mode_count m i (Matita_nat_nat.S(c)) tl)
 685  | Matita_datatypes_bool.False -> (get_mode_count m i c tl))
 686 )
 687 )))) in get_mode_count
 688 ;;
 689
 690 let test_not_impl_byte =
 691 let rec test_not_impl_byte =
 692 (function b -> (function l ->
 693 (match l with
 694    Matita_list_list.Nil -> Matita_datatypes_bool.False
 695  | Matita_list_list.Cons(hd,tl) ->
 696 (match (Matita_freescale_byte8.eq_b8 b hd) with
 697    Matita_datatypes_bool.True -> Matita_datatypes_bool.True
 698  | Matita_datatypes_bool.False -> (test_not_impl_byte b tl))
 699 )
 700 )) in test_not_impl_byte
 701 ;;
 702
 703 let test_not_impl_pseudo =
 704 let rec test_not_impl_pseudo =
 705 (function o -> (function l ->
 706 (match l with
 707    Matita_list_list.Nil -> Matita_datatypes_bool.False
 708  | Matita_list_list.Cons(hd,tl) ->
 709 (match (eqop HC05 (AnyOP(o)) (AnyOP(hd))) with
 710    Matita_datatypes_bool.True -> Matita_datatypes_bool.True
 711  | Matita_datatypes_bool.False -> (test_not_impl_pseudo o tl))
 712 )
 713 )) in test_not_impl_pseudo
 714 ;;
 715
 716 let test_not_impl_mode =
 717 let rec test_not_impl_mode =
 718 (function i -> (function l ->
 719 (match l with
 720    Matita_list_list.Nil -> Matita_datatypes_bool.False
 721  | Matita_list_list.Cons(hd,tl) ->
 722 (match (eqim i hd) with
 723    Matita_datatypes_bool.True -> Matita_datatypes_bool.True
 724  | Matita_datatypes_bool.False -> (test_not_impl_mode i tl))
 725 )
 726 )) in test_not_impl_mode
 727 ;;
 728
 729 let get_OpIm_count =
 730 let rec get_OpIm_count =
 731 (function m -> (function o -> (function i -> (function c -> (function l ->
 732 (match l with
 733    Matita_list_list.Nil -> c
 734  | Matita_list_list.Cons(hd,tl) ->
 735 (match (Matita_freescale_extra.and_bool (eqop m o (Matita_freescale_extra.fst4T hd)) (eqim i (Matita_freescale_extra.snd4T hd))) with
 736    Matita_datatypes_bool.True -> (get_OpIm_count m o i (Matita_nat_nat.S(c)) tl)
 737  | Matita_datatypes_bool.False -> (get_OpIm_count m o i c tl))
 738 )
 739 ))))) in get_OpIm_count
 740 ;;
 741
 742 let forall_opcode =
 743 (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 (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 (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 (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 (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 (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 ADC) (p ADD)) (p AIS)) (p AIX)) (p AND)) (p ASL)) (p ASR)) (p BCC)) (p BCLRn)) (p BCS)) (p BEQ)) (p BGE)) (p BGND)) (p BGT)) (p BHCC)) (p BHCS)) (p BHI)) (p BIH)) (p BIL)) (p BIT)) (p BLE)) (p BLS)) (p BLT)) (p BMC)) (p BMI)) (p BMS)) (p BNE)) (p BPL)) (p BRA)) (p BRCLRn)) (p BRN)) (p BRSETn)) (p BSETn)) (p BSR)) (p CBEQA)) (p CBEQX)) (p CLC)) (p CLI)) (p CLR)) (p CMP)) (p COM)) (p CPHX)) (p CPX)) (p DAA)) (p DBNZ)) (p DEC)) (p DIV)) (p EOR)) (p INC)) (p JMP)) (p JSR)) (p LDA)) (p LDHX)) (p LDX)) (p LSR)) (p MOV)) (p MUL)) (p NEG)) (p NOP)) (p NSA)) (p ORA)) (p PSHA)) (p PSHH)) (p PSHX)) (p PULA)) (p PULH)) (p PULX)) (p ROL)) (p ROR)) (p RSP)) (p RTI)) (p RTS)) (p SBC)) (p SEC)) (p SEI)) (p SHA)) (p SLA)) (p STA)) (p STHX)) (p STOP)) (p STX)) (p SUB)) (p SWI)) (p TAP)) (p TAX)) (p TPA)) (p TST)) (p TSX)) (p TXA)) (p TXS)) (p WAIT)))
 744 ;;
 745
 746 let forall_instr_mode =
 747 (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 (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 (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (p MODE_INH) (p MODE_INHA)) (p MODE_INHX)) (p MODE_INHH)) (p MODE_INHX0ADD)) (p MODE_INHX1ADD)) (p MODE_INHX2ADD)) (p MODE_IMM1)) (p MODE_IMM1EXT)) (p MODE_IMM2)) (p MODE_DIR1)) (p MODE_DIR2)) (p MODE_IX0)) (p MODE_IX1)) (p MODE_IX2)) (p MODE_SP1)) (p MODE_SP2)) (p MODE_DIR1_to_DIR1)) (p MODE_IMM1_to_DIR1)) (p MODE_IX0p_to_DIR1)) (p MODE_DIR1_to_IX0p)) (p MODE_INHA_and_IMM1)) (p MODE_INHX_and_IMM1)) (p MODE_IMM1_and_IMM1)) (p MODE_DIR1_and_IMM1)) (p MODE_IX0_and_IMM1)) (p MODE_IX0p_and_IMM1)) (p MODE_IX1_and_IMM1)) (p MODE_IX1p_and_IMM1)) (p MODE_SP1_and_IMM1)) (Matita_freescale_aux_bases.forall_oct (function o -> (p (MODE_DIRn(o)))))) (Matita_freescale_aux_bases.forall_oct (function o -> (p (MODE_DIRn_and_IMM1(o)))))) (Matita_freescale_exadecim.forall_exadecim (function e -> (p (MODE_TNY(e)))))) (Matita_freescale_aux_bases.forall_bitrigesim (function t -> (p (MODE_SRT(t)))))))
 748 ;;
 749