-(* 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 ]
-
- ].
-