+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 …)).
-*)
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
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
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
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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
projects / helm.git / commitdiff