tagged 0.5.0-rc1

[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_micro_tests.ml

let mTest_bytes =
(Matita_list_list.append (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.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X5)),(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.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XB)),(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.X1,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X4,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (Matita_list_list.append (Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X0)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XE,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))) (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.XF,Matita_freescale_exadecim.X1)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X2)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X3)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X4)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X5)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X6)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X7)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X8)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.X9)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XA)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XB)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XC)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XD)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XE)),(Matita_list_list.Cons((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_list_list.Nil))))))))))))))))))))))))))))))))))))))))))))))))
;;

let mTest_HC05_RAM =
(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.X8,Matita_freescale_exadecim.X0))))
;;

let mTest_HC05_prog =
(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.X0,Matita_freescale_exadecim.X0))))
;;

let mTest_HC05_data =
(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))))
;;

let mTest_HC08_RAM =
(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.X5,Matita_freescale_exadecim.X0))))
;;

let mTest_HC08_prog =
(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XB,Matita_freescale_exadecim.XE)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))
;;

let mTest_HC08_data =
(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XD)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))
;;

let mTest_HCS08_RAM =
(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.X7,Matita_freescale_exadecim.X0))))
;;

let mTest_HCS08_prog =
(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.X6,Matita_freescale_exadecim.X0))))
;;

let mTest_HCS08_data =
(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))
;;

let mTest_RS08_RAM =
(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.X2,Matita_freescale_exadecim.X0))))
;;

let mTest_RS08_prog =
(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X8)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))
;;

let mTest_RS08_data =
(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))
;;

let mTest_HCS08_ADC_source =
(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.ADC (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XA,Matita_freescale_exadecim.XA))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaDIR1((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_DIR2 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaDIR2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(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_IX2 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaIX2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,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.X2,Matita_freescale_exadecim.X4))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0 Matita_freescale_opcode.ADC Matita_freescale_translation.MaIX0) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP2 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaSP2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X1))))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1 Matita_freescale_opcode.ADC (Matita_freescale_translation.MaSP1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X4))))))))))))))
;;

let mTest_HCS08_ADC_status =
(function t -> (Matita_freescale_status.set_c_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.MC9S08AW60)) t (Matita_freescale_memory_abs.load_from_source_at 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) mTest_HCS08_ADC_source mTest_HCS08_prog) mTest_bytes mTest_HCS08_RAM) mTest_bytes mTest_HCS08_data) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) 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) mTest_HCS08_prog) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X0))))) (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.X1,Matita_freescale_exadecim.X0))))) Matita_datatypes_bool.True))
;;

let mTest_HCS08_MOV_source =
(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_to_DIR1 Matita_freescale_opcode.MOV (Matita_freescale_translation.MaIMM1_to_DIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XA)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1_to_DIR1 Matita_freescale_opcode.MOV (Matita_freescale_translation.MaDIR1_to_DIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0p_to_DIR1 Matita_freescale_opcode.MOV (Matita_freescale_translation.MaIX0p_to_DIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X2))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1_to_IX0p Matita_freescale_opcode.MOV (Matita_freescale_translation.MaDIR1_to_IX0p((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X2))))))))))
;;

let mTest_HCS08_MOV_status =
(function t -> (function b1 -> (function b2 -> (function b3 -> (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.MC9S08AW60)) 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) mTest_HCS08_MOV_source mTest_HCS08_prog) (Matita_list_list.Cons(b1,(Matita_list_list.Cons(b2,(Matita_list_list.Cons(b3,(Matita_list_list.Nil))))))) mTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) 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) mTest_HCS08_prog) (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.X7,Matita_freescale_exadecim.X1)))))))))
;;

let mTest_HCS08_ROL_ROR_source =
(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_IMM2 Matita_freescale_opcode.LDHX (Matita_freescale_translation.MaIMM2((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X2)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.X4))))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X5,Matita_freescale_exadecim.X6))))) (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_INHX Matita_freescale_opcode.ROL Matita_freescale_translation.MaINHX) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA Matita_freescale_opcode.ROR Matita_freescale_translation.MaINHA) (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_INHA Matita_freescale_opcode.CLR 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_freescale_translation.compile m Matita_freescale_opcode.MODE_INHH Matita_freescale_opcode.CLR Matita_freescale_translation.MaINHH)))))))))))
;;

let mTest_HCS08_ROL_ROR_status =
(function t -> (Matita_freescale_status.set_z_flag 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.MC9S08AW60)) t (Matita_freescale_memory_abs.load_from_source_at t (Matita_freescale_memory_abs.zero_memory t) mTest_HCS08_ROL_ROR_source mTest_HCS08_prog) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) 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) mTest_HCS08_prog) (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_datatypes_bool.True))
;;

