X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fmeta_type.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fmeta_type.ma;h=751a4bb56cca5537a9523a56abd77043bf3bc474;hb=9dc61a4f11210bccf34f63f48968afca4261c1b4;hp=1574f46ca947ebbab785ce13a8db1dd4e0b66eac;hpb=fc1e871dde0f9f4cfde6f4a4fda8d18022584e65;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma b/helm/software/matita/contribs/ng_assembly/common/meta_type.ma
index 1574f46ca..751a4bb56 100755
--- a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/meta_type.ma
@@ -39,10 +39,231 @@ nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
 
 (* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
 ninductive UN : Type ≝
-  uq0 : UN | uq1 : UN | uq2 : UN | uq3 : UN
-| uo0 : UN | uo1 : UN | uo2 : UN | uo3 : UN | uo4 : UN | uo5 : UN | uo6 : UN | uo7 : UN
-| 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
+(* 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 *)
@@ -52,6 +273,7 @@ ndefinition eq_UN ≝
  | 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 ]
@@ -60,6 +282,7 @@ ndefinition eq_UN ≝
  | 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 ]
@@ -76,16 +299,408 @@ ndefinition eq_UN ≝
  | 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 ]
+
  ].
 
+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.
+
+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 pippo : ∀A,B:Prop.(A → B) → ((¬B) → (¬A)).
+ #A; #B; #H; nnormalize;
+ #H1; #H2;
+ napply (H1 (H H2)).
+nqed.
+
+nlemma pluto1 : ∀x.x = false → x ≠ true.
+ #x; nelim x;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##]
+nqed.
+
+nlemma pluto2 : ∀x.x = true → x ≠ false.
+ #x; nelim x;
+ ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##| ##2: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma pluto3 : ∀x.x ≠ false → x = true.
+ #x; nelim x;
+ ##[ ##1: #H; napply refl_eq
+ ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
+ ##]
+nqed.
+
+nlemma pluto4 : ∀x.x ≠ true → x = false.
+ #x; nelim x;
+ ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
+ ##| ##2: #H; napply refl_eq
+ ##]
+nqed.
+
+nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
+ #e1; #e2; #H;
+ napply (pippo (e1 = e2) (eq_UN e1 e2 = true) …);
+ ##[ ##1: napply (eq_to_eqUN e1 e2)
+ ##| ##2: napply (pluto1 … H)
+ ##]
+nqed.
+
+naxiom eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
+
+nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
+ #e1; #e2; #H;
+ napply (pluto4 (eq_UN e1 e2));
+ napply (pippo (eq_UN e1 e2 = true) (e1 = e2) ? H);
+ napply (eqUN_to_eq e1 e2).
+nqed.
+
+nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_UN x y = true) (eq_UN x y = false) ?);
+ ##[ ##1: ncases (eq_UN x y);
+          ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
+          ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+          ##]
+ ##| ##2: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqUN_to_eq … H))
+ ##| ##3: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqUN_to_neq … H))
+ ##]
+nqed.
+
+ nrewrite > (eq_to_eqUN e1 e2 ?);
+
+nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
+ #e1; #e2; #H;
+ 
+
+nlemma pippo : ∀P.(¬¬¬P) → (¬P).
+ #P; nnormalize; #H; #H1;
+ napply H; #H2;
+ napply (H2 H1).
+nqed.
+
+nlemma pippo2 : ∀P.(¬¬P) → P.
+ #P; nnormalize; #H;
+ napply (or2_elim (¬P) (¬¬¬¬P) ?);
+ ##[ ##1: napply (or2_intro2 ?? (prop_to_nnprop ? H))
+ ##| ##2: #H1; nelim (H H1)
+ ##| ##3: #H1; napply False_ind;
+          napply (H (pippo …));
+          nnormalize; #H2;
+          napply False_ind;
+          napply (pippo ? H1);
+          #H2;
+          napply H;
+          napply False_ind;
+          napply H1; #H2;
+        
+ ##[ ##2: #H1;napply (prop_to_nnprop ? H);
+ ##| ##1: nnormalize; #H1;
+ napply False_ind;
+ napply H; #H1;
+ napply H;
+ napply (or2_elim (¬¬P) (¬¬¬P) ?);
+ ##[ ##1: napply (or2_intro1 ?? H);
+ 
+ napply (absurd (¬¬¬P) P ??);
+ ##[ ##2: napply (prop_to_nnprop ? H);
+ ##| ##1:
+ napply (pippo P);
+ nnormalize;
+ nnormalize in H:(%);
+ #H1;
+ #H1;
+ napply (absurd ? False H ?);
+ nnormalize;
+ #H2;
+ nnormalize; #H;
+ napply False_ind;
+ napply H; #H1;
+ napply (absurd ? False (prop_to_nnprop (¬P) ?));
+ ##[ ##1: nnormalize; #H2; napply (H2 H)
+ ##| ##2:
+ nnormalize; #H2;
+ nnormalize in K:(%);
+ # .
+nqed.
+
+nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
+ #e1; #e2;
+ napply (or2_elim (eq_UN e1 e2 = false) (e1 ≠ e2) ?);
+ ##[ ##3:
+ nelim e1;
+ nnormalize;
+ nchange with (match e2 with [ ? ⇒ true | _ ⇒ false ]);
+ nelim e2;
+ #H;
+ napply (or2_elim (e1 = e2) (e1 ≠ e2) …);
+ ##[ ##2:
+ 
+ ##[ ##1: ncases (eq_UN e1 e2);
+          ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
+          ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+          ##]
+ ##| ##3: 
+
+
+ nnormalize;
+ nrewrite > H;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+ndefinition decidable_UN1 ≝ λx.∀y:UN.decidable (x = y).
+ #x;
+ nnormalize;
+ nelim x;
+ ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (UN_destruct … H)
+ ##]
+nqed.
+
+naxiom decidable_UN : ∀x,y:UN.decidable (x = y).
+
+nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
+ #e1; #e2; #H;
+
+nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
+ #e1; #e2; #H; napply (or2_elim ??? (decidable_UN e1 e2));
+ ##[ ##2: #H1;
+
+nlemma pippo : ∀e1,e2:UN.decidable (e1 = e2).
+ #e1; #e2; nnormalize;
+ nelim e1;
+ napply (or2_intro1 (? = ?) (? ≠ ?) …);
+ nchange with (match e2 with [ ? ⇒ refl_eq UN ? | _ ⇒ ? ]);
+ napply (destruct_UN ? e2 (? = e2) ?);
+
+nlemma pippo : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
+ #e1; nelim e1; #e2;
+
+
 (* 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 : Πe:UN.(member_list UN e eq_UN l) = true → S_UN l
+  S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → 
+               (∀y.x = y → (eq_UN x y = true)) →
+               (∀y.(eq_UN x y = true) → x = y) →
+               (∀y.decidable (x = y)) →
+               (∀y.x ≠ y → (eq_UN x y = false)) →
+               (∀y.(eq_UN x y = false) → x ≠ y) →
+               S_UN l
 | S_KO : False → S_UN l. 
 
+ndefinition SUN_create : Πl.Πe.(member_list UN e eq_UN l = true) → S_UN l.
+ #l; #e; #dim; napply (S_EL l e dim …);
+ ##[ ##1: #y; #H; nrewrite > H; nelim y; nnormalize; napply refl_eq
+ ##| ##2: #y;
+
 (* sottoinsieme degli esadecimali *)
 ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
 
@@ -140,7 +755,7 @@ ndefinition succ_EX_UN ≝
  (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 …)).
 
