(test_not_impl_byte b RS08_not_impl_byte ⊙ eq_w16 (get_byte_count RS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
(⊖ (test_not_impl_byte b RS08_not_impl_byte) ⊙ eq_w16 (get_byte_count RS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x0〉〉))
= true.
napply refl_eq.
(test_not_impl_byte b RS08_not_impl_byte ⊙ eq_w16 (get_byte_count RS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
(⊖ (test_not_impl_byte b RS08_not_impl_byte) ⊙ eq_w16 (get_byte_count RS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x0〉〉))
= true.
napply refl_eq.