X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_medium_tests_lemmas.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_medium_tests_lemmas.ml;h=c57b3213524df33b5a62ef58aaa70d434453b50c;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_medium_tests_lemmas.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_medium_tests_lemmas.ml
new file mode 100644
index 000000000..c57b32135
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_medium_tests_lemmas.ml
@@ -0,0 +1,4 @@
+let execute_HCS08_STHX_maSP1_aux =
+(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))))))))))))
+;;
+