include "freescale/table_HCS08.ma".
-(* CORRETTEZZA *)
-
(* HCS08: opcode non implementati come da manuale (byte) *)
definition HCS08_not_impl_byte ≝
[〈x8,xD〉
reflexivity.
qed.
+(*
lemma ok_OpIm_table_HCS08 :
forall_instr_mode (λi:instr_mode.
forall_opcode (λop:opcode.
leb (get_OpIm_count HCS08 (anyOP HCS08 op) i 0 opcode_table_HCS08) 1)) = true.
reflexivity.
qed.
-
+*)