freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / opcodes / HC08_table_tests.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma
index aa792b55ea20a46bf5743d601bca05410078ac80..06b4d26571ac3ad042020841279684bc4594d26b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma
@@ -78,8 +78,8 @@ ndefinition HC08_not_impl_word ≝
 
 (* test bytecode non implementati *)
 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〉〉))
+ (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〉〉))
  = true.
  napply refl_eq.
 nqed.