nqed.
nlemma ok_OpIm_table_HC08 :
forall_instr_mode (λi:instr_mode.
forall_opcode (λop:opcode.
le_nat (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.
nqed.
nlemma ok_OpIm_table_HC08 :
forall_instr_mode (λi:instr_mode.
forall_opcode (λop:opcode.
le_nat (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.