9 (function p -> (function p1 -> (function p2 -> (function p3 -> (function m ->
19 (function p -> (function p1 -> (function p2 -> (function p3 -> (function m ->
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
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 ->
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 )))))))))))))))))))))))))))))))))))
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 ->
112 | MODE_INHX0ADD -> p4
113 | MODE_INHX1ADD -> p5
114 | MODE_INHX2ADD -> p6
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 )))))))))))))))))))))))))))))))))))
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 ->
333 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
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 ->
430 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
438 (function m -> (function f -> (function a ->
444 let any_opcode_rect =
445 (function m -> (function f -> (function a ->
451 type byte8_or_word16 =
452 Byte of Matita_freescale_byte8.byte8
453 | Word of Matita_freescale_word16.word16
456 let byte8_or_word16_rec =
457 (function f -> (function f1 -> (function b ->
464 let byte8_or_word16_rect =
465 (function f -> (function f1 -> (function b ->
472 let byte8_or_word16_OF_bitrigesim =
473 (function a -> (Byte((Matita_freescale_aux_bases.byte8_of_bitrigesim a))))
476 let magic_of_opcode =
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)))
574 (function m -> (function o -> (function o' ->
578 AnyOP(p') -> (Matita_freescale_byte8.eq_b8 (magic_of_opcode p) (magic_of_opcode p')))
583 let magic_of_instr_mode =
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)))
624 (function i -> (function i' -> (Matita_freescale_byte8.eq_b8 (magic_of_instr_mode i) (magic_of_instr_mode i'))))
628 let rec get_byte_count =
629 (function m -> (function b -> (function c -> (function l ->
631 Matita_list_list.Nil -> c
632 | Matita_list_list.Cons(hd,tl) ->
633 (match (Matita_freescale_extra.thd4T hd) with
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))
639 | Word(_) -> (get_byte_count m b c tl))
641 )))) in get_byte_count
645 let rec get_word_count =
646 (function m -> (function b -> (function c -> (function l ->
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)
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))
658 )))) in get_word_count
661 let get_pseudo_count =
662 let rec get_pseudo_count =
663 (function m -> (function o -> (function c -> (function l ->
665 Matita_list_list.Nil -> c
666 | Matita_list_list.Cons(hd,tl) ->
667 (match (Matita_freescale_extra.fst4T hd) with
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))
674 )))) in get_pseudo_count
678 let rec get_mode_count =
679 (function m -> (function i -> (function c -> (function l ->
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))
687 )))) in get_mode_count
690 let test_not_impl_byte =
691 let rec test_not_impl_byte =
692 (function b -> (function l ->
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))
700 )) in test_not_impl_byte
703 let test_not_impl_pseudo =
704 let rec test_not_impl_pseudo =
705 (function o -> (function l ->
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))
713 )) in test_not_impl_pseudo
716 let test_not_impl_mode =
717 let rec test_not_impl_mode =
718 (function i -> (function l ->
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))
726 )) in test_not_impl_mode
730 let rec get_OpIm_count =
731 (function m -> (function o -> (function i -> (function c -> (function l ->
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))
739 ))))) in get_OpIm_count
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)))
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)))))))