From: Cosimo Oliboni Date: Wed, 12 Aug 2009 22:54:21 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3551 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9b16ad62794042c2b31c6e3433b3c4035f8a0d5;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma b/helm/software/matita/contribs/ng_assembly/common/meta_type.ma deleted file mode 100755 index 1ba04df07..000000000 --- a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma +++ /dev/null @@ -1,714 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "common/list_utility_lemmas.ma". - -nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝ - match l with - [ nil ⇒ true - | cons h t ⇒ match f elem h with - [ true ⇒ false | false ⇒ nmember_list T elem f t ] - ]. - -(* elem presente una ed una sola volta in l *) -nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝ - match l with - [ nil ⇒ false - | cons h t ⇒ match f elem h with - [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ] - ]. - -(* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *) -ninductive UN : Type ≝ -(* quaternari[4] 1-4 *) - uq0 : UN -| uq1 : UN -| uq2 : UN -| uq3 : UN - -(* ottali[8] 5-12 *) -| uo0 : UN -| uo1 : UN -| uo2 : UN -| uo3 : UN -| uo4 : UN -| uo5 : UN -| uo6 : UN -| uo7 : UN - -(* esadecimali[16] 13-28 *) -| ux0 : UN -| ux1 : UN -| ux2 : UN -| ux3 : UN -| ux4 : UN -| ux5 : UN -| ux6 : UN -| ux7 : UN -| ux8 : UN -| ux9 : UN -| uxA : UN -| uxB : UN -| uxC : UN -| uxD : UN -| uxE : UN -| uxF : UN - -(* bitrigesimali[32] 29-60 *) -| ut00 : UN -| ut01 : UN -| ut02 : UN -| ut03 : UN -| ut04 : UN -| ut05 : UN -| ut06 : UN -| ut07 : UN -| ut08 : UN -| ut09 : UN -| ut0A : UN -| ut0B : UN -| ut0C : UN -| ut0D : UN -| ut0E : UN -| ut0F : UN -| ut10 : UN -| ut11 : UN -| ut12 : UN -| ut13 : UN -| ut14 : UN -| ut15 : UN -| ut16 : UN -| ut17 : UN -| ut18 : UN -| ut19 : UN -| ut1A : UN -| ut1B : UN -| ut1C : UN -| ut1D : UN -| ut1E : UN -| ut1F : UN - -(* ascii[63] 61-123 *) -| uch_0 : UN -| uch_1 : UN -| uch_2 : UN -| uch_3 : UN -| uch_4 : UN -| uch_5 : UN -| uch_6 : UN -| uch_7 : UN -| uch_8 : UN -| uch_9 : UN -| uch__ : UN -| uch_A : UN -| uch_B : UN -| uch_C : UN -| uch_D : UN -| uch_E : UN -| uch_F : UN -| uch_G : UN -| uch_H : UN -| uch_I : UN -| uch_J : UN -| uch_K : UN -| uch_L : UN -| uch_M : UN -| uch_N : UN -| uch_O : UN -| uch_P : UN -| uch_Q : UN -| uch_R : UN -| uch_S : UN -| uch_T : UN -| uch_U : UN -| uch_V : UN -| uch_W : UN -| uch_X : UN -| uch_Y : UN -| uch_Z : UN -| uch_a : UN -| uch_b : UN -| uch_c : UN -| uch_d : UN -| uch_e : UN -| uch_f : UN -| uch_g : UN -| uch_h : UN -| uch_i : UN -| uch_j : UN -| uch_k : UN -| uch_l : UN -| uch_m : UN -| uch_n : UN -| uch_o : UN -| uch_p : UN -| uch_q : UN -| uch_r : UN -| uch_s : UN -| uch_t : UN -| uch_u : UN -| uch_v : UN -| uch_w : UN -| uch_x : UN -| uch_y : UN -| 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 -. - -(* funzione di uguaglianza sugli atomi *) -ndefinition eq_UN ≝ -λu1,u2.match u1 with - [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ] - | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ] - | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ] - | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ] - - | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ] - | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ] - | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ] - | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ] - | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ] - | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ] - | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ] - | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ] - - | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ] - | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ] - | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ] - | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ] - | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ] - | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ] - | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ] - | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ] - | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ] - | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ] - | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ] - | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ] - | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ] - | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ] - | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ] - | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ] - - | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ] - | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ] - | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ] - | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ] - | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ] - | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ] - | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ] - | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ] - | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ] - | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ] - | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ] - | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ] - | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ] - | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ] - | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ] - | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ] - | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ] - | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ] - | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ] - | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ] - | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ] - | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ] - | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ] - | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ] - | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ] - | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ] - | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ] - | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ] - | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ] - | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ] - | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ] - | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ] - - | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ] - | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ] - | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ] - | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ] - | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ] - | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ] - | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ] - | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ] - | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ] - | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ] - | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ] - | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ] - | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ] - | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ] - | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ] - | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ] - | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ] - | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ] - | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ] - | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ] - | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ] - | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ] - | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ] - | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ] - | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ] - | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ] - | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ] - | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ] - | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ] - | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ] - | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ] - | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ] - | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ] - | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ] - | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ] - | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ] - | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ] - | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ] - | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ] - | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ] - | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ] - | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ] - | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ] - | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ] - | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ] - | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ] - | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ] - | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ] - | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ] - | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ] - | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ] - | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ] - | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ] - | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ] - | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ] - | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ] - | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ] - | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ] - | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ] - | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ] - | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ] - | 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 ] - - ]. - -(* costruttore di un sottouniverso: - S_EL cioe' uno qualsiasi degli elementi del sottouniverso - S_KO cioe' il caso impossibile -*) -ninductive S_UN (l:list UN) : Type ≝ - S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l -| S_KO : False → S_UN l. - -ndefinition getelem : ∀l.∀e:S_UN l.UN. - #l; #s; nelim s; - ##[ ##1: #u; #dim1; #dim2; napply u - ##| ##2: #F; nelim F - ##] -nqed. - -ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y). - -ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true. - #l; #s; nelim s; - ##[ ##2: #F; nelim F - ##| ##1: #u; #dim1; #dim2; napply dim1 - ##] -nqed. - -ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y). - #l; #s; nelim s; - ##[ ##2: #F; nelim F - ##| ##1: #u; #dim1; #dim2; napply dim2 - ##] -nqed. - -nlemma SUN_destruct_1 - : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2. - #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H; - nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]); - nrewrite < H; - nnormalize; - napply refl_eq. -nqed. - -ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P | false ⇒ P ]. - #x; #y; #P; #H; - nrewrite > H; - nelim y; - nnormalize; - napply (λx.x). -nqed. - -ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ]. - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; #P; - nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ])); - #H; napply (UN_destruct u1 u2); - napply (SUN_destruct_1 l … H) - ##] - ##] -nqed. - -nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true. - #e1; #e2; #H; - nrewrite > H; - nelim e2; - nnormalize; - napply refl_eq. -nqed. - -nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true. - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; - nchange with (? → eq_UN u1 u2 = true); - #H; napply (eq_to_eqUN u1 u2); - napply (SUN_destruct_1 l … H) - ##] - ##] -nqed. - -nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2. - #e1; #e2; #H; - napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …); - ##[ ##1: napply (eq_to_eqUN e1 e2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y. - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; - nchange with ((eq_UN u1 u2 = false) → ?); - #H; nnormalize; #H1; - napply (neqUN_to_neq u1 u2 H); - napply (SUN_destruct_1 l … H1) - ##] - ##] -nqed. - -naxiom SUN_construct - : ∀l.∀u. - ∀dim11,dim21:(member_list UN u eq_UN l = true). - ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)). - ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)). - -nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y. - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; - nchange with (u1 = u2 → ?); #H; - nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12; - napply (SUN_construct l u2 dim11 dim21 dim12 dim22); - ##] - ##] -nqed. - -nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y). - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; #H; - napply (not_to_not ((getelem l ?) = (getelem l ?)) - ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?); - ##[ ##1: napply H - ##| ##2: napply (eqgetelem_to_eq l …) - ##] - ##] - ##] -nqed. - -nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y. - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; - nchange with ((eq_UN u1 u2 = true) → ?); #H; - nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H)); - napply refl_eq - ##] - ##] -nqed. - -nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false. - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; #H; - napply neqtrue_to_eqfalse; - napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ; - napply H - ##] - ##] -nqed. - -nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y). - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; nnormalize; - napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)))); - ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H)) - ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H)) - ##] -nqed. - -nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l). - #l; #x; nelim x; - ##[ ##2: #F; nelim F - ##| ##1: #u1; #dim11; #dim12; #y; nelim y; - ##[ ##2: #F; nelim F - ##| ##1: #u2; #dim21; #dim22; - napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H); - napply (symmetric_eq ? (eq_SUN l ??) false); - 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 …)). -*) 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/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma new file mode 100755 index 000000000..2d84b78e5 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma @@ -0,0 +1,683 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "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 + [ nil ⇒ true + | cons h t ⇒ match f elem h with + [ true ⇒ false | false ⇒ nmember_list T elem f t ] + ]. + +(* elem presente una ed una sola volta in l *) +nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝ + match l with + [ nil ⇒ false + | cons h t ⇒ match f elem h with + [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ] + ]. + +(* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *) +ninductive UN : Type ≝ +(* quaternari[4] 1-4 *) + uq0 : UN +| uq1 : UN +| uq2 : UN +| uq3 : UN + +(* ottali[8] 5-12 *) +| uo0 : UN +| uo1 : UN +| uo2 : UN +| uo3 : UN +| uo4 : UN +| uo5 : UN +| uo6 : UN +| uo7 : UN + +(* esadecimali[16] 13-28 *) +| ux0 : UN +| ux1 : UN +| ux2 : UN +| ux3 : UN +| ux4 : UN +| ux5 : UN +| ux6 : UN +| ux7 : UN +| ux8 : UN +| ux9 : UN +| uxA : UN +| uxB : UN +| uxC : UN +| uxD : UN +| uxE : UN +| uxF : UN + +(* bitrigesimali[32] 29-60 *) +| ut00 : UN +| ut01 : UN +| ut02 : UN +| ut03 : UN +| ut04 : UN +| ut05 : UN +| ut06 : UN +| ut07 : UN +| ut08 : UN +| ut09 : UN +| ut0A : UN +| ut0B : UN +| ut0C : UN +| ut0D : UN +| ut0E : UN +| ut0F : UN +| ut10 : UN +| ut11 : UN +| ut12 : UN +| ut13 : UN +| ut14 : UN +| ut15 : UN +| ut16 : UN +| ut17 : UN +| ut18 : UN +| ut19 : UN +| ut1A : UN +| ut1B : UN +| ut1C : UN +| ut1D : UN +| ut1E : UN +| ut1F : UN + +(* ascii[63] 61-123 *) +| uch_0 : UN +| uch_1 : UN +| uch_2 : UN +| uch_3 : UN +| uch_4 : UN +| uch_5 : UN +| uch_6 : UN +| uch_7 : UN +| uch_8 : UN +| uch_9 : UN +| uch__ : UN +| uch_A : UN +| uch_B : UN +| uch_C : UN +| uch_D : UN +| uch_E : UN +| uch_F : UN +| uch_G : UN +| uch_H : UN +| uch_I : UN +| uch_J : UN +| uch_K : UN +| uch_L : UN +| uch_M : UN +| uch_N : UN +| uch_O : UN +| uch_P : UN +| uch_Q : UN +| uch_R : UN +| uch_S : UN +| uch_T : UN +| uch_U : UN +| uch_V : UN +| uch_W : UN +| uch_X : UN +| uch_Y : UN +| uch_Z : UN +| uch_a : UN +| uch_b : UN +| uch_c : UN +| uch_d : UN +| uch_e : UN +| uch_f : UN +| uch_g : UN +| uch_h : UN +| uch_i : UN +| uch_j : UN +| uch_k : UN +| uch_l : UN +| uch_m : UN +| uch_n : UN +| uch_o : UN +| uch_p : UN +| uch_q : UN +| uch_r : UN +| uch_s : UN +| uch_t : UN +| uch_u : UN +| uch_v : UN +| uch_w : UN +| uch_x : UN +| uch_y : UN +| uch_z : UN + +(* opcode[91] 124-214 *) +| 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 *) +ndefinition eq_UN ≝ +λu1,u2.match u1 with + [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ] + | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ] + | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ] + | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ] + + | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ] + | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ] + | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ] + | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ] + | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ] + | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ] + | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ] + | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ] + + | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ] + | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ] + | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ] + | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ] + | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ] + | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ] + | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ] + | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ] + | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ] + | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ] + | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ] + | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ] + | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ] + | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ] + | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ] + | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ] + + | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ] + | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ] + | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ] + | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ] + | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ] + | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ] + | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ] + | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ] + | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ] + | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ] + | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ] + | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ] + | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ] + | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ] + | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ] + | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ] + | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ] + | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ] + | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ] + | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ] + | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ] + | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ] + | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ] + | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ] + | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ] + | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ] + | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ] + | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ] + | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ] + | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ] + | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ] + | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ] + + | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ] + | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ] + | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ] + | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ] + | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ] + | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ] + | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ] + | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ] + | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ] + | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ] + | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ] + | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ] + | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ] + | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ] + | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ] + | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ] + | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ] + | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ] + | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ] + | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ] + | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ] + | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ] + | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ] + | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ] + | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ] + | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ] + | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ] + | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ] + | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ] + | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ] + | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ] + | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ] + | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ] + | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ] + | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ] + | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ] + | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ] + | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ] + | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ] + | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ] + | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ] + | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ] + | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ] + | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ] + | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ] + | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ] + | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ] + | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ] + | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ] + | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ] + | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ] + | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ] + | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ] + | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ] + | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ] + | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ] + | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ] + | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ] + | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ] + | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ] + | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ] + | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ] + | uch_z ⇒ match u2 with [ uch_z ⇒ 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 ] + + ]. + +(* costruttore di un sottouniverso: + S_EL cioe' uno qualsiasi degli elementi del sottouniverso + S_KO cioe' il caso impossibile +*) +ninductive S_UN (l:list UN) : Type ≝ + S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l +| S_KO : False → S_UN l. + +ndefinition getelem : ∀l.∀e:S_UN l.UN. + #l; #s; nelim s; + ##[ ##1: #u; #dim1; #dim2; napply u + ##| ##2: #F; nelim F + ##] +nqed. + +ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y). + +ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true. + #l; #s; nelim s; + ##[ ##2: #F; nelim F + ##| ##1: #u; #dim1; #dim2; napply dim1 + ##] +nqed. + +ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y). + #l; #s; nelim s; + ##[ ##2: #F; nelim F + ##| ##1: #u; #dim1; #dim2; napply dim2 + ##] +nqed. + +nlemma SUN_destruct_1 + : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2. + #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H; + nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P | false ⇒ P ]. + #x; #y; #P; #H; + nrewrite > H; + nelim y; + nnormalize; + napply (λx.x). +nqed. + +ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ]. + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; #P; + nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ])); + #H; napply (UN_destruct u1 u2); + napply (SUN_destruct_1 l … H) + ##] + ##] +nqed. + +nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true. + #e1; #e2; #H; + nrewrite > H; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true. + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; + nchange with (? → eq_UN u1 u2 = true); + #H; napply (eq_to_eqUN u1 u2); + napply (SUN_destruct_1 l … H) + ##] + ##] +nqed. + +nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2. + #e1; #e2; #H; + napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …); + ##[ ##1: napply (eq_to_eqUN e1 e2) + ##| ##2: napply (eqfalse_to_neqtrue … H) + ##] +nqed. + +nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y. + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; + nchange with ((eq_UN u1 u2 = false) → ?); + #H; nnormalize; #H1; + napply (neqUN_to_neq u1 u2 H); + napply (SUN_destruct_1 l … H1) + ##] + ##] +nqed. + +naxiom SUN_construct + : ∀l.∀u. + ∀dim11,dim21:(member_list UN u eq_UN l = true). + ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)). + ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)). + +nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y. + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; + nchange with (u1 = u2 → ?); #H; + nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12; + napply (SUN_construct l u2 dim11 dim21 dim12 dim22); + ##] + ##] +nqed. + +nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y). + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; #H; + napply (not_to_not ((getelem l ?) = (getelem l ?)) + ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?); + ##[ ##1: napply H + ##| ##2: napply (eqgetelem_to_eq l …) + ##] + ##] + ##] +nqed. + +nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y. + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; + nchange with ((eq_UN u1 u2 = true) → ?); #H; + nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H)); + napply refl_eq + ##] + ##] +nqed. + +nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false. + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; #H; + napply neqtrue_to_eqfalse; + napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ; + napply H + ##] + ##] +nqed. + +nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y). + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; nnormalize; + napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)))); + ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H)) + ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H)) + ##] +nqed. + +nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l). + #l; #x; nelim x; + ##[ ##2: #F; nelim F + ##| ##1: #u1; #dim11; #dim12; #y; nelim y; + ##[ ##2: #F; nelim F + ##| ##1: #u2; #dim21; #dim22; + napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H); + napply (symmetric_eq ? (eq_SUN l ??) false); + napply (neq_to_neqSUN l … (symmetric_neq … H)) + ##] +nqed.