(* 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 *)
| 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 ]
| 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 ]
| 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 ].
(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 ]);
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;
##[ ##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:
projects / helm.git / blobdiff