+ ]
+in get_word_count.
+
+(* su tutta la lista quante volte compare lo pseudocodice *)
+definition get_pseudo_count := \lambda m:mcu_type.
+let rec get_pseudo_count (o:opcode) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match fst4T ???? hd with
+ [ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with
+ [ true ⇒ get_pseudo_count o (S c) tl
+ | false ⇒ get_pseudo_count o c tl
+ ]
+ ]
+ ]
+in get_pseudo_count.
+
+(* su tutta la lista quante volte compare la modalita' *)
+definition get_mode_count := \lambda m:mcu_type.
+let rec get_mode_count (i:instr_mode) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match eqim (snd4T ???? hd) i with
+ [ true ⇒ get_mode_count i (S c) tl
+ | false ⇒ get_mode_count i c tl
+ ]
+ ]
+ in get_mode_count.