(* descrittore del click = stato di avanzamento dell'esecuzione *)
(* 1) None = istruzione eseguita, attesa del fetch *)
(* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *)
-ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_op_type m) (aux_im_type m) byte8 word16.
+ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
(* tipo processore dipendente dalla mcu, varia solo la ALU *)
nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
(forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
].
-ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_op m) (eq_im m) eq_b8 eq_w16).
+ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_pseudo m) (eq_im m) eq_b8 eq_w16).
(* generalizzazione del confronto fra stati *)
ndefinition eq_anystatus ≝