(* dimostrazione senza svolgimento degli stati, immediata *)
nlemma ok_mTest_HCS08_ADC_full :
∀t:memory_impl.
(* dimostrazione senza svolgimento degli stati, immediata *)
nlemma ok_mTest_HCS08_ADC_full :
∀t:memory_impl.
(* 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 *)
(* 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 *)