-(* destruct universale per accedere ai due testimoni di esistenza *)
+(* lemmi *)
 nlemma same_UN_1 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
  #l; #e1; #e2; #dim1; #dim2; #H;
  nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a | S_KO _ ⇒ False ]);
@@ -149,8 +764,9 @@ nlemma same_UN_1 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 
  napply refl_eq.
 nqed.
 
-(* destruct universale che funziona su qualsiasi sottouniverso *)
-ndefinition destruct_UN
+
+
+ndefinition destruct_SUN
  : ∀l.∀e1,e2:S_UN l.∀P:Prop.
    e1 = e2 → match eq_UN (getelem ? e1) (getelem ? e2) with [ true ⇒ P → P | false ⇒ P ].
  #l; #e1; nelim e1;
@@ -159,20 +775,88 @@ ndefinition destruct_UN
           ##[ ##2: #H; nelim H
           ##| ##1: #u2; #dim2; #P; #H;
                    nchange with (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]);
-                   nrewrite > (same_UN_1 l … H);
-                   nelim u2;
-                   nnormalize;
-                   napply (λx.x)
+                   napply (destruct_UN u1 u2 P (same_UN_1 l … H))
           ##]
  ##]
 nqed.
 
-nlemma eqUN_to_eq : ∀l.∀e1,e2:S_UN l.eq_UN (getelem ? e1) (getelem ? e2) = true → (getelem ? e1) = (getelem ? e2).
+
+
+nlemma eq_to_eqSUN
+ : ∀l.∀e1,e2:S_UN l.(getelem ? e1) = (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = true.
  #l; #e1; nelim e1;
  ##[ ##2: #H; nelim H
  ##| ##1: #u1; #dim1; #e2; ncases e2;
           ##[ ##2: #H; nelim H;
-          ##| ##1: #u2; #dim2; #H; nelim u1;
+          ##| ##1: #u2; #dim2; nchange with ((u1 = u2) → (eq_UN u1 u2 = true));
+                   napply (eq_to_eqUN u1 u2);
+          ##]
+ ##]
+nqed.
+
+nlet rec scan (T:Type) (e:T) (f:T → T → bool) (l:list T) (n:nat) on l ≝
+ match l with
+  [ nil ⇒ None ?
+  | cons h t ⇒ match f e h with
+   [ true ⇒ Some ? n
+   | false ⇒ scan T e f t (S n)
+   ]
+  ].
+
+nlemma pippo : ∀l.∀x,y:S_UN l.x = y → scan ? (getelem ? x) eq_UN l O = scan ? (getelem ? y) eq_UN l O. 
+ #l; nelim l;
+ ##[ ##1: #x; #y; #H; nnormalize; napply refl_eq
+ ##| ##2: #hh; #tt; #H; #x; nelim x;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u1; #dim1; #y; nelim y;
+                   ##[ ##2: #F; nelim F
+                   ##| ##1: #u2; #dim2; #H1;
+                            nchange with ((scan ? u1 ???) = (scan ? u2 ???));
+                            nrewrite > (same_UN_1 (hh::tt) … H1);
+                            nchange with 
+                            nletin K ≝ (same_UN_1 (hh::tt) … H1);
+                            nchange in K:(%) with (u1 = u2);
+                            nnormalize in K:(%);
+                            nrewrite > (same_UN_1 (hh::tt) … H1) in dim1:(%) dim2:(%) ⊢ %;
+                            nchange with (match eq_UN 
+                   
+                    nchange with (scan ? u1 eq_UN ? O = scan ? u2 eq_UN ? O);
+ 
+ #x; nelim x;
+ ##[ ##2: #H; nelim H
+ ##| ##1: #u1; #dim1; #y; nelim y;
+     ##[ ##2: #H; nelim H
+     ##| ##1: #u2; #dim2; #H; nchange with (scan ? u1 eq_UN l O = scan ? u2 eq_UN l O);
+              nrewrite > (same_UN_1 l … H);
+              nelim l in x:(%) dim1:(%) y:(%) dim2:(%) H:(%) ⊢ %;
+              ##[ ##1: #x; #dim1; #y; #dim2; #H; nnormalize; napply refl_eq
+              ##| ##2: #uu1; #ll; #H; #y;
+              nnormalize;
+
+nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
+ #x; nnormalize; #y;
+ napply (Or2_ind);
+ 
+ 
+  napply (destruct_UN ? y (Or2 ??) ?);
+
+nlemma neq_to_neqUN
+ : ∀l.∀e1,e2:S_UN l.(getelem ? e1) ≠ (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = false.
+ #l; #e1; nelim e1;
+ ##[ ##2: #H; nelim H
+ ##| ##1: #u1; #dim1; #e2; ncases e2;
+          ##[ ##2: #H; nelim H;
+          ##| ##1: #u2; #dim2; nchange with ((u1 ≠ u2) → (eq_UN u1 u2 = false));
+                   #H; nrewrite > H;
+                   nelim u2; nnormalize; napply refl_eq
+          ##]
+ ##]
+nqed.
+
+                   nelim u1 in dim1:(%) H:(%) ⊢ %; #dim1; #H;
+                   ##[ ##1: nelim u2 in dim2:(%) H:(%) ⊢ %; #dim2; #H;
+                            napply (destruct_UN l (S_EL l uq0 dim1) ?? H);
+                   
                    ##[ ##1: nelim u2; ##[ ##1: