1 let dTest_HCS08_sReverse_source =
2 (function elems -> (let m = Matita_freescale_opcode.HCS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.LDA Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.LDA Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.STA Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.STA Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.RTS Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaIMM2(elems))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BRA (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.SUB (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.STA Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.SBC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.LDX Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TXA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BSR (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.LSR Matita_freescale_translation.MaINHA) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.ROR Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BHI (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XD)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
5 let dTest_HCS08_sReverse_status =
6 (function t -> (function a_op -> (function hX_op -> (function elems -> (function data -> (Matita_freescale_status.set_acc_8_low_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_z_flag Matita_freescale_opcode.HCS08 t (Matita_freescale_status.setweak_sp_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.setweak_indX_16_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_pc_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_model.start_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08GB60)) t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.zero_memory t) (dTest_HCS08_sReverse_source elems) Matita_freescale_medium_tests_tools.dTest_HCS08_prog) data Matita_freescale_medium_tests_tools.dTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08GB60)) t) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0))))) hX_op) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XA))))) Matita_datatypes_bool.True) a_op))))))
11 (match (Matita_freescale_multivm.execute Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_multivm.TickOK((dTest_HCS08_sReverse_status Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB)))) (Matita_freescale_medium_tests_tools.byte8_strlen string) string))) (Matita_nat_plus.plus (Matita_nat_plus.plus (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.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.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Matita_nat_times.times (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.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.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.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.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.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Matita_freescale_word16.nat_of_word16 (Matita_freescale_medium_tests_tools.byte8_strlen string)))) (Matita_nat_times.times (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))) (Matita_nat_div_and_mod.div (Matita_freescale_word16.nat_of_word16 (Matita_freescale_medium_tests_tools.byte8_strlen string)) (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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
12 Matita_freescale_multivm.TickERR(s,_) -> (Matita_datatypes_constructors.None)
13 | Matita_freescale_multivm.TickSUSP(s,_) -> (Matita_datatypes_constructors.None)
14 | Matita_freescale_multivm.TickOK(s) -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s (Matita_freescale_memory_abs.load_from_source_at Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s) Matita_freescale_medium_tests_tools.dTest_zeros (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))))
20 (match (Matita_freescale_multivm.execute Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_multivm.TickOK((dTest_HCS08_sReverse_status Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB)))) (Matita_freescale_medium_tests_tools.byte8_strlen string) string)))
22 Matita_freescale_word16.nat_of_word16(Matita_freescale_word16.Mk_word16(
23 Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XF),
24 Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X9)))
27 Matita_freescale_multivm.TickERR(s,_) -> (Matita_datatypes_constructors.None)
28 | Matita_freescale_multivm.TickSUSP(s,_) -> (Matita_datatypes_constructors.None)
29 | Matita_freescale_multivm.TickOK(s) -> (Matita_datatypes_constructors.Some(s)))
34 (function string -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_pc_reg Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (dTest_HCS08_sReverse_status Matita_freescale_memory_abs.MEM_TREE (Matita_datatypes_constructors.fst(Matita_freescale_byte8.shr_b8(Matita_freescale_word16.w16h(Matita_freescale_medium_tests_tools.byte8_strlen string)))) (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_freescale_medium_tests_tools.byte8_strlen string))) (Matita_freescale_medium_tests_tools.byte8_strlen string) (Matita_freescale_medium_tests_tools.byte8_reverse string)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XB))))))))
37 let dTest_HCS08_cSort_source =
38 (function elems -> (let m = Matita_freescale_opcode.HCS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BRA (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XD))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.ASL Matita_freescale_translation.MaINHA) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.ROL Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TXA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.INC Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.INC Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaIMM2(elems))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BCS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XB))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.CLR Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BRA (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.ASL Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.ROL Matita_freescale_translation.MaINHA) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.INC Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X8))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.STOP Matita_freescale_translation.MaINH))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
41 let dTest_HCS08_cSort_status =
42 (function t -> (function i_op -> (function a_op -> (function hX_op -> (function elems -> (function data -> (Matita_freescale_status.setweak_i_flag Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_acc_8_low_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_z_flag Matita_freescale_opcode.HCS08 t (Matita_freescale_status.setweak_sp_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.setweak_indX_16_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_pc_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_model.start_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08GB60)) t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.zero_memory t) (dTest_HCS08_cSort_source elems) Matita_freescale_medium_tests_tools.dTest_HCS08_prog) data Matita_freescale_medium_tests_tools.dTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08GB60)) t) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False) Matita_freescale_medium_tests_tools.dTest_HCS08_prog) hX_op) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB))))) Matita_datatypes_bool.True) a_op) i_op)))))))
47 (match (Matita_freescale_multivm.execute Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_multivm.TickOK((dTest_HCS08_cSort_status Matita_freescale_memory_abs.MEM_TREE Matita_datatypes_bool.True (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XC)))) (Matita_freescale_medium_tests_tools.byte8_strlen string) string))) (Matita_nat_plus.plus (Matita_freescale_word16.nat_of_word16 (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4))))) (Matita_nat_times.times (Matita_freescale_byte8.nat_of_byte8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X6))) (Matita_freescale_word16.nat_of_word16 (Matita_freescale_medium_tests_tools.byte8_strlen string))))) with
48 Matita_freescale_multivm.TickERR(s,_) -> (Matita_datatypes_constructors.None)
49 | Matita_freescale_multivm.TickSUSP(s,_) -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s (Matita_freescale_memory_abs.load_from_source_at Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s) Matita_freescale_medium_tests_tools.dTest_zeros (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))))
50 | Matita_freescale_multivm.TickOK(s) -> (Matita_datatypes_constructors.None))
55 (function string -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_pc_reg Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (dTest_HCS08_cSort_status Matita_freescale_memory_abs.MEM_TREE Matita_datatypes_bool.False (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) (Matita_freescale_medium_tests_tools.byte8_strlen string) (Matita_freescale_medium_tests_tools.byte8_list_ordering string)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC))))))))
58 let dTest_HCS08_gNum_source =
59 (function elems -> (let m = Matita_freescale_opcode.HCS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.CLR Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X1))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BRA (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BSR (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XB))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BRA (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XB))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHA) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR2 Matita_freescale_opcode.STA (Matita_freescale_translation.MaDIR2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BHI (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XD))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XD))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.ASL Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHH Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX2 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.INC Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.CPHX (Matita_freescale_translation.MaIMM2(elems))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BCS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.STOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHH Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHH Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX Matita_freescale_opcode.INC Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.RTS Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.LDHX Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.LDHX Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX0ADD Matita_freescale_opcode.JMP Matita_freescale_translation.MaINHX0ADD) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JMP (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XC))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.TST (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHH Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.DIV Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.DIV Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.RTS Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHA) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.LDX (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.CLC Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.ROL (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.ROL (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.ROL (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CMP (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BHI (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XD))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BNE (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CMP (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BHI (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.SUB (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.SBC (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.SEC Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX_and_IMM1 Matita_freescale_opcode.DBNZ (Matita_freescale_translation.MaINHX_and_IMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.ROL Matita_freescale_translation.MaINHA) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.RTS Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.TSX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.RTS Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XE))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.STHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X2))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.RTS Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XC))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM2 Matita_freescale_opcode.JSR (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XB))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PSHA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.STA Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X7))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaIX1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULA Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULH Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.PULX Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.AIS (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHX0ADD Matita_freescale_opcode.JMP Matita_freescale_translation.MaINHX0ADD)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
62 let dTest_HCS08_gNum_status =
63 (function t -> (function i_op -> (function a_op -> (function hX_op -> (function pC_op -> (function addr -> (function elems -> (function data -> (Matita_freescale_status.setweak_i_flag Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_acc_8_low_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_z_flag Matita_freescale_opcode.HCS08 t (Matita_freescale_status.setweak_sp_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.setweak_indX_16_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_status.set_pc_reg Matita_freescale_opcode.HCS08 t (Matita_freescale_model.start_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08GB60)) t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.zero_memory t) (dTest_HCS08_gNum_source elems) addr) data Matita_freescale_medium_tests_tools.dTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08GB60)) t) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False Matita_datatypes_bool.False) pC_op) hX_op) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XF))))) Matita_datatypes_bool.True) a_op) i_op)))))))))
66 let dTest_HCS08_gNum_aurei =
67 (function num -> (Matita_list_list.append
68 (match (Matita_freescale_word16.gt_w16 num (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0))))) with
69 Matita_datatypes_bool.True -> (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_list_list.Nil)))))))))))))))))
70 | Matita_datatypes_bool.False ->
71 (match (Matita_freescale_word16.gt_w16 num (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X0))))) with
72 Matita_datatypes_bool.True -> (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Nil)))))))))))))))))
73 | Matita_datatypes_bool.False ->
74 (match (Matita_freescale_word16.gt_w16 num (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC))))) with
75 Matita_datatypes_bool.True -> (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Nil)))))))))))))))))
76 | Matita_datatypes_bool.False ->
77 (match (Matita_freescale_word16.gt_w16 num (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6))))) with
78 Matita_datatypes_bool.True -> (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Nil)))))))))))))))))
79 | Matita_datatypes_bool.False -> (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Nil))))))))))))))))))
83 (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_list_list.Nil)))))))))))))))))))))))))))))))))))))))))))))))))))
86 let dTest_HCS08_gNum_execute1 =
87 let rec dTest_HCS08_gNum_execute1 =
88 (function m -> (function t -> (function s -> (function n -> (function ntot ->
90 Matita_freescale_multivm.TickERR(s',error) -> (Matita_freescale_multivm.TickERR(s',error))
91 | Matita_freescale_multivm.TickSUSP(s',susp) -> (Matita_freescale_multivm.TickSUSP(s',susp))
92 | Matita_freescale_multivm.TickOK(s') ->
94 Matita_nat_nat.O -> (Matita_freescale_multivm.TickOK(s'))
95 | Matita_nat_nat.S(n') -> (dTest_HCS08_gNum_execute1 m t (Matita_freescale_multivm.execute m t (Matita_freescale_multivm.TickOK(s')) (Matita_nat_plus.plus ntot (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))) n' ntot))
97 ))))) in dTest_HCS08_gNum_execute1
100 let dTest_HCS08_gNum_execute2 =
101 let rec dTest_HCS08_gNum_execute2 =
102 (function m -> (function t -> (function s -> (function n -> (function ntot ->
104 Matita_freescale_multivm.TickERR(s',error) -> (Matita_freescale_multivm.TickERR(s',error))
105 | Matita_freescale_multivm.TickSUSP(s',susp) -> (Matita_freescale_multivm.TickSUSP(s',susp))
106 | Matita_freescale_multivm.TickOK(s') ->
108 Matita_nat_nat.O -> (Matita_freescale_multivm.TickOK(s'))
109 | Matita_nat_nat.S(n') -> (dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (Matita_freescale_multivm.TickOK(s')) (Matita_nat_plus.plus ntot (Matita_nat_nat.S(Matita_nat_nat.O))) ntot) n' ntot))
111 ))))) in dTest_HCS08_gNum_execute2
114 let dTest_HCS08_gNum_execute3 =
115 let rec dTest_HCS08_gNum_execute3 =
116 (function m -> (function t -> (function s -> (function n -> (function ntot ->
118 Matita_freescale_multivm.TickERR(s',error) -> (Matita_freescale_multivm.TickERR(s',error))
119 | Matita_freescale_multivm.TickSUSP(s',susp) -> (Matita_freescale_multivm.TickSUSP(s',susp))
120 | Matita_freescale_multivm.TickOK(s') ->
122 Matita_nat_nat.O -> (Matita_freescale_multivm.TickOK(s'))
123 | Matita_nat_nat.S(n') -> (dTest_HCS08_gNum_execute3 m t (dTest_HCS08_gNum_execute2 m t (Matita_freescale_multivm.TickOK(s')) ntot ntot) n' ntot))
125 ))))) in dTest_HCS08_gNum_execute3
128 let dTest_HCS08_gNum_execute4 =
129 (function m -> (function t -> (function s -> (function ntot ->
131 Matita_freescale_multivm.TickERR(s',error) -> (Matita_freescale_multivm.TickERR(s',error))
132 | Matita_freescale_multivm.TickSUSP(s',susp) -> (Matita_freescale_multivm.TickSUSP(s',susp))
133 | Matita_freescale_multivm.TickOK(s') -> (Matita_freescale_multivm.execute m t (dTest_HCS08_gNum_execute3 m t (Matita_freescale_multivm.TickOK(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)))))))))))))))))))))) ntot) (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.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.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.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.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.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
139 (match (dTest_HCS08_gNum_execute4 Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_multivm.TickOK((dTest_HCS08_gNum_status Matita_freescale_memory_abs.MEM_TREE Matita_datatypes_bool.True (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XE)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XE)))) num Matita_freescale_medium_tests_tools.dTest_zeros))) (Matita_freescale_word16.nat_of_word16 num)) with
140 Matita_freescale_multivm.TickERR(s,_) -> (Matita_datatypes_constructors.None)
141 | Matita_freescale_multivm.TickSUSP(s,_) -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s (Matita_freescale_memory_abs.load_from_source_at Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s) Matita_freescale_medium_tests_tools.dTest_zeros3K (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))))))))
142 | Matita_freescale_multivm.TickOK(s) -> (Matita_datatypes_constructors.None))
147 (function num -> (Matita_datatypes_constructors.Some((dTest_HCS08_gNum_status Matita_freescale_memory_abs.MEM_TREE Matita_datatypes_bool.False (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) num (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X1)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XE)))) num (dTest_HCS08_gNum_aurei num)))))
150 (* CHANGED: COMPUTE RESULTS *)
152 print_string("evaluating sReverseCalc32");;
155 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_32)
160 print_string("evaluating sReverseCalc64");;
163 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_64)
168 print_string("evaluating sReverseCalc128");;
170 let sReverseCalc128 =
171 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_128)
176 print_string("evaluating sReverseCalc256");;
178 let sReverseCalc256 =
179 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_256)
184 print_string("evaluating sReverseCalc512");;
186 let sReverseCalc512 =
187 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_512)
192 print_string("evaluating sReverseCalc1024");;
194 let sReverseCalc1024 =
195 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_1024)
200 print_string("evaluating sReverseCalc2048");;
202 let sReverseCalc2048 =
203 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_2048)
208 print_string("evaluating sReverseCalc3072");;
210 let sReverseCalc3072 =
211 (sReverseCalc Matita_freescale_medium_tests_tools.dTest_random_3072)
216 print_string("evaluating sReverseNoCalc...");;
220 let sReverseNoCalc32 =
221 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_32)
224 let sReverseNoCalc64 =
225 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_64)
228 let sReverseNoCalc128 =
229 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_128)
232 let sReverseNoCalc256 =
233 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_256)
236 let sReverseNoCalc512 =
237 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_512)
240 let sReverseNoCalc1024 =
241 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_1024)
244 let sReverseNoCalc2048 =
245 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_2048)
248 let sReverseNoCalc3072 =
249 (sReverseNoCalc Matita_freescale_medium_tests_tools.dTest_random_3072)
254 print_string("evaluating cSortCalc32");;
257 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_32)
262 print_string("evaluating cSortCalc64");;
265 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_64)
270 print_string("evaluating cSortCalc128");;
273 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_128)
278 print_string("evaluating cSortCalc256");;
281 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_256)
286 print_string("evaluating cSortCalc512");;
289 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_512)
294 print_string("evaluating cSortCalc1024");;
297 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_1024)
302 print_string("evaluating cSortCalc2048");;
305 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_2048)
310 print_string("evaluating cSortCalc3072");;
313 (cSortCalc Matita_freescale_medium_tests_tools.dTest_random_3072)
318 print_string("evaluating cSortNoCalc...");;
323 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_32)
327 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_64)
331 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_128)
335 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_256)
339 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_512)
342 let cSortNoCalc1024 =
343 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_1024)
346 let cSortNoCalc2048 =
347 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_2048)
350 let cSortNoCalc3072 =
351 (cSortNoCalc Matita_freescale_medium_tests_tools.dTest_random_3072)
356 print_string("evaluating gNumCalc1");;
359 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)))))
364 print_string("evaluating gNumCalc2");;
367 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)))))
372 print_string("evaluating gNumCalc5");;
375 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5)))))
380 print_string("evaluating gNumCalc10");;
383 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA)))))
388 print_string("evaluating gNumCalc20");;
391 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4)))))
396 print_string("evaluating gNumCalc50");;
399 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2)))))
404 print_string("evaluating gNumCalc100");;
407 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4)))))
412 print_string("evaluating gNumCalc250");;
415 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XA)))))
420 print_string("evaluating gNumCalc500");;
423 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X4)))))
428 print_string("evaluating gNumCalc1000");;
431 (gNumCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X8)))))
436 print_string("evaluating gNumNoCalc...");;
441 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)))))
445 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)))))
449 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5)))))
453 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA)))))
457 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4)))))
461 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2)))))
465 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4)))))
469 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XA)))))
473 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X4)))))
477 (gNumNoCalc (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X8)))))
480 (* CHANGED: COMPARE RESULTS *)
482 let medium_tests_show_CPU_RAM = Matita_datatypes_bool.True;;
484 if sReverseCalc32 = sReverseNoCalc32
485 then print_string("sReverse32 OK")
486 else print_string("sReverse32 KO");;
488 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
489 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc32 sReverseNoCalc32;;
492 if sReverseCalc64 = sReverseNoCalc64
493 then print_string("sReverse64 OK")
494 else print_string("sReverse64 KO");;
496 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
497 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc64 sReverseNoCalc64;;
500 if sReverseCalc128 = sReverseNoCalc128
501 then print_string("sReverse128 OK")
502 else print_string("sReverse128 KO");;
504 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
505 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc128 sReverseNoCalc128;;
508 if sReverseCalc256 = sReverseNoCalc256
509 then print_string("sReverse256 OK")
510 else print_string("sReverse256 KO");;
512 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
513 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc256 sReverseNoCalc256;;
516 if sReverseCalc512 = sReverseNoCalc512
517 then print_string("sReverse512 OK")
518 else print_string("sReverse512 KO");;
520 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
521 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc512 sReverseNoCalc512;;
524 if sReverseCalc1024 = sReverseNoCalc1024
525 then print_string("sReverse1024 OK")
526 else print_string("sReverse1024 KO");;
528 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
529 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc1024 sReverseNoCalc1024;;
532 if sReverseCalc2048 = sReverseNoCalc2048
533 then print_string("sReverse2048 OK")
534 else print_string("sReverse2048 KO");;
536 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
537 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc2048 sReverseNoCalc2048;;
540 if sReverseCalc3072 = sReverseNoCalc3072
541 then print_string("sReverse3072 OK")
542 else print_string("sReverse3072 KO");;
544 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
545 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE sReverseCalc3072 sReverseNoCalc3072;;
548 if cSortCalc32 = cSortNoCalc32
549 then print_string("cSort32 OK")
550 else print_string("cSort32 KO");;
552 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
553 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc32 cSortNoCalc32;;
556 if cSortCalc64 = cSortNoCalc64
557 then print_string("cSort64 OK")
558 else print_string("cSort64 KO");;
560 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
561 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc64 cSortNoCalc64;;
564 if cSortCalc128 = cSortNoCalc128
565 then print_string("cSort128 OK")
566 else print_string("cSort128 KO");;
568 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
569 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc128 cSortNoCalc128;;
572 if cSortCalc256 = cSortNoCalc256
573 then print_string("cSort256 OK")
574 else print_string("cSort256 KO");;
576 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
577 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc256 cSortNoCalc256;;
580 if cSortCalc512 = cSortNoCalc512
581 then print_string("cSort512 OK")
582 else print_string("cSort512 KO");;
584 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
585 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc512 cSortNoCalc512;;
588 if cSortCalc1024 = cSortNoCalc1024
589 then print_string("cSort1024 OK")
590 else print_string("cSort1024 KO");;
592 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
593 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc1024 cSortNoCalc1024;;
596 if cSortCalc2048 = cSortNoCalc2048
597 then print_string("cSort2048 OK")
598 else print_string("cSort2048 KO");;
600 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
601 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc2048 cSortNoCalc2048;;
604 if cSortCalc3072 = cSortNoCalc3072
605 then print_string("cSort3072 OK")
606 else print_string("cSort3072 KO");;
608 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
609 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE cSortCalc3072 cSortNoCalc3072;;
612 if gNumCalc1 = gNumNoCalc1
613 then print_string("gNum1 OK")
614 else print_string("gNum1 KO");;
616 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
617 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc1 gNumCalc1;;
620 if gNumCalc2 = gNumNoCalc2
621 then print_string("gNum2 OK")
622 else print_string("gNum2 KO");;
624 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
625 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc2 gNumNoCalc2;;
628 if gNumCalc5 = gNumNoCalc5
629 then print_string("gNum5 OK")
630 else print_string("gNum5 KO");;
632 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
633 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc5 gNumNoCalc5;;
636 if gNumCalc10 = gNumNoCalc10
637 then print_string("gNum10 OK")
638 else print_string("gNum10 KO");;
640 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
641 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc10 gNumNoCalc10;;
644 if gNumCalc20 = gNumNoCalc20
645 then print_string("gNum20 OK")
646 else print_string("gNum20 KO");;
648 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
649 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc20 gNumNoCalc20;;
652 if gNumCalc50 = gNumNoCalc50
653 then print_string("gNum50 OK")
654 else print_string("gNum50 KO");;
656 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
657 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc50 gNumNoCalc50;;
660 if gNumCalc100 = gNumNoCalc100
661 then print_string("gNum100 OK")
662 else print_string("gNum100 KO");;
664 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
665 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc100 gNumNoCalc100;;
668 if gNumCalc250 = gNumNoCalc250
669 then print_string("gNum250 OK")
670 else print_string("gNum250 KO");;
672 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
673 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc250 gNumNoCalc250;;
676 if gNumCalc500 = gNumNoCalc500
677 then print_string("gNum500 OK")
678 else print_string("gNum500 KO");;
680 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
681 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc500 gNumNoCalc500;;
684 if gNumCalc1000 = gNumNoCalc1000
685 then print_string("gNum1000 OK")
686 else print_string("gNum1000 KO");;
688 if (medium_tests_show_CPU_RAM = Matita_datatypes_bool.True)
689 then Matita_freescale_debug.compare_CPU_RAM Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE gNumCalc1000 gNumNoCalc1000;;