-nlemma ok_word_table_HC08 : forall_b8 (λb.
- (test_not_impl_byte b HC08_not_impl_word ⊙ eq_w16 (get_word_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
- (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eq_w16 (get_word_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉))
+(* !!! per brevita... *)
+(*nlemma ok_word_table_HC08 : forall_b8 (λb.
+ (test_not_impl_byte b HC08_not_impl_word ⊙ eq_w16 (get_word_count HC08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
+ (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eq_w16 (get_word_count HC08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉))