freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma
index 60a40cb73b72562856ea1455ec32c01afe727ac4..c7b9c15491cabcdbcb3491f7c64e8a564bde6970 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma
@@ -73,8 +73,8 @@ ndefinition HCS08_not_impl_word ≝
 
 (* test bytecode non implementati *)
 nlemma ok_word_table_HCS08 : forall_b8 (λb.
- (test_not_impl_byte b HCS08_not_impl_word     ⊙ eq_w16 (get_word_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
- (⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
+ (test_not_impl_byte b HCS08_not_impl_word     ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
+ (⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
  = true.
  napply refl_eq.
 nqed.