(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
(* dimostrazione senza svolgimento degli stati, immediata *)
nlemma ok_mTest_HCS08_ADC_full :
∀t:memory_impl.
- execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) 28 =
+ execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) nat28 =
(* NB: V,N,Z sono tornati false C e' tornato true *)
TickOK ? (set_pc_reg HCS08 t (* nuovo PC *)
(set_acc_8_low_reg HCS08 t (mTest_HCS08_ADC_status t) 〈x1,x6〉) (* nuovo A *)
napply refl_eq.
nqed.
+(* -------------------------------------
+
(* ********* *)
(* HCS08 MOV *)
(* ********* *)
reflexivity.
qed.
*)
+*)