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

   1 let execute_HCS08_STHX_maSP1_aux =
   2 (function s -> (function blow -> (Matita_freescale_multivm.TickOK((Matita_freescale_status.set_pc_reg Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.setweak_v_flag Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.setweak_n_flag Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.set_z_flag Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE (Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s (Obj.magic(Matita_freescale_memory_trees.mt_update (Matita_freescale_memory_trees.mt_update (Obj.magic(Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s)) (Matita_freescale_word16.plus_w16nc (Matita_freescale_status.sp_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),blow))) (Matita_freescale_status.indX_high_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s)))) (Matita_freescale_word16.succ_w16 (Matita_freescale_word16.plus_w16nc (Matita_freescale_status.sp_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),blow)))) (Matita_freescale_status.indX_low_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s)))))) (Matita_freescale_word16.eq_w16 (Matita_freescale_word16.Mk_word16((Matita_freescale_status.indX_high_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s))),(Matita_freescale_status.indX_low_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s))))) (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_freescale_byte8.mSB_b8 (Matita_freescale_status.indX_high_reg_HC08 (Obj.magic(Matita_freescale_status.alu Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s))))) Matita_datatypes_bool.False) (Matita_freescale_load_write.filtered_plus_w16 Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s (Matita_freescale_status.get_pc_reg Matita_freescale_opcode.HCS08 Matita_freescale_memory_abs.MEM_TREE s) (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))
   3 ;;
   4