From f9b16ad62794042c2b31c6e3433b3c4035f8a0d5 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Wed, 12 Aug 2009 22:54:21 +0000 Subject: [PATCH] freescale porting, work in progress --- .../matita/contribs/ng_assembly/depends | 14 +- .../contribs/ng_assembly/universe/ascii.ma | 105 +++++ .../ng_assembly/universe/bitrigesim.ma | 69 +++ .../contribs/ng_assembly/universe/exadecim.ma | 52 +++ .../contribs/ng_assembly/universe/oct.ma | 44 ++ .../contribs/ng_assembly/universe/opcode.ma | 136 ++++++ .../contribs/ng_assembly/universe/quatern.ma | 40 ++ .../meta_type.ma => universe/universe.ma} | 399 ++++++++---------- 8 files changed, 640 insertions(+), 219 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/universe/ascii.ma create mode 100755 helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma create mode 100755 helm/software/matita/contribs/ng_assembly/universe/exadecim.ma create mode 100755 helm/software/matita/contribs/ng_assembly/universe/oct.ma create mode 100755 helm/software/matita/contribs/ng_assembly/universe/opcode.ma create mode 100755 helm/software/matita/contribs/ng_assembly/universe/quatern.ma rename helm/software/matita/contribs/ng_assembly/{common/meta_type.ma => universe/universe.ma} (67%) diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 311889200..26c8f7e8d 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -7,10 +7,10 @@ freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma freescale/multivm.ma freescale/load_write.ma common/nat_to_num.ma common/nat.ma num/word32.ma +common/nat.ma num/bool.ma freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma freescale_tests/medium_tests_tools.ma freescale/multivm.ma common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma common/string.ma -common/nat.ma num/bool.ma compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma num/quatern.ma num/bool.ma freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma @@ -19,27 +19,31 @@ num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma num/byte8.ma num/bitrigesim.ma num/exadecim.ma freescale/memory_func.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma freescale/load_write.ma freescale/model.ma freescale/translation.ma -freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma +freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma +universe/quatern.ma universe/universe.ma +universe/ascii.ma universe/universe.ma freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma freescale/translation_lemmas.ma freescale/translation.ma num/byte8_lemmas.ma -common/meta_type.ma common/string_lemmas.ma freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma test_errori.ma common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma +universe/bitrigesim.ma universe/universe.ma freescale/memory_struct.ma num/byte8.ma num/oct.ma freescale/model.ma freescale/status.ma freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma +universe/exadecim.ma universe/universe.ma common/string.ma common/ascii.ma common/list_utility.ma common/theory.ma compiler/ast_type.ma common/list_utility.ma +common/prod.ma num/bool.ma num/word16.ma num/byte8.ma freescale/memory_trees.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma -common/prod.ma num/bool.ma num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma +universe/oct.ma universe/universe.ma num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma freescale_tests/medium_tests.ma common/list_utility.ma common/nat_to_num.ma freescale_tests/medium_tests_tools.ma freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base_lemmas_opcode.ma num/word16_lemmas.ma @@ -53,6 +57,7 @@ num/word32.ma num/word16.ma freescale/opcode_base.ma num/word16.ma freescale/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/status.ma num/word16_lemmas.ma num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +universe/opcode.ma universe/universe.ma freescale/table_HC08_tests.ma freescale/opcode.ma freescale/table_HC08.ma common/option_lemmas.ma common/option.ma num/bool_lemmas.ma common/option.ma num/bool.ma @@ -60,6 +65,7 @@ num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma freescale/opcode_base_lemmas_opcode.ma freescale/opcode_base.ma num/bool_lemmas.ma common/list_lemmas.ma common/list.ma common/sigma.ma +universe/universe.ma common/list.ma num/bool_lemmas.ma num/bitrigesim.ma num/bool.ma common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base.ma num/bitrigesim_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma diff --git a/helm/software/matita/contribs/ng_assembly/universe/ascii.ma b/helm/software/matita/contribs/ng_assembly/universe/ascii.ma new file mode 100755 index 000000000..a16343588 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/ascii.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "universe/universe.ma". + +ndefinition ASCII_UN ≝ [ uch_0; uch_1; uch_2; uch_3; uch_4; uch_5; uch_6; uch_7; uch_8; uch_9; + uch__; uch_A; uch_B; uch_C; uch_D; uch_E; uch_F; uch_G; uch_H; uch_I; + uch_J; uch_K; uch_L; uch_M; uch_N; uch_O; uch_P; uch_Q; uch_R; uch_S; + uch_T; uch_U; uch_V; uch_W; uch_X; uch_Y; uch_Z; uch_a; uch_b; uch_c; + uch_d; uch_e; uch_f; uch_g; uch_h; uch_i; uch_j; uch_k; uch_l; uch_m; + uch_n; uch_o; uch_p; uch_q; uch_r; uch_s; uch_t; uch_u; uch_v; uch_w; + uch_x; uch_y; uch_z ]. + +(* derivati dall'universo + 1) SUN_destruct ASCII_UN + 2) eq_to_eqSUN ASCII_UN + 3) neq_to_neqSUN ASCII_UN + 4) eqSUN_to_eq ASCII_UN + 5) neqSUN_to_neq ASCII_UN + 6) decidable_SUN ASCII_UN + 7) symmetric_eqSUN ASCII_UN +*) + +nlemma un_ch_0 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_0 (refl_eq …) ?); #y; nelim y; ##[ ##61: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_1 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_1 (refl_eq …) ?); #y; nelim y; ##[ ##62: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_2 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_2 (refl_eq …) ?); #y; nelim y; ##[ ##63: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_3 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_3 (refl_eq …) ?); #y; nelim y; ##[ ##64: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_4 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_4 (refl_eq …) ?); #y; nelim y; ##[ ##65: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_5 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_5 (refl_eq …) ?); #y; nelim y; ##[ ##66: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_6 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_6 (refl_eq …) ?); #y; nelim y; ##[ ##67: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_7 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_7 (refl_eq …) ?); #y; nelim y; ##[ ##68: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_8 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_8 (refl_eq …) ?); #y; nelim y; ##[ ##69: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_9 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_9 (refl_eq …) ?); #y; nelim y; ##[ ##70: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch__ : S_UN ASCII_UN. napply (S_EL ASCII_UN uch__ (refl_eq …) ?); #y; nelim y; ##[ ##71: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_A : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_A (refl_eq …) ?); #y; nelim y; ##[ ##72: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_B : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_B (refl_eq …) ?); #y; nelim y; ##[ ##73: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_C : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_C (refl_eq …) ?); #y; nelim y; ##[ ##74: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_D : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_D (refl_eq …) ?); #y; nelim y; ##[ ##75: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_E : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_E (refl_eq …) ?); #y; nelim y; ##[ ##76: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_F : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_F (refl_eq …) ?); #y; nelim y; ##[ ##77: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_G : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_G (refl_eq …) ?); #y; nelim y; ##[ ##78: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_H : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_H (refl_eq …) ?); #y; nelim y; ##[ ##79: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_I : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_I (refl_eq …) ?); #y; nelim y; ##[ ##80: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_J : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_J (refl_eq …) ?); #y; nelim y; ##[ ##81: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_K : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_K (refl_eq …) ?); #y; nelim y; ##[ ##82: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_L : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_L (refl_eq …) ?); #y; nelim y; ##[ ##83: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_M : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_M (refl_eq …) ?); #y; nelim y; ##[ ##84: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_N : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_N (refl_eq …) ?); #y; nelim y; ##[ ##85: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_O : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_O (refl_eq …) ?); #y; nelim y; ##[ ##86: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_P : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_P (refl_eq …) ?); #y; nelim y; ##[ ##87: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_Q : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_Q (refl_eq …) ?); #y; nelim y; ##[ ##88: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_R : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_R (refl_eq …) ?); #y; nelim y; ##[ ##89: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_S : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_S (refl_eq …) ?); #y; nelim y; ##[ ##90: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_T : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_T (refl_eq …) ?); #y; nelim y; ##[ ##91: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_U : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_U (refl_eq …) ?); #y; nelim y; ##[ ##92: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_V : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_V (refl_eq …) ?); #y; nelim y; ##[ ##93: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_W : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_W (refl_eq …) ?); #y; nelim y; ##[ ##94: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_X : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_X (refl_eq …) ?); #y; nelim y; ##[ ##95: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_Y : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_Y (refl_eq …) ?); #y; nelim y; ##[ ##96: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_Z : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_Z (refl_eq …) ?); #y; nelim y; ##[ ##97: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_a : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_a (refl_eq …) ?); #y; nelim y; ##[ ##98: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_b : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_b (refl_eq …) ?); #y; nelim y; ##[ ##99: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_c : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_c (refl_eq …) ?); #y; nelim y; ##[ ##100: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_d : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_d (refl_eq …) ?); #y; nelim y; ##[ ##101: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_e : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_e (refl_eq …) ?); #y; nelim y; ##[ ##102: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_f : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_f (refl_eq …) ?); #y; nelim y; ##[ ##103: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_g : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_g (refl_eq …) ?); #y; nelim y; ##[ ##104: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_h : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_h (refl_eq …) ?); #y; nelim y; ##[ ##105: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_i : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_i (refl_eq …) ?); #y; nelim y; ##[ ##106: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_j : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_j (refl_eq …) ?); #y; nelim y; ##[ ##107: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_k : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_k (refl_eq …) ?); #y; nelim y; ##[ ##108: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_l : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_l (refl_eq …) ?); #y; nelim y; ##[ ##109: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_m : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_m (refl_eq …) ?); #y; nelim y; ##[ ##110: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_n : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_n (refl_eq …) ?); #y; nelim y; ##[ ##111: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_o : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_o (refl_eq …) ?); #y; nelim y; ##[ ##112: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_p : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_p (refl_eq …) ?); #y; nelim y; ##[ ##113: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_q : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_q (refl_eq …) ?); #y; nelim y; ##[ ##114: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_r : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_r (refl_eq …) ?); #y; nelim y; ##[ ##115: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_s : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_s (refl_eq …) ?); #y; nelim y; ##[ ##116: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_t : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_t (refl_eq …) ?); #y; nelim y; ##[ ##117: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_u : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_u (refl_eq …) ?); #y; nelim y; ##[ ##118: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_v : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_v (refl_eq …) ?); #y; nelim y; ##[ ##119: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_w : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_w (refl_eq …) ?); #y; nelim y; ##[ ##120: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_x : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_x (refl_eq …) ?); #y; nelim y; ##[ ##121: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_y : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_y (refl_eq …) ?); #y; nelim y; ##[ ##122: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ch_z : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_z (refl_eq …) ?); #y; nelim y; ##[ ##123: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma new file mode 100755 index 000000000..bbed39718 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "universe/universe.ma". + +ndefinition BIT_UN ≝ [ ut00; ut01; ut02; ut03; ut04; ut05; ut06; ut07; ut08; ut09; ut0A; ut0B; ut0C; ut0D; ut0E; ut0F; + ut10; ut11; ut12; ut13; ut14; ut15; ut16; ut17; ut18; ut19; ut1A; ut1B; ut1C; ut1D; ut1E; ut1F ]. + +(* derivati dall'universo + 1) SUN_destruct BIT_UN + 2) eq_to_eqSUN BIT_UN + 3) neq_to_neqSUN BIT_UN + 4) eqSUN_to_eq BIT_UN + 5) neqSUN_to_neq BIT_UN + 6) decidable_SUN BIT_UN + 7) symmetric_eqSUN BIT_UN +*) + +nlemma un_t00 : S_UN BIT_UN. napply (S_EL BIT_UN ut00 (refl_eq …) ?); #y; nelim y; ##[ ##29: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t01 : S_UN BIT_UN. napply (S_EL BIT_UN ut01 (refl_eq …) ?); #y; nelim y; ##[ ##30: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t02 : S_UN BIT_UN. napply (S_EL BIT_UN ut02 (refl_eq …) ?); #y; nelim y; ##[ ##31: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t03 : S_UN BIT_UN. napply (S_EL BIT_UN ut03 (refl_eq …) ?); #y; nelim y; ##[ ##32: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t04 : S_UN BIT_UN. napply (S_EL BIT_UN ut04 (refl_eq …) ?); #y; nelim y; ##[ ##33: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t05 : S_UN BIT_UN. napply (S_EL BIT_UN ut05 (refl_eq …) ?); #y; nelim y; ##[ ##34: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t06 : S_UN BIT_UN. napply (S_EL BIT_UN ut06 (refl_eq …) ?); #y; nelim y; ##[ ##35: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t07 : S_UN BIT_UN. napply (S_EL BIT_UN ut07 (refl_eq …) ?); #y; nelim y; ##[ ##36: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t08 : S_UN BIT_UN. napply (S_EL BIT_UN ut08 (refl_eq …) ?); #y; nelim y; ##[ ##37: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t09 : S_UN BIT_UN. napply (S_EL BIT_UN ut09 (refl_eq …) ?); #y; nelim y; ##[ ##38: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t0A : S_UN BIT_UN. napply (S_EL BIT_UN ut0A (refl_eq …) ?); #y; nelim y; ##[ ##39: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t0B : S_UN BIT_UN. napply (S_EL BIT_UN ut0B (refl_eq …) ?); #y; nelim y; ##[ ##40: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t0C : S_UN BIT_UN. napply (S_EL BIT_UN ut0C (refl_eq …) ?); #y; nelim y; ##[ ##41: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t0D : S_UN BIT_UN. napply (S_EL BIT_UN ut0D (refl_eq …) ?); #y; nelim y; ##[ ##42: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t0E : S_UN BIT_UN. napply (S_EL BIT_UN ut0E (refl_eq …) ?); #y; nelim y; ##[ ##43: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t0F : S_UN BIT_UN. napply (S_EL BIT_UN ut0F (refl_eq …) ?); #y; nelim y; ##[ ##44: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t10 : S_UN BIT_UN. napply (S_EL BIT_UN ut10 (refl_eq …) ?); #y; nelim y; ##[ ##45: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t11 : S_UN BIT_UN. napply (S_EL BIT_UN ut11 (refl_eq …) ?); #y; nelim y; ##[ ##46: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t12 : S_UN BIT_UN. napply (S_EL BIT_UN ut12 (refl_eq …) ?); #y; nelim y; ##[ ##47: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t13 : S_UN BIT_UN. napply (S_EL BIT_UN ut13 (refl_eq …) ?); #y; nelim y; ##[ ##48: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t14 : S_UN BIT_UN. napply (S_EL BIT_UN ut14 (refl_eq …) ?); #y; nelim y; ##[ ##49: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t15 : S_UN BIT_UN. napply (S_EL BIT_UN ut15 (refl_eq …) ?); #y; nelim y; ##[ ##50: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t16 : S_UN BIT_UN. napply (S_EL BIT_UN ut16 (refl_eq …) ?); #y; nelim y; ##[ ##51: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t17 : S_UN BIT_UN. napply (S_EL BIT_UN ut17 (refl_eq …) ?); #y; nelim y; ##[ ##52: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t18 : S_UN BIT_UN. napply (S_EL BIT_UN ut18 (refl_eq …) ?); #y; nelim y; ##[ ##53: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t19 : S_UN BIT_UN. napply (S_EL BIT_UN ut19 (refl_eq …) ?); #y; nelim y; ##[ ##54: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t1A : S_UN BIT_UN. napply (S_EL BIT_UN ut1A (refl_eq …) ?); #y; nelim y; ##[ ##55: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t1B : S_UN BIT_UN. napply (S_EL BIT_UN ut1B (refl_eq …) ?); #y; nelim y; ##[ ##56: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t1C : S_UN BIT_UN. napply (S_EL BIT_UN ut1C (refl_eq …) ?); #y; nelim y; ##[ ##57: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t1D : S_UN BIT_UN. napply (S_EL BIT_UN ut1D (refl_eq …) ?); #y; nelim y; ##[ ##58: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t1E : S_UN BIT_UN. napply (S_EL BIT_UN ut1E (refl_eq …) ?); #y; nelim y; ##[ ##59: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_t1F : S_UN BIT_UN. napply (S_EL BIT_UN ut1F (refl_eq …) ?); #y; nelim y; ##[ ##60: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/universe/exadecim.ma b/helm/software/matita/contribs/ng_assembly/universe/exadecim.ma new file mode 100755 index 000000000..f51d2ce3b --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/exadecim.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "universe/universe.ma". + +ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ]. + +(* derivati dall'universo + 1) SUN_destruct EX_UN + 2) eq_to_eqSUN EX_UN + 3) neq_to_neqSUN EX_UN + 4) eqSUN_to_eq EX_UN + 5) neqSUN_to_neq EX_UN + 6) decidable_SUN EX_UN + 7) symmetric_eqSUN EX_UN +*) + +nlemma un_x0 : S_UN EX_UN. napply (S_EL EX_UN ux0 (refl_eq …) ?); #y; nelim y; ##[ ##13: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x1 : S_UN EX_UN. napply (S_EL EX_UN ux1 (refl_eq …) ?); #y; nelim y; ##[ ##14: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x2 : S_UN EX_UN. napply (S_EL EX_UN ux2 (refl_eq …) ?); #y; nelim y; ##[ ##15: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x3 : S_UN EX_UN. napply (S_EL EX_UN ux3 (refl_eq …) ?); #y; nelim y; ##[ ##16: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x4 : S_UN EX_UN. napply (S_EL EX_UN ux4 (refl_eq …) ?); #y; nelim y; ##[ ##17: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x5 : S_UN EX_UN. napply (S_EL EX_UN ux5 (refl_eq …) ?); #y; nelim y; ##[ ##18: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x6 : S_UN EX_UN. napply (S_EL EX_UN ux6 (refl_eq …) ?); #y; nelim y; ##[ ##19: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x7 : S_UN EX_UN. napply (S_EL EX_UN ux7 (refl_eq …) ?); #y; nelim y; ##[ ##20: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x8 : S_UN EX_UN. napply (S_EL EX_UN ux8 (refl_eq …) ?); #y; nelim y; ##[ ##21: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_x9 : S_UN EX_UN. napply (S_EL EX_UN ux9 (refl_eq …) ?); #y; nelim y; ##[ ##22: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_xA : S_UN EX_UN. napply (S_EL EX_UN uxA (refl_eq …) ?); #y; nelim y; ##[ ##23: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_xB : S_UN EX_UN. napply (S_EL EX_UN uxB (refl_eq …) ?); #y; nelim y; ##[ ##24: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_xC : S_UN EX_UN. napply (S_EL EX_UN uxC (refl_eq …) ?); #y; nelim y; ##[ ##25: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_xD : S_UN EX_UN. napply (S_EL EX_UN uxD (refl_eq …) ?); #y; nelim y; ##[ ##26: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_xE : S_UN EX_UN. napply (S_EL EX_UN uxE (refl_eq …) ?); #y; nelim y; ##[ ##27: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_xF : S_UN EX_UN. napply (S_EL EX_UN uxF (refl_eq …) ?); #y; nelim y; ##[ ##28: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/universe/oct.ma b/helm/software/matita/contribs/ng_assembly/universe/oct.ma new file mode 100755 index 000000000..4de98f2e3 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/oct.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "universe/universe.ma". + +ndefinition OCT_UN ≝ [ uo0; uo1; uo2; uo3; uo4; uo5; uo6; uo7 ]. + +(* derivati dall'universo + 1) SUN_destruct OCT_UN + 2) eq_to_eqSUN OCT_UN + 3) neq_to_neqSUN OCT_UN + 4) eqSUN_to_eq OCT_UN + 5) neqSUN_to_neq OCT_UN + 6) decidable_SUN OCT_UN + 7) symmetric_eqSUN OCT_UN +*) + +nlemma un_o0 : S_UN OCT_UN. napply (S_EL OCT_UN uo0 (refl_eq …) ?); #y; nelim y; ##[ ##5: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o1 : S_UN OCT_UN. napply (S_EL OCT_UN uo1 (refl_eq …) ?); #y; nelim y; ##[ ##6: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o2 : S_UN OCT_UN. napply (S_EL OCT_UN uo2 (refl_eq …) ?); #y; nelim y; ##[ ##7: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o3 : S_UN OCT_UN. napply (S_EL OCT_UN uo3 (refl_eq …) ?); #y; nelim y; ##[ ##8: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o4 : S_UN OCT_UN. napply (S_EL OCT_UN uo4 (refl_eq …) ?); #y; nelim y; ##[ ##9: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o5 : S_UN OCT_UN. napply (S_EL OCT_UN uo5 (refl_eq …) ?); #y; nelim y; ##[ ##10: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o6 : S_UN OCT_UN. napply (S_EL OCT_UN uo6 (refl_eq …) ?); #y; nelim y; ##[ ##11: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_o7 : S_UN OCT_UN. napply (S_EL OCT_UN uo7 (refl_eq …) ?); #y; nelim y; ##[ ##12: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/universe/opcode.ma b/helm/software/matita/contribs/ng_assembly/universe/opcode.ma new file mode 100755 index 000000000..287d2668e --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/opcode.ma @@ -0,0 +1,136 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "universe/universe.ma". + +ndefinition OP_UN ≝ [ uADC; uADD; uAIS; uAIX; uAND; uASL; uASR; uBCC; uBCLRn; uBCS; + uBEQ; uBGE; uBGND; uBGT; uBHCC; uBHCS; uBHI; uBIH; uBIL; uBIT; + uBLE; uBLS; uBLT; uBMC; uBMI; uBMS; uBNE; uBPL; uBRA; uBRCLRn; + uBRN; uBRSETn; uBSETn; uBSR; uCBEQA; uCBEQX; uCLC; uCLI; uCLR; + uCMP; uCOM; uCPHX; uCPX; uDAA; uDBNZ; uDEC; uDIV; uEOR; uINC; + uJMP; uJSR; uLDA; uLDHX; uLDX; uLSR; uMOV; uMUL; uNEG; uNOP; + uNSA; uORA; uPSHA; uPSHH; uPSHX; uPULA; uPULH; uPULX; uROL; + uROR; uRSP; uRTI; uRTS; uSBC; uSEC; uSEI; uSHA; uSLA; uSTA; + uSTHX; uSTOP; uSTX; uSUB; uSWI; uTAP; uTAX; uTPA; uTST; uTSX; + uTXA; uTXS; uWAIT ]. + +(* derivati dall'universo + 1) SUN_destruct OP_UN + 2) eq_to_eqSUN OP_UN + 3) neq_to_neqSUN OP_UN + 4) eqSUN_to_eq OP_UN + 5) neqSUN_to_neq OP_UN + 6) decidable_SUN OP_UN + 7) symmetric_eqSUN OP_UN +*) + +nlemma un_ADC : S_UN OP_UN. napply (S_EL OP_UN uADC (refl_eq …) ?); #y; nelim y; ##[ ##124: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ADD : S_UN OP_UN. napply (S_EL OP_UN uADD (refl_eq …) ?); #y; nelim y; ##[ ##125: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_AIS : S_UN OP_UN. napply (S_EL OP_UN uAIS (refl_eq …) ?); #y; nelim y; ##[ ##126: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_AIX : S_UN OP_UN. napply (S_EL OP_UN uAIX (refl_eq …) ?); #y; nelim y; ##[ ##127: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_AND : S_UN OP_UN. napply (S_EL OP_UN uAND (refl_eq …) ?); #y; nelim y; ##[ ##128: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ASL : S_UN OP_UN. napply (S_EL OP_UN uASL (refl_eq …) ?); #y; nelim y; ##[ ##129: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ASR : S_UN OP_UN. napply (S_EL OP_UN uASR (refl_eq …) ?); #y; nelim y; ##[ ##130: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BCC : S_UN OP_UN. napply (S_EL OP_UN uBCC (refl_eq …) ?); #y; nelim y; ##[ ##131: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BCLRn : S_UN OP_UN. napply (S_EL OP_UN uBCLRn (refl_eq …) ?); #y; nelim y; ##[ ##132: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BCS : S_UN OP_UN. napply (S_EL OP_UN uBCS (refl_eq …) ?); #y; nelim y; ##[ ##133: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BEQ : S_UN OP_UN. napply (S_EL OP_UN uBEQ (refl_eq …) ?); #y; nelim y; ##[ ##134: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BGE : S_UN OP_UN. napply (S_EL OP_UN uBGE (refl_eq …) ?); #y; nelim y; ##[ ##135: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BGND : S_UN OP_UN. napply (S_EL OP_UN uBGND (refl_eq …) ?); #y; nelim y; ##[ ##136: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BGT : S_UN OP_UN. napply (S_EL OP_UN uBGT (refl_eq …) ?); #y; nelim y; ##[ ##137: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BHCC : S_UN OP_UN. napply (S_EL OP_UN uBHCC (refl_eq …) ?); #y; nelim y; ##[ ##138: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BHCS : S_UN OP_UN. napply (S_EL OP_UN uBHCS (refl_eq …) ?); #y; nelim y; ##[ ##139: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BHI : S_UN OP_UN. napply (S_EL OP_UN uBHI (refl_eq …) ?); #y; nelim y; ##[ ##140: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BIH : S_UN OP_UN. napply (S_EL OP_UN uBIH (refl_eq …) ?); #y; nelim y; ##[ ##141: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BIL : S_UN OP_UN. napply (S_EL OP_UN uBIL (refl_eq …) ?); #y; nelim y; ##[ ##142: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BIT : S_UN OP_UN. napply (S_EL OP_UN uBIT (refl_eq …) ?); #y; nelim y; ##[ ##143: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BLE : S_UN OP_UN. napply (S_EL OP_UN uBLE (refl_eq …) ?); #y; nelim y; ##[ ##144: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BLS : S_UN OP_UN. napply (S_EL OP_UN uBLS (refl_eq …) ?); #y; nelim y; ##[ ##145: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BLT : S_UN OP_UN. napply (S_EL OP_UN uBLT (refl_eq …) ?); #y; nelim y; ##[ ##146: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BMC : S_UN OP_UN. napply (S_EL OP_UN uBMC (refl_eq …) ?); #y; nelim y; ##[ ##147: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BMI : S_UN OP_UN. napply (S_EL OP_UN uBMI (refl_eq …) ?); #y; nelim y; ##[ ##148: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BMS : S_UN OP_UN. napply (S_EL OP_UN uBMS (refl_eq …) ?); #y; nelim y; ##[ ##149: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BNE : S_UN OP_UN. napply (S_EL OP_UN uBNE (refl_eq …) ?); #y; nelim y; ##[ ##150: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BPL : S_UN OP_UN. napply (S_EL OP_UN uBPL (refl_eq …) ?); #y; nelim y; ##[ ##151: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BRA : S_UN OP_UN. napply (S_EL OP_UN uBRA (refl_eq …) ?); #y; nelim y; ##[ ##152: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BRCLRn : S_UN OP_UN. napply (S_EL OP_UN uBRCLRn (refl_eq …) ?); #y; nelim y; ##[ ##153: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BRN : S_UN OP_UN. napply (S_EL OP_UN uBRN (refl_eq …) ?); #y; nelim y; ##[ ##154: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BRSETn : S_UN OP_UN. napply (S_EL OP_UN uBRSETn (refl_eq …) ?); #y; nelim y; ##[ ##155: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BSETn : S_UN OP_UN. napply (S_EL OP_UN uBSETn (refl_eq …) ?); #y; nelim y; ##[ ##156: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_BSR : S_UN OP_UN. napply (S_EL OP_UN uBSR (refl_eq …) ?); #y; nelim y; ##[ ##157: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CBEQA : S_UN OP_UN. napply (S_EL OP_UN uCBEQA (refl_eq …) ?); #y; nelim y; ##[ ##158: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CBEQX : S_UN OP_UN. napply (S_EL OP_UN uCBEQX (refl_eq …) ?); #y; nelim y; ##[ ##159: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CLC : S_UN OP_UN. napply (S_EL OP_UN uCLC (refl_eq …) ?); #y; nelim y; ##[ ##160: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CLI : S_UN OP_UN. napply (S_EL OP_UN uCLI (refl_eq …) ?); #y; nelim y; ##[ ##161: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CLR : S_UN OP_UN. napply (S_EL OP_UN uCLR (refl_eq …) ?); #y; nelim y; ##[ ##162: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CMP : S_UN OP_UN. napply (S_EL OP_UN uCMP (refl_eq …) ?); #y; nelim y; ##[ ##163: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_COM : S_UN OP_UN. napply (S_EL OP_UN uCOM (refl_eq …) ?); #y; nelim y; ##[ ##164: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CPHX : S_UN OP_UN. napply (S_EL OP_UN uCPHX (refl_eq …) ?); #y; nelim y; ##[ ##165: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_CPX : S_UN OP_UN. napply (S_EL OP_UN uCPX (refl_eq …) ?); #y; nelim y; ##[ ##166: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_DAA : S_UN OP_UN. napply (S_EL OP_UN uDAA (refl_eq …) ?); #y; nelim y; ##[ ##167: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_DBNZ : S_UN OP_UN. napply (S_EL OP_UN uDBNZ (refl_eq …) ?); #y; nelim y; ##[ ##168: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_DEC : S_UN OP_UN. napply (S_EL OP_UN uDEC (refl_eq …) ?); #y; nelim y; ##[ ##169: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_DIV : S_UN OP_UN. napply (S_EL OP_UN uDIV (refl_eq …) ?); #y; nelim y; ##[ ##170: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_EOR : S_UN OP_UN. napply (S_EL OP_UN uEOR (refl_eq …) ?); #y; nelim y; ##[ ##171: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_INC : S_UN OP_UN. napply (S_EL OP_UN uINC (refl_eq …) ?); #y; nelim y; ##[ ##172: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_JMP : S_UN OP_UN. napply (S_EL OP_UN uJMP (refl_eq …) ?); #y; nelim y; ##[ ##173: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_JSR : S_UN OP_UN. napply (S_EL OP_UN uJSR (refl_eq …) ?); #y; nelim y; ##[ ##174: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_LDA : S_UN OP_UN. napply (S_EL OP_UN uLDA (refl_eq …) ?); #y; nelim y; ##[ ##175: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_LDHX : S_UN OP_UN. napply (S_EL OP_UN uLDHX (refl_eq …) ?); #y; nelim y; ##[ ##176: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_LDX : S_UN OP_UN. napply (S_EL OP_UN uLDX (refl_eq …) ?); #y; nelim y; ##[ ##177: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_LSR : S_UN OP_UN. napply (S_EL OP_UN uLSR (refl_eq …) ?); #y; nelim y; ##[ ##178: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_MOV : S_UN OP_UN. napply (S_EL OP_UN uMOV (refl_eq …) ?); #y; nelim y; ##[ ##179: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_MUL : S_UN OP_UN. napply (S_EL OP_UN uMUL (refl_eq …) ?); #y; nelim y; ##[ ##180: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_NEG : S_UN OP_UN. napply (S_EL OP_UN uNEG (refl_eq …) ?); #y; nelim y; ##[ ##181: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_NOP : S_UN OP_UN. napply (S_EL OP_UN uNOP (refl_eq …) ?); #y; nelim y; ##[ ##182: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_NSA : S_UN OP_UN. napply (S_EL OP_UN uNSA (refl_eq …) ?); #y; nelim y; ##[ ##183: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ORA : S_UN OP_UN. napply (S_EL OP_UN uORA (refl_eq …) ?); #y; nelim y; ##[ ##184: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_PSHA : S_UN OP_UN. napply (S_EL OP_UN uPSHA (refl_eq …) ?); #y; nelim y; ##[ ##185: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_PSHH : S_UN OP_UN. napply (S_EL OP_UN uPSHH (refl_eq …) ?); #y; nelim y; ##[ ##186: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_PSHX : S_UN OP_UN. napply (S_EL OP_UN uPSHX (refl_eq …) ?); #y; nelim y; ##[ ##187: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_PULA : S_UN OP_UN. napply (S_EL OP_UN uPULA (refl_eq …) ?); #y; nelim y; ##[ ##188: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_PULH : S_UN OP_UN. napply (S_EL OP_UN uPULH (refl_eq …) ?); #y; nelim y; ##[ ##189: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_PULX : S_UN OP_UN. napply (S_EL OP_UN uPULX (refl_eq …) ?); #y; nelim y; ##[ ##190: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ROL : S_UN OP_UN. napply (S_EL OP_UN uROL (refl_eq …) ?); #y; nelim y; ##[ ##191: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_ROR : S_UN OP_UN. napply (S_EL OP_UN uROR (refl_eq …) ?); #y; nelim y; ##[ ##192: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_RSP : S_UN OP_UN. napply (S_EL OP_UN uRSP (refl_eq …) ?); #y; nelim y; ##[ ##193: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_RTI : S_UN OP_UN. napply (S_EL OP_UN uRTI (refl_eq …) ?); #y; nelim y; ##[ ##194: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_RTS : S_UN OP_UN. napply (S_EL OP_UN uRTS (refl_eq …) ?); #y; nelim y; ##[ ##195: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SBC : S_UN OP_UN. napply (S_EL OP_UN uSBC (refl_eq …) ?); #y; nelim y; ##[ ##196: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SEC : S_UN OP_UN. napply (S_EL OP_UN uSEC (refl_eq …) ?); #y; nelim y; ##[ ##197: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SEI : S_UN OP_UN. napply (S_EL OP_UN uSEI (refl_eq …) ?); #y; nelim y; ##[ ##198: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SHA : S_UN OP_UN. napply (S_EL OP_UN uSHA (refl_eq …) ?); #y; nelim y; ##[ ##199: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SLA : S_UN OP_UN. napply (S_EL OP_UN uSLA (refl_eq …) ?); #y; nelim y; ##[ ##200: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_STA : S_UN OP_UN. napply (S_EL OP_UN uSTA (refl_eq …) ?); #y; nelim y; ##[ ##201: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_STHX : S_UN OP_UN. napply (S_EL OP_UN uSTHX (refl_eq …) ?); #y; nelim y; ##[ ##202: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_STOP : S_UN OP_UN. napply (S_EL OP_UN uSTOP (refl_eq …) ?); #y; nelim y; ##[ ##203: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_STX : S_UN OP_UN. napply (S_EL OP_UN uSTX (refl_eq …) ?); #y; nelim y; ##[ ##204: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SUB : S_UN OP_UN. napply (S_EL OP_UN uSUB (refl_eq …) ?); #y; nelim y; ##[ ##205: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_SWI : S_UN OP_UN. napply (S_EL OP_UN uSWI (refl_eq …) ?); #y; nelim y; ##[ ##206: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TAP : S_UN OP_UN. napply (S_EL OP_UN uTAP (refl_eq …) ?); #y; nelim y; ##[ ##207: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TAX : S_UN OP_UN. napply (S_EL OP_UN uTAX (refl_eq …) ?); #y; nelim y; ##[ ##208: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TPA : S_UN OP_UN. napply (S_EL OP_UN uTPA (refl_eq …) ?); #y; nelim y; ##[ ##209: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TST : S_UN OP_UN. napply (S_EL OP_UN uTST (refl_eq …) ?); #y; nelim y; ##[ ##210: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TSX : S_UN OP_UN. napply (S_EL OP_UN uTSX (refl_eq …) ?); #y; nelim y; ##[ ##211: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TXA : S_UN OP_UN. napply (S_EL OP_UN uTXA (refl_eq …) ?); #y; nelim y; ##[ ##212: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_TXS : S_UN OP_UN. napply (S_EL OP_UN uTXS (refl_eq …) ?); #y; nelim y; ##[ ##213: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_WAIT : S_UN OP_UN. napply (S_EL OP_UN uWAIT (refl_eq …) ?); #y; nelim y; ##[ ##214: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/universe/quatern.ma b/helm/software/matita/contribs/ng_assembly/universe/quatern.ma new file mode 100755 index 000000000..d4137d6f1 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/quatern.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "universe/universe.ma". + +ndefinition QU_UN ≝ [ uq0; uq1; uq2; uq3 ]. + +(* derivati dall'universo + 1) SUN_destruct QU_UN + 2) eq_to_eqSUN QU_UN + 3) neq_to_neqSUN QU_UN + 4) eqSUN_to_eq QU_UN + 5) neqSUN_to_neq QU_UN + 6) decidable_SUN QU_UN + 7) symmetric_eqSUN QU_UN +*) + +nlemma un_q0 : S_UN QU_UN. napply (S_EL QU_UN uq0 (refl_eq …) ?); #y; nelim y; ##[ ##1: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_q1 : S_UN QU_UN. napply (S_EL QU_UN uq1 (refl_eq …) ?); #y; nelim y; ##[ ##2: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_q2 : S_UN QU_UN. napply (S_EL QU_UN uq2 (refl_eq …) ?); #y; nelim y; ##[ ##3: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. +nlemma un_q3 : S_UN QU_UN. napply (S_EL QU_UN uq3 (refl_eq …) ?); #y; nelim y; ##[ ##4: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma similarity index 67% rename from helm/software/matita/contribs/ng_assembly/common/meta_type.ma rename to helm/software/matita/contribs/ng_assembly/universe/universe.ma index 1ba04df07..2d84b78e5 100755 --- a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma +++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma @@ -20,7 +20,8 @@ (* *) (* ********************************************************************** *) -include "common/list_utility_lemmas.ma". +include "common/list.ma". +include "num/bool_lemmas.ma". nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝ match l with @@ -173,97 +174,97 @@ ninductive UN : Type ≝ | uch_z : UN (* opcode[91] 124-214 *) -| ADC : UN -| ADD : UN -| AIS : UN -| AIX : UN -| AND : UN -| ASL : UN -| ASR : UN -| BCC : UN -| BCLRn : UN -| BCS : UN -| BEQ : UN -| BGE : UN -| BGND : UN -| BGT : UN -| BHCC : UN -| BHCS : UN -| BHI : UN -| BIH : UN -| BIL : UN -| BIT : UN -| BLE : UN -| BLS : UN -| BLT : UN -| BMC : UN -| BMI : UN -| BMS : UN -| BNE : UN -| BPL : UN -| BRA : UN -| BRCLRn : UN -| BRN : UN -| BRSETn : UN -| BSETn : UN -| BSR : UN -| CBEQA : UN -| CBEQX : UN -| CLC : UN -| CLI : UN -| CLR : UN -| CMP : UN -| COM : UN -| CPHX : UN -| CPX : UN -| DAA : UN -| DBNZ : UN -| DEC : UN -| DIV : UN -| EOR : UN -| INC : UN -| JMP : UN -| JSR : UN -| LDA : UN -| LDHX : UN -| LDX : UN -| LSR : UN -| MOV : UN -| MUL : UN -| NEG : UN -| NOP : UN -| NSA : UN -| ORA : UN -| PSHA : UN -| PSHH : UN -| PSHX : UN -| PULA : UN -| PULH : UN -| PULX : UN -| ROL : UN -| ROR : UN -| RSP : UN -| RTI : UN -| RTS : UN -| SBC : UN -| SEC : UN -| SEI : UN -| SHA : UN -| SLA : UN -| STA : UN -| STHX : UN -| STOP : UN -| STX : UN -| SUB : UN -| SWI : UN -| TAP : UN -| TAX : UN -| TPA : UN -| TST : UN -| TSX : UN -| TXA : UN -| TXS : UN -| WAIT : UN +| uADC : UN +| uADD : UN +| uAIS : UN +| uAIX : UN +| uAND : UN +| uASL : UN +| uASR : UN +| uBCC : UN +| uBCLRn : UN +| uBCS : UN +| uBEQ : UN +| uBGE : UN +| uBGND : UN +| uBGT : UN +| uBHCC : UN +| uBHCS : UN +| uBHI : UN +| uBIH : UN +| uBIL : UN +| uBIT : UN +| uBLE : UN +| uBLS : UN +| uBLT : UN +| uBMC : UN +| uBMI : UN +| uBMS : UN +| uBNE : UN +| uBPL : UN +| uBRA : UN +| uBRCLRn : UN +| uBRN : UN +| uBRSETn : UN +| uBSETn : UN +| uBSR : UN +| uCBEQA : UN +| uCBEQX : UN +| uCLC : UN +| uCLI : UN +| uCLR : UN +| uCMP : UN +| uCOM : UN +| uCPHX : UN +| uCPX : UN +| uDAA : UN +| uDBNZ : UN +| uDEC : UN +| uDIV : UN +| uEOR : UN +| uINC : UN +| uJMP : UN +| uJSR : UN +| uLDA : UN +| uLDHX : UN +| uLDX : UN +| uLSR : UN +| uMOV : UN +| uMUL : UN +| uNEG : UN +| uNOP : UN +| uNSA : UN +| uORA : UN +| uPSHA : UN +| uPSHH : UN +| uPSHX : UN +| uPULA : UN +| uPULH : UN +| uPULX : UN +| uROL : UN +| uROR : UN +| uRSP : UN +| uRTI : UN +| uRTS : UN +| uSBC : UN +| uSEC : UN +| uSEI : UN +| uSHA : UN +| uSLA : UN +| uSTA : UN +| uSTHX : UN +| uSTOP : UN +| uSTX : UN +| uSUB : UN +| uSWI : UN +| uTAP : UN +| uTAX : UN +| uTPA : UN +| uTST : UN +| uTSX : UN +| uTXA : UN +| uTXS : UN +| uWAIT : UN . (* funzione di uguaglianza sugli atomi *) @@ -397,97 +398,97 @@ ndefinition eq_UN ≝ | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ] | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ] - | ADC ⇒ match u2 with [ ADC ⇒ true | _ ⇒ false ] - | ADD ⇒ match u2 with [ ADD ⇒ true | _ ⇒ false ] - | AIS ⇒ match u2 with [ AIS ⇒ true | _ ⇒ false ] - | AIX ⇒ match u2 with [ AIX ⇒ true | _ ⇒ false ] - | AND ⇒ match u2 with [ AND ⇒ true | _ ⇒ false ] - | ASL ⇒ match u2 with [ ASL ⇒ true | _ ⇒ false ] - | ASR ⇒ match u2 with [ ASR ⇒ true | _ ⇒ false ] - | BCC ⇒ match u2 with [ BCC ⇒ true | _ ⇒ false ] - | BCLRn ⇒ match u2 with [ BCLRn ⇒ true | _ ⇒ false ] - | BCS ⇒ match u2 with [ BCS ⇒ true | _ ⇒ false ] - | BEQ ⇒ match u2 with [ BEQ ⇒ true | _ ⇒ false ] - | BGE ⇒ match u2 with [ BGE ⇒ true | _ ⇒ false ] - | BGND ⇒ match u2 with [ BGND ⇒ true | _ ⇒ false ] - | BGT ⇒ match u2 with [ BGT ⇒ true | _ ⇒ false ] - | BHCC ⇒ match u2 with [ BHCC ⇒ true | _ ⇒ false ] - | BHCS ⇒ match u2 with [ BHCS ⇒ true | _ ⇒ false ] - | BHI ⇒ match u2 with [ BHI ⇒ true | _ ⇒ false ] - | BIH ⇒ match u2 with [ BIH ⇒ true | _ ⇒ false ] - | BIL ⇒ match u2 with [ BIL ⇒ true | _ ⇒ false ] - | BIT ⇒ match u2 with [ BIT ⇒ true | _ ⇒ false ] - | BLE ⇒ match u2 with [ BLE ⇒ true | _ ⇒ false ] - | BLS ⇒ match u2 with [ BLS ⇒ true | _ ⇒ false ] - | BLT ⇒ match u2 with [ BLT ⇒ true | _ ⇒ false ] - | BMC ⇒ match u2 with [ BMC ⇒ true | _ ⇒ false ] - | BMI ⇒ match u2 with [ BMI ⇒ true | _ ⇒ false ] - | BMS ⇒ match u2 with [ BMS ⇒ true | _ ⇒ false ] - | BNE ⇒ match u2 with [ BNE ⇒ true | _ ⇒ false ] - | BPL ⇒ match u2 with [ BPL ⇒ true | _ ⇒ false ] - | BRA ⇒ match u2 with [ BRA ⇒ true | _ ⇒ false ] - | BRCLRn ⇒ match u2 with [ BRCLRn ⇒ true | _ ⇒ false ] - | BRN ⇒ match u2 with [ BRN ⇒ true | _ ⇒ false ] - | BRSETn ⇒ match u2 with [ BRSETn ⇒ true | _ ⇒ false ] - | BSETn ⇒ match u2 with [ BSETn ⇒ true | _ ⇒ false ] - | BSR ⇒ match u2 with [ BSR ⇒ true | _ ⇒ false ] - | CBEQA ⇒ match u2 with [ CBEQA ⇒ true | _ ⇒ false ] - | CBEQX ⇒ match u2 with [ CBEQX ⇒ true | _ ⇒ false ] - | CLC ⇒ match u2 with [ CLC ⇒ true | _ ⇒ false ] - | CLI ⇒ match u2 with [ CLI ⇒ true | _ ⇒ false ] - | CLR ⇒ match u2 with [ CLR ⇒ true | _ ⇒ false ] - | CMP ⇒ match u2 with [ CMP ⇒ true | _ ⇒ false ] - | COM ⇒ match u2 with [ COM ⇒ true | _ ⇒ false ] - | CPHX ⇒ match u2 with [ CPHX ⇒ true | _ ⇒ false ] - | CPX ⇒ match u2 with [ CPX ⇒ true | _ ⇒ false ] - | DAA ⇒ match u2 with [ DAA ⇒ true | _ ⇒ false ] - | DBNZ ⇒ match u2 with [ DBNZ ⇒ true | _ ⇒ false ] - | DEC ⇒ match u2 with [ DEC ⇒ true | _ ⇒ false ] - | DIV ⇒ match u2 with [ DIV ⇒ true | _ ⇒ false ] - | EOR ⇒ match u2 with [ EOR ⇒ true | _ ⇒ false ] - | INC ⇒ match u2 with [ INC ⇒ true | _ ⇒ false ] - | JMP ⇒ match u2 with [ JMP ⇒ true | _ ⇒ false ] - | JSR ⇒ match u2 with [ JSR ⇒ true | _ ⇒ false ] - | LDA ⇒ match u2 with [ LDA ⇒ true | _ ⇒ false ] - | LDHX ⇒ match u2 with [ LDHX ⇒ true | _ ⇒ false ] - | LDX ⇒ match u2 with [ LDX ⇒ true | _ ⇒ false ] - | LSR ⇒ match u2 with [ LSR ⇒ true | _ ⇒ false ] - | MOV ⇒ match u2 with [ MOV ⇒ true | _ ⇒ false ] - | MUL ⇒ match u2 with [ MUL ⇒ true | _ ⇒ false ] - | NEG ⇒ match u2 with [ NEG ⇒ true | _ ⇒ false ] - | NOP ⇒ match u2 with [ NOP ⇒ true | _ ⇒ false ] - | NSA ⇒ match u2 with [ NSA ⇒ true | _ ⇒ false ] - | ORA ⇒ match u2 with [ ORA ⇒ true | _ ⇒ false ] - | PSHA ⇒ match u2 with [ PSHA ⇒ true | _ ⇒ false ] - | PSHH ⇒ match u2 with [ PSHH ⇒ true | _ ⇒ false ] - | PSHX ⇒ match u2 with [ PSHX ⇒ true | _ ⇒ false ] - | PULA ⇒ match u2 with [ PULA ⇒ true | _ ⇒ false ] - | PULH ⇒ match u2 with [ PULH ⇒ true | _ ⇒ false ] - | PULX ⇒ match u2 with [ PULX ⇒ true | _ ⇒ false ] - | ROL ⇒ match u2 with [ ROL ⇒ true | _ ⇒ false ] - | ROR ⇒ match u2 with [ ROR ⇒ true | _ ⇒ false ] - | RSP ⇒ match u2 with [ RSP ⇒ true | _ ⇒ false ] - | RTI ⇒ match u2 with [ RTI ⇒ true | _ ⇒ false ] - | RTS ⇒ match u2 with [ RTS ⇒ true | _ ⇒ false ] - | SBC ⇒ match u2 with [ SBC ⇒ true | _ ⇒ false ] - | SEC ⇒ match u2 with [ SEC ⇒ true | _ ⇒ false ] - | SEI ⇒ match u2 with [ SEI ⇒ true | _ ⇒ false ] - | SHA ⇒ match u2 with [ SHA ⇒ true | _ ⇒ false ] - | SLA ⇒ match u2 with [ SLA ⇒ true | _ ⇒ false ] - | STA ⇒ match u2 with [ STA ⇒ true | _ ⇒ false ] - | STHX ⇒ match u2 with [ STHX ⇒ true | _ ⇒ false ] - | STOP ⇒ match u2 with [ STOP ⇒ true | _ ⇒ false ] - | STX ⇒ match u2 with [ STX ⇒ true | _ ⇒ false ] - | SUB ⇒ match u2 with [ SUB ⇒ true | _ ⇒ false ] - | SWI ⇒ match u2 with [ SWI ⇒ true | _ ⇒ false ] - | TAP ⇒ match u2 with [ TAP ⇒ true | _ ⇒ false ] - | TAX ⇒ match u2 with [ TAX ⇒ true | _ ⇒ false ] - | TPA ⇒ match u2 with [ TPA ⇒ true | _ ⇒ false ] - | TST ⇒ match u2 with [ TST ⇒ true | _ ⇒ false ] - | TSX ⇒ match u2 with [ TSX ⇒ true | _ ⇒ false ] - | TXA ⇒ match u2 with [ TXA ⇒ true | _ ⇒ false ] - | TXS ⇒ match u2 with [ TXS ⇒ true | _ ⇒ false ] - | WAIT ⇒ match u2 with [ WAIT ⇒ true | _ ⇒ false ] + | uADC ⇒ match u2 with [ uADC ⇒ true | _ ⇒ false ] + | uADD ⇒ match u2 with [ uADD ⇒ true | _ ⇒ false ] + | uAIS ⇒ match u2 with [ uAIS ⇒ true | _ ⇒ false ] + | uAIX ⇒ match u2 with [ uAIX ⇒ true | _ ⇒ false ] + | uAND ⇒ match u2 with [ uAND ⇒ true | _ ⇒ false ] + | uASL ⇒ match u2 with [ uASL ⇒ true | _ ⇒ false ] + | uASR ⇒ match u2 with [ uASR ⇒ true | _ ⇒ false ] + | uBCC ⇒ match u2 with [ uBCC ⇒ true | _ ⇒ false ] + | uBCLRn ⇒ match u2 with [ uBCLRn ⇒ true | _ ⇒ false ] + | uBCS ⇒ match u2 with [ uBCS ⇒ true | _ ⇒ false ] + | uBEQ ⇒ match u2 with [ uBEQ ⇒ true | _ ⇒ false ] + | uBGE ⇒ match u2 with [ uBGE ⇒ true | _ ⇒ false ] + | uBGND ⇒ match u2 with [ uBGND ⇒ true | _ ⇒ false ] + | uBGT ⇒ match u2 with [ uBGT ⇒ true | _ ⇒ false ] + | uBHCC ⇒ match u2 with [ uBHCC ⇒ true | _ ⇒ false ] + | uBHCS ⇒ match u2 with [ uBHCS ⇒ true | _ ⇒ false ] + | uBHI ⇒ match u2 with [ uBHI ⇒ true | _ ⇒ false ] + | uBIH ⇒ match u2 with [ uBIH ⇒ true | _ ⇒ false ] + | uBIL ⇒ match u2 with [ uBIL ⇒ true | _ ⇒ false ] + | uBIT ⇒ match u2 with [ uBIT ⇒ true | _ ⇒ false ] + | uBLE ⇒ match u2 with [ uBLE ⇒ true | _ ⇒ false ] + | uBLS ⇒ match u2 with [ uBLS ⇒ true | _ ⇒ false ] + | uBLT ⇒ match u2 with [ uBLT ⇒ true | _ ⇒ false ] + | uBMC ⇒ match u2 with [ uBMC ⇒ true | _ ⇒ false ] + | uBMI ⇒ match u2 with [ uBMI ⇒ true | _ ⇒ false ] + | uBMS ⇒ match u2 with [ uBMS ⇒ true | _ ⇒ false ] + | uBNE ⇒ match u2 with [ uBNE ⇒ true | _ ⇒ false ] + | uBPL ⇒ match u2 with [ uBPL ⇒ true | _ ⇒ false ] + | uBRA ⇒ match u2 with [ uBRA ⇒ true | _ ⇒ false ] + | uBRCLRn ⇒ match u2 with [ uBRCLRn ⇒ true | _ ⇒ false ] + | uBRN ⇒ match u2 with [ uBRN ⇒ true | _ ⇒ false ] + | uBRSETn ⇒ match u2 with [ uBRSETn ⇒ true | _ ⇒ false ] + | uBSETn ⇒ match u2 with [ uBSETn ⇒ true | _ ⇒ false ] + | uBSR ⇒ match u2 with [ uBSR ⇒ true | _ ⇒ false ] + | uCBEQA ⇒ match u2 with [ uCBEQA ⇒ true | _ ⇒ false ] + | uCBEQX ⇒ match u2 with [ uCBEQX ⇒ true | _ ⇒ false ] + | uCLC ⇒ match u2 with [ uCLC ⇒ true | _ ⇒ false ] + | uCLI ⇒ match u2 with [ uCLI ⇒ true | _ ⇒ false ] + | uCLR ⇒ match u2 with [ uCLR ⇒ true | _ ⇒ false ] + | uCMP ⇒ match u2 with [ uCMP ⇒ true | _ ⇒ false ] + | uCOM ⇒ match u2 with [ uCOM ⇒ true | _ ⇒ false ] + | uCPHX ⇒ match u2 with [ uCPHX ⇒ true | _ ⇒ false ] + | uCPX ⇒ match u2 with [ uCPX ⇒ true | _ ⇒ false ] + | uDAA ⇒ match u2 with [ uDAA ⇒ true | _ ⇒ false ] + | uDBNZ ⇒ match u2 with [ uDBNZ ⇒ true | _ ⇒ false ] + | uDEC ⇒ match u2 with [ uDEC ⇒ true | _ ⇒ false ] + | uDIV ⇒ match u2 with [ uDIV ⇒ true | _ ⇒ false ] + | uEOR ⇒ match u2 with [ uEOR ⇒ true | _ ⇒ false ] + | uINC ⇒ match u2 with [ uINC ⇒ true | _ ⇒ false ] + | uJMP ⇒ match u2 with [ uJMP ⇒ true | _ ⇒ false ] + | uJSR ⇒ match u2 with [ uJSR ⇒ true | _ ⇒ false ] + | uLDA ⇒ match u2 with [ uLDA ⇒ true | _ ⇒ false ] + | uLDHX ⇒ match u2 with [ uLDHX ⇒ true | _ ⇒ false ] + | uLDX ⇒ match u2 with [ uLDX ⇒ true | _ ⇒ false ] + | uLSR ⇒ match u2 with [ uLSR ⇒ true | _ ⇒ false ] + | uMOV ⇒ match u2 with [ uMOV ⇒ true | _ ⇒ false ] + | uMUL ⇒ match u2 with [ uMUL ⇒ true | _ ⇒ false ] + | uNEG ⇒ match u2 with [ uNEG ⇒ true | _ ⇒ false ] + | uNOP ⇒ match u2 with [ uNOP ⇒ true | _ ⇒ false ] + | uNSA ⇒ match u2 with [ uNSA ⇒ true | _ ⇒ false ] + | uORA ⇒ match u2 with [ uORA ⇒ true | _ ⇒ false ] + | uPSHA ⇒ match u2 with [ uPSHA ⇒ true | _ ⇒ false ] + | uPSHH ⇒ match u2 with [ uPSHH ⇒ true | _ ⇒ false ] + | uPSHX ⇒ match u2 with [ uPSHX ⇒ true | _ ⇒ false ] + | uPULA ⇒ match u2 with [ uPULA ⇒ true | _ ⇒ false ] + | uPULH ⇒ match u2 with [ uPULH ⇒ true | _ ⇒ false ] + | uPULX ⇒ match u2 with [ uPULX ⇒ true | _ ⇒ false ] + | uROL ⇒ match u2 with [ uROL ⇒ true | _ ⇒ false ] + | uROR ⇒ match u2 with [ uROR ⇒ true | _ ⇒ false ] + | uRSP ⇒ match u2 with [ uRSP ⇒ true | _ ⇒ false ] + | uRTI ⇒ match u2 with [ uRTI ⇒ true | _ ⇒ false ] + | uRTS ⇒ match u2 with [ uRTS ⇒ true | _ ⇒ false ] + | uSBC ⇒ match u2 with [ uSBC ⇒ true | _ ⇒ false ] + | uSEC ⇒ match u2 with [ uSEC ⇒ true | _ ⇒ false ] + | uSEI ⇒ match u2 with [ uSEI ⇒ true | _ ⇒ false ] + | uSHA ⇒ match u2 with [ uSHA ⇒ true | _ ⇒ false ] + | uSLA ⇒ match u2 with [ uSLA ⇒ true | _ ⇒ false ] + | uSTA ⇒ match u2 with [ uSTA ⇒ true | _ ⇒ false ] + | uSTHX ⇒ match u2 with [ uSTHX ⇒ true | _ ⇒ false ] + | uSTOP ⇒ match u2 with [ uSTOP ⇒ true | _ ⇒ false ] + | uSTX ⇒ match u2 with [ uSTX ⇒ true | _ ⇒ false ] + | uSUB ⇒ match u2 with [ uSUB ⇒ true | _ ⇒ false ] + | uSWI ⇒ match u2 with [ uSWI ⇒ true | _ ⇒ false ] + | uTAP ⇒ match u2 with [ uTAP ⇒ true | _ ⇒ false ] + | uTAX ⇒ match u2 with [ uTAX ⇒ true | _ ⇒ false ] + | uTPA ⇒ match u2 with [ uTPA ⇒ true | _ ⇒ false ] + | uTST ⇒ match u2 with [ uTST ⇒ true | _ ⇒ false ] + | uTSX ⇒ match u2 with [ uTSX ⇒ true | _ ⇒ false ] + | uTXA ⇒ match u2 with [ uTXA ⇒ true | _ ⇒ false ] + | uTXS ⇒ match u2 with [ uTXS ⇒ true | _ ⇒ false ] + | uWAIT ⇒ match u2 with [ uWAIT ⇒ true | _ ⇒ false ] ]. @@ -680,35 +681,3 @@ nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l). napply (neq_to_neqSUN l … (symmetric_neq … H)) ##] nqed. - -(* -ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ]. - -ndefinition f1_EX_UN - : ∀e:S_UN EX_UN. - ∀f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN. - S_UN EX_UN. - #input; #f1; #f2; #f3; #f4; #f5; #f6; #f7; #f8; #f9; #f10; #f11; #f12; #f13; #f14; #f15; #f16; - nelim input; - ##[ ##2: #H; nelim H - ##| ##1: #u; #H; nelim u in H:(%); #H; - ##[ ##13: napply f1 ##| ##14: napply f2 ##| ##15: napply f3 ##| ##16: napply f4 - ##| ##17: napply f5 ##| ##18: napply f6 ##| ##19: napply f7 ##| ##20: napply f8 - ##| ##21: napply f9 ##| ##22: napply f10 ##| ##23: napply f11 ##| ##24: napply f12 - ##| ##25: napply f13 ##| ##26: napply f14 ##| ##27: napply f15 ##| ##28: napply f16 - ##| ##*: nnormalize in H:(%); napply (S_KO EX_UN (bool_destruct false true False H)) - ##] - ##] -nqed. - -ndefinition succ_EX_UN ≝ -λe:S_UN EX_UN.f1_EX_UN - (S_EL EX_UN ux1 (refl_eq …)) (S_EL EX_UN ux2 (refl_eq …)) - (S_EL EX_UN ux3 (refl_eq …)) (S_EL EX_UN ux4 (refl_eq …)) - (S_EL EX_UN ux5 (refl_eq …)) (S_EL EX_UN ux6 (refl_eq …)) - (S_EL EX_UN ux7 (refl_eq …)) (S_EL EX_UN ux8 (refl_eq …)) - (S_EL EX_UN ux9 (refl_eq …)) (S_EL EX_UN uxA (refl_eq …)) - (S_EL EX_UN uxB (refl_eq …)) (S_EL EX_UN uxC (refl_eq …)) - (S_EL EX_UN uxD (refl_eq …)) (S_EL EX_UN uxE (refl_eq …)) - (S_EL EX_UN uxF (refl_eq …)) (S_EL EX_UN ux0 (refl_eq …)). -*) -- 2.39.2