-nlemma ok_pseudo_table_HCS08 : forall_opcode (λo.
- (test_not_impl_pseudo o HCS08_not_impl_pseudo ⊙ le_nat 1 (get_pseudo_count HCS08 o 0 opcode_table_HCS08)) ⊗
- (⊖ (test_not_impl_pseudo o HCS08_not_impl_pseudo) ⊙ eq_nat (get_pseudo_count HCS08 o 0 opcode_table_HCS08) 0))
+nlemma ok_pseudo_table_HCS08 : forall_op (λo.
+ (test_not_impl_pseudo o HCS08_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) ⊗
+ (⊖ (test_not_impl_pseudo o HCS08_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))