let mTest_HCS08_CBEQ_DBNZ_source =
(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_DIR1_and_IMM1 Matita_freescale_opcode.CBEQA (Matita_freescale_translation.MaDIR1_and_IMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,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_INH Matita_freescale_opcode.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1_and_IMM1 Matita_freescale_opcode.CBEQA (Matita_freescale_translation.MaIMM1_and_IMM1((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))))) (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_IMM1_and_IMM1 Matita_freescale_opcode.CBEQX (Matita_freescale_translation.MaIMM1_and_IMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.XF)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX1p_and_IMM1 Matita_freescale_opcode.CBEQA (Matita_freescale_translation.MaIX1p_and_IMM1((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_INH Matita_freescale_opcode.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0p_and_IMM1 Matita_freescale_opcode.CBEQA (Matita_freescale_translation.MaIX0p_and_IMM1((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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1_and_IMM1 Matita_freescale_opcode.CBEQA (Matita_freescale_translation.MaSP1_and_IMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1_and_IMM1 Matita_freescale_opcode.DBNZ (Matita_freescale_translation.MaDIR1_and_IMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X2)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INHA_and_IMM1 Matita_freescale_opcode.DBNZ (Matita_freescale_translation.MaINHA_and_IMM1((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.NOP 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.X0,Matita_freescale_exadecim.X1))))) (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_IX1_and_IMM1 Matita_freescale_opcode.DBNZ (Matita_freescale_translation.MaIX1_and_IMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IX0_and_IMM1 Matita_freescale_opcode.DBNZ (Matita_freescale_translation.MaIX0_and_IMM1((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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_SP1_and_IMM1 Matita_freescale_opcode.DBNZ (Matita_freescale_translation.MaSP1_and_IMM1((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_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.NOP Matita_freescale_translation.MaINH))))))))))))))))))))))))))
;;

let mTest_HCS08_CBEQ_DBNZ_status =
(function t -> (function b1 -> (function b2 -> (function b3 -> (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.MC9S08AW60)) t (Matita_freescale_memory_abs.load_from_source_at 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) mTest_HCS08_CBEQ_DBNZ_source mTest_HCS08_prog) mTest_bytes mTest_HCS08_RAM) (Matita_list_list.Cons(b1,(Matita_list_list.Cons(b2,(Matita_list_list.Cons(b3,(Matita_list_list.Nil))))))) mTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) 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) mTest_HCS08_prog) (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.XF))))) (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.XF)))))))))
;;

let mTest_HCS08_BSETn_BCLRn_source =
(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_DIRn(Matita_freescale_aux_bases.O0)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O0,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O1)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O1,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O2)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O2,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O3)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O3,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O4)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O4,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O5)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O5,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O6)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O6,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O7)) Matita_freescale_opcode.BSETn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O7,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O0)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O0,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O1)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O1,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O2)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O2,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O3)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O3,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O4)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O4,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O5)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O5,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O6)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O6,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))) (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn(Matita_freescale_aux_bases.O7)) Matita_freescale_opcode.BCLRn (Matita_freescale_translation.MaDIRn(Matita_freescale_aux_bases.O7,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0))))))))))))))))))))))
;;

let mTest_HCS08_BSETn_BCLRn_status =
(function t -> (function b1 -> (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.MC9S08AW60)) 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) mTest_HCS08_BSETn_BCLRn_source mTest_HCS08_prog) (Matita_list_list.Cons(b1,(Matita_list_list.Nil))) mTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) 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) mTest_HCS08_prog)))
;;

let mTest_HCS08_BRSETn_BRCLRn_source =
(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_DIRn_and_IMM1(Matita_freescale_aux_bases.O0)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O0,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O1)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O1,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O2)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O2,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O3)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O3,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O4)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O4,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O5)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O5,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O6)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O6,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O7)) Matita_freescale_opcode.BRSETn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O7,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O0)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O0,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O1)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O1,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O2)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O2,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O3)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O3,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O4)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O4,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O5)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O5,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O6)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O6,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_DIRn_and_IMM1(Matita_freescale_aux_bases.O7)) Matita_freescale_opcode.BRCLRn (Matita_freescale_translation.MaDIRn_and_IMM1(Matita_freescale_aux_bases.O7,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X5)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.NOP Matita_freescale_translation.MaINH))))))))))))))))))))))))))))))))))
;;

let mTest_HCS08_BRSETn_BRCLRn_status =
(function 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.MC9S08AW60)) 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) mTest_HCS08_BRSETn_BRCLRn_source mTest_HCS08_prog) mTest_bytes mTest_HCS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) 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) mTest_HCS08_prog))
;;

let mTest_RS08_TNY_source =
(let m = Matita_freescale_opcode.RS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_TNY(Matita_freescale_exadecim.XD)) Matita_freescale_opcode.ADD (Matita_freescale_translation.MaTNY(Matita_freescale_exadecim.XD))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_TNY(Matita_freescale_exadecim.XE)) Matita_freescale_opcode.ADD (Matita_freescale_translation.MaTNY(Matita_freescale_exadecim.XE))) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_TNY(Matita_freescale_exadecim.XF)) Matita_freescale_opcode.ADD (Matita_freescale_translation.MaTNY(Matita_freescale_exadecim.XF))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XF))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XE)))))))))))
;;

let mTest_RS08_TNY_status =
(function t -> (Matita_freescale_status.setweak_x_map Matita_freescale_opcode.RS08 t (Matita_freescale_status.setweak_ps_map Matita_freescale_opcode.RS08 t (Matita_freescale_status.set_pc_reg Matita_freescale_opcode.RS08 t (Matita_freescale_model.start_of_mcu_version (Matita_freescale_model.FamilyRS08(Matita_freescale_model.MC9RS08KA2)) 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) mTest_RS08_TNY_source mTest_RS08_prog) mTest_bytes (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))))) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyRS08(Matita_freescale_model.MC9RS08KA2)) 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) mTest_RS08_prog) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))))
;;

let mTest_RS08_SRT_source =
(let m = Matita_freescale_opcode.RS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_SRT(Matita_freescale_aux_bases.T1F)) Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSRT(Matita_freescale_aux_bases.T1F))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.SUB (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_IMM1 Matita_freescale_opcode.BEQ (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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m (Matita_freescale_opcode.MODE_SRT(Matita_freescale_aux_bases.T0E)) Matita_freescale_opcode.LDA (Matita_freescale_translation.MaSRT(Matita_freescale_aux_bases.T0E))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.SUB (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_IMM1 Matita_freescale_opcode.BEQ (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.NOP Matita_freescale_translation.MaINH) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.SUB (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BEQ (Matita_freescale_translation.MaIMM1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))))) (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_INH Matita_freescale_opcode.NOP Matita_freescale_translation.MaINH))))))))))))))
;;

let mTest_RS08_SRT_status =
(function t -> (Matita_freescale_status.setweak_x_map Matita_freescale_opcode.RS08 t (Matita_freescale_status.setweak_ps_map Matita_freescale_opcode.RS08 t (Matita_freescale_status.set_z_flag Matita_freescale_opcode.RS08 t (Matita_freescale_status.set_pc_reg Matita_freescale_opcode.RS08 t (Matita_freescale_model.start_of_mcu_version (Matita_freescale_model.FamilyRS08(Matita_freescale_model.MC9RS08KA2)) 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) mTest_RS08_SRT_source mTest_RS08_prog) mTest_bytes mTest_RS08_data) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyRS08(Matita_freescale_model.MC9RS08KA2)) 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) mTest_RS08_prog) Matita_datatypes_bool.True) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XE))) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))
;;

let mTest_RS08_mult_source =
(let m = Matita_freescale_opcode.RS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.CLR (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BEQ (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_DIR1 Matita_freescale_opcode.LDA (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.DEC (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X1))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.ADD (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X0))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1 Matita_freescale_opcode.BCC (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_DIR1 Matita_freescale_opcode.INC (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X2))))) (Matita_list_list.append (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_DIR1 Matita_freescale_opcode.STA (Matita_freescale_translation.MaDIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X2,Matita_freescale_exadecim.X3))))) (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.XE,Matita_freescale_exadecim.XE)))))))))))))))))
;;

let mTest_RS08_mult_status =
(function t -> (function b1 -> (function b2 -> (function b3 -> (function b4 -> (Matita_freescale_status.set_z_flag Matita_freescale_opcode.RS08 t (Matita_freescale_status.set_pc_reg Matita_freescale_opcode.RS08 t (Matita_freescale_model.start_of_mcu_version (Matita_freescale_model.FamilyRS08(Matita_freescale_model.MC9RS08KA2)) 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) mTest_RS08_mult_source mTest_RS08_prog) (Matita_list_list.Cons(b1,(Matita_list_list.Cons(b2,(Matita_list_list.Cons(b3,(Matita_list_list.Cons(b4,(Matita_list_list.Nil))))))))) mTest_RS08_RAM) (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyRS08(Matita_freescale_model.MC9RS08KA2)) 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) mTest_RS08_prog) Matita_datatypes_bool.True))))))
;;

let mTest_bits_source =
(let m = Matita_freescale_opcode.HCS08 in (Matita_freescale_translation.source_to_byte8 m (Matita_freescale_translation.compile m Matita_freescale_opcode.MODE_IMM1_to_DIR1 Matita_freescale_opcode.MOV (Matita_freescale_translation.MaIMM1_to_DIR1((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X7,Matita_freescale_exadecim.X0)))))))
;;

let mTest_bits_status =
(function t -> (function sub -> (function b -> (Matita_freescale_status.setweak_n_flag 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.MC9S08AW60)) 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) mTest_bits_source mTest_HCS08_prog) (Matita_list_list.Cons(b,(Matita_list_list.Nil))) mTest_HCS08_RAM) (Matita_freescale_memory_abs.check_update_bit t (Matita_freescale_model.build_memory_type_of_mcu_version (Matita_freescale_model.FamilyHCS08(Matita_freescale_model.MC9S08AW60)) t) mTest_HCS08_RAM sub Matita_freescale_memory_struct.MEM_READ_ONLY) (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) mTest_HCS08_prog) Matita_datatypes_bool.True))))
;;