include "freescale/table_HC08.ma".
-(* CORRETTEZZA *)
-
(* HC08: opcode non implementati come da manuale (byte) *)
definition HC08_not_impl_byte ≝
[〈x3,x2〉;〈x3,xE〉
leb (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.
reflexivity.
qed.
-