-nlemma ok_pseudo_table_RS08 : forall_opcode (λo.
- (test_not_impl_pseudo o RS08_not_impl_pseudo ⊙ le_nat 1 (get_pseudo_count RS08 o 0 opcode_table_RS08)) ⊗
- (⊖ (test_not_impl_pseudo o RS08_not_impl_pseudo) ⊙ eq_nat (get_pseudo_count RS08 o 0 opcode_table_RS08) 0))
+nlemma ok_pseudo_table_RS08 : forall_op (λo.
+ (test_not_impl_pseudo o RS08_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count RS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08)) ⊗
+ (⊖ (test_not_impl_pseudo o RS08_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count RS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x0〉〉))