-(**************************************************************************)
-(* ___ *)
-(* ||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 …)).
-*)