--- /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: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* Questo materiale fa parte della tesi: *)
+(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
+(* *)
+(* data ultima modifica 15/11/2007 *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/opcode_base.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+ndefinition opcode_destruct1 : Πop2.ΠP:Prop.ADC = op2 → match op2 with [ ADC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##1: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ADC with [ ADC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct2 : Πop2.ΠP:Prop.ADD = op2 → match op2 with [ ADD ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##2: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ADD with [ ADD ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct3 : Πop2.ΠP:Prop.AIS = op2 → match op2 with [ AIS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##3: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match AIS with [ AIS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct4 : Πop2.ΠP:Prop.AIX = op2 → match op2 with [ AIX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##4: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match AIX with [ AIX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct5 : Πop2.ΠP:Prop.AND = op2 → match op2 with [ AND ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##5: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match AND with [ AND ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct6 : Πop2.ΠP:Prop.ASL = op2 → match op2 with [ ASL ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##6: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ASL with [ ASL ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct7 : Πop2.ΠP:Prop.ASR = op2 → match op2 with [ ASR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##7: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ASR with [ ASR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct8 : Πop2.ΠP:Prop.BCC = op2 → match op2 with [ BCC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##8: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BCC with [ BCC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct9 : Πop2.ΠP:Prop.BCLRn = op2 → match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##9: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BCLRn with [ BCLRn ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct10 : Πop2.ΠP:Prop.BCS = op2 → match op2 with [ BCS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##10: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BCS with [ BCS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct11 : Πop2.ΠP:Prop.BEQ = op2 → match op2 with [ BEQ ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##11: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BEQ with [ BEQ ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct12 : Πop2.ΠP:Prop.BGE = op2 → match op2 with [ BGE ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##12: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BGE with [ BGE ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct13 : Πop2.ΠP:Prop.BGND = op2 → match op2 with [ BGND ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##13: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BGND with [ BGND ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct14 : Πop2.ΠP:Prop.BGT = op2 → match op2 with [ BGT ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##14: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BGT with [ BGT ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct15 : Πop2.ΠP:Prop.BHCC = op2 → match op2 with [ BHCC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##15: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BHCC with [ BHCC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct16 : Πop2.ΠP:Prop.BHCS = op2 → match op2 with [ BHCS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##16: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BHCS with [ BHCS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct17 : Πop2.ΠP:Prop.BHI = op2 → match op2 with [ BHI ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##17: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BHI with [ BHI ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct18 : Πop2.ΠP:Prop.BIH = op2 → match op2 with [ BIH ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##18: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BIH with [ BIH ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct19 : Πop2.ΠP:Prop.BIL = op2 → match op2 with [ BIL ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##19: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BIL with [ BIL ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct20 : Πop2.ΠP:Prop.BIT = op2 → match op2 with [ BIT ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##20: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BIT with [ BIT ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct21 : Πop2.ΠP:Prop.BLE = op2 → match op2 with [ BLE ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##21: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BLE with [ BLE ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct22 : Πop2.ΠP:Prop.BLS = op2 → match op2 with [ BLS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##22: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BLS with [ BLS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct23 : Πop2.ΠP:Prop.BLT = op2 → match op2 with [ BLT ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##23: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BLT with [ BLT ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct24 : Πop2.ΠP:Prop.BMC = op2 → match op2 with [ BMC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##24: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BMC with [ BMC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct25 : Πop2.ΠP:Prop.BMI = op2 → match op2 with [ BMI ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##25: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BMI with [ BMI ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct26 : Πop2.ΠP:Prop.BMS = op2 → match op2 with [ BMS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##26: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BMS with [ BMS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct27 : Πop2.ΠP:Prop.BNE = op2 → match op2 with [ BNE ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##27: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BNE with [ BNE ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct28 : Πop2.ΠP:Prop.BPL = op2 → match op2 with [ BPL ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##28: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BPL with [ BPL ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct29 : Πop2.ΠP:Prop.BRA = op2 → match op2 with [ BRA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##29: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BRA with [ BRA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##30: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BRCLRn with [ BRCLRn ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct31 : Πop2.ΠP:Prop.BRN = op2 → match op2 with [ BRN ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##31: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BRN with [ BRN ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct32 : Πop2.ΠP:Prop.BRSETn = op2 → match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##32: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BRSETn with [ BRSETn ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct33 : Πop2.ΠP:Prop.BSETn = op2 → match op2 with [ BSETn ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##33: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BSETn with [ BSETn ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct34 : Πop2.ΠP:Prop.BSR = op2 → match op2 with [ BSR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##34: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match BSR with [ BSR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct35 : Πop2.ΠP:Prop.CBEQA = op2 → match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##35: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CBEQA with [ CBEQA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct36 : Πop2.ΠP:Prop.CBEQX = op2 → match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##36: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CBEQX with [ CBEQX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct37 : Πop2.ΠP:Prop.CLC = op2 → match op2 with [ CLC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##37: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CLC with [ CLC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct38 : Πop2.ΠP:Prop.CLI = op2 → match op2 with [ CLI ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##38: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CLI with [ CLI ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct39 : Πop2.ΠP:Prop.CLR = op2 → match op2 with [ CLR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##39: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CLR with [ CLR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct40 : Πop2.ΠP:Prop.CMP = op2 → match op2 with [ CMP ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##40: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CMP with [ CMP ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct41 : Πop2.ΠP:Prop.COM = op2 → match op2 with [ COM ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##41: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match COM with [ COM ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct42 : Πop2.ΠP:Prop.CPHX = op2 → match op2 with [ CPHX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##42: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CPHX with [ CPHX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct43 : Πop2.ΠP:Prop.CPX = op2 → match op2 with [ CPX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##43: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match CPX with [ CPX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct44 : Πop2.ΠP:Prop.DAA = op2 → match op2 with [ DAA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##44: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match DAA with [ DAA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct45 : Πop2.ΠP:Prop.DBNZ = op2 → match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##45: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match DBNZ with [ DBNZ ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct46 : Πop2.ΠP:Prop.DEC = op2 → match op2 with [ DEC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##46: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match DEC with [ DEC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct47 : Πop2.ΠP:Prop.DIV = op2 → match op2 with [ DIV ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##47: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match DIV with [ DIV ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct48 : Πop2.ΠP:Prop.EOR = op2 → match op2 with [ EOR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##48: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match EOR with [ EOR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct49 : Πop2.ΠP:Prop.INC = op2 → match op2 with [ INC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##49: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match INC with [ INC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct50 : Πop2.ΠP:Prop.JMP = op2 → match op2 with [ JMP ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##50: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match JMP with [ JMP ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct51 : Πop2.ΠP:Prop.JSR = op2 → match op2 with [ JSR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##51: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match JSR with [ JSR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct52 : Πop2.ΠP:Prop.LDA = op2 → match op2 with [ LDA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##52: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match LDA with [ LDA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct53 : Πop2.ΠP:Prop.LDHX = op2 → match op2 with [ LDHX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##53: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match LDHX with [ LDHX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct54 : Πop2.ΠP:Prop.LDX = op2 → match op2 with [ LDX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##54: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match LDX with [ LDX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct55 : Πop2.ΠP:Prop.LSR = op2 → match op2 with [ LSR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##55: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match LSR with [ LSR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct56 : Πop2.ΠP:Prop.MOV = op2 → match op2 with [ MOV ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##56: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match MOV with [ MOV ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct57 : Πop2.ΠP:Prop.MUL = op2 → match op2 with [ MUL ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##57: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match MUL with [ MUL ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct58 : Πop2.ΠP:Prop.NEG = op2 → match op2 with [ NEG ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##58: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match NEG with [ NEG ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct59 : Πop2.ΠP:Prop.NOP = op2 → match op2 with [ NOP ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##59: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match NOP with [ NOP ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct60 : Πop2.ΠP:Prop.NSA = op2 → match op2 with [ NSA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##60: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match NSA with [ NSA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct61 : Πop2.ΠP:Prop.ORA = op2 → match op2 with [ ORA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##61: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ORA with [ ORA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct62 : Πop2.ΠP:Prop.PSHA = op2 → match op2 with [ PSHA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##62: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match PSHA with [ PSHA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct63 : Πop2.ΠP:Prop.PSHH = op2 → match op2 with [ PSHH ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##63: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match PSHH with [ PSHH ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct64 : Πop2.ΠP:Prop.PSHX = op2 → match op2 with [ PSHX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##64: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match PSHX with [ PSHX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct65 : Πop2.ΠP:Prop.PULA = op2 → match op2 with [ PULA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##65: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match PULA with [ PULA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct66 : Πop2.ΠP:Prop.PULH = op2 → match op2 with [ PULH ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##66: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match PULH with [ PULH ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct67 : Πop2.ΠP:Prop.PULX = op2 → match op2 with [ PULX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##67: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match PULX with [ PULX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct68 : Πop2.ΠP:Prop.ROL = op2 → match op2 with [ ROL ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##68: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ROL with [ ROL ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct69 : Πop2.ΠP:Prop.ROR = op2 → match op2 with [ ROR ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##69: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match ROR with [ ROR ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct70 : Πop2.ΠP:Prop.RSP = op2 → match op2 with [ RSP ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##70: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match RSP with [ RSP ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct71 : Πop2.ΠP:Prop.RTI = op2 → match op2 with [ RTI ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##71: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match RTI with [ RTI ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct72 : Πop2.ΠP:Prop.RTS = op2 → match op2 with [ RTS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##72: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match RTS with [ RTS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct73 : Πop2.ΠP:Prop.SBC = op2 → match op2 with [ SBC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##73: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SBC with [ SBC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct74 : Πop2.ΠP:Prop.SEC = op2 → match op2 with [ SEC ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##74: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SEC with [ SEC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct75 : Πop2.ΠP:Prop.SEI = op2 → match op2 with [ SEI ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##75: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SEI with [ SEI ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct76 : Πop2.ΠP:Prop.SHA = op2 → match op2 with [ SHA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##76: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SHA with [ SHA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct77 : Πop2.ΠP:Prop.SLA = op2 → match op2 with [ SLA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##77: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SLA with [ SLA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct78 : Πop2.ΠP:Prop.STA = op2 → match op2 with [ STA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##78: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match STA with [ STA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct79 : Πop2.ΠP:Prop.STHX = op2 → match op2 with [ STHX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##79: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match STHX with [ STHX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct80 : Πop2.ΠP:Prop.STOP = op2 → match op2 with [ STOP ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##80: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match STOP with [ STOP ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct81 : Πop2.ΠP:Prop.STX = op2 → match op2 with [ STX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##81: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match STX with [ STX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct82 : Πop2.ΠP:Prop.SUB = op2 → match op2 with [ SUB ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##82: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SUB with [ SUB ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct83 : Πop2.ΠP:Prop.SWI = op2 → match op2 with [ SWI ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##83: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match SWI with [ SWI ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct84 : Πop2.ΠP:Prop.TAP = op2 → match op2 with [ TAP ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##84: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TAP with [ TAP ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct85 : Πop2.ΠP:Prop.TAX = op2 → match op2 with [ TAX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##85: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TAX with [ TAX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct86 : Πop2.ΠP:Prop.TPA = op2 → match op2 with [ TPA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##86: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TPA with [ TPA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct87 : Πop2.ΠP:Prop.TST = op2 → match op2 with [ TST ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##87: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TST with [ TST ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct88 : Πop2.ΠP:Prop.TSX = op2 → match op2 with [ TSX ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##88: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TSX with [ TSX ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct89 : Πop2.ΠP:Prop.TXA = op2 → match op2 with [ TXA ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##89: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TXA with [ TXA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct90 : Πop2.ΠP:Prop.TXS = op2 → match op2 with [ TXS ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##90: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match TXS with [ TXS ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct91 : Πop2.ΠP:Prop.WAIT = op2 → match op2 with [ WAIT ⇒ P → P | _ ⇒ P ].
+ #op2; #P; ncases op2; nnormalize;
+ ##[ ##91: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind ??);
+ nchange with (match WAIT with [ WAIT ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition opcode_destruct_aux ≝
+Πop1,op2.ΠP:Prop.op1 = op2 →
+ match op1 with
+ [ ADC ⇒ match op2 with [ ADC ⇒ P → P | _ ⇒ P ]
+ | ADD ⇒ match op2 with [ ADD ⇒ P → P | _ ⇒ P ]
+ | AIS ⇒ match op2 with [ AIS ⇒ P → P | _ ⇒ P ]
+ | AIX ⇒ match op2 with [ AIX ⇒ P → P | _ ⇒ P ]
+ | AND ⇒ match op2 with [ AND ⇒ P → P | _ ⇒ P ]
+ | ASL ⇒ match op2 with [ ASL ⇒ P → P | _ ⇒ P ]
+ | ASR ⇒ match op2 with [ ASR ⇒ P → P | _ ⇒ P ]
+ | BCC ⇒ match op2 with [ BCC ⇒ P → P | _ ⇒ P ]
+ | BCLRn ⇒ match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ]
+ | BCS ⇒ match op2 with [ BCS ⇒ P → P | _ ⇒ P ]
+ | BEQ ⇒ match op2 with [ BEQ ⇒ P → P | _ ⇒ P ]
+ | BGE ⇒ match op2 with [ BGE ⇒ P → P | _ ⇒ P ]
+ | BGND ⇒ match op2 with [ BGND ⇒ P → P | _ ⇒ P ]
+ | BGT ⇒ match op2 with [ BGT ⇒ P → P | _ ⇒ P ]
+ | BHCC ⇒ match op2 with [ BHCC ⇒ P → P | _ ⇒ P ]
+ | BHCS ⇒ match op2 with [ BHCS ⇒ P → P | _ ⇒ P ]
+ | BHI ⇒ match op2 with [ BHI ⇒ P → P | _ ⇒ P ]
+ | BIH ⇒ match op2 with [ BIH ⇒ P → P | _ ⇒ P ]
+ | BIL ⇒ match op2 with [ BIL ⇒ P → P | _ ⇒ P ]
+ | BIT ⇒ match op2 with [ BIT ⇒ P → P | _ ⇒ P ]
+ | BLE ⇒ match op2 with [ BLE ⇒ P → P | _ ⇒ P ]
+ | BLS ⇒ match op2 with [ BLS ⇒ P → P | _ ⇒ P ]
+ | BLT ⇒ match op2 with [ BLT ⇒ P → P | _ ⇒ P ]
+ | BMC ⇒ match op2 with [ BMC ⇒ P → P | _ ⇒ P ]
+ | BMI ⇒ match op2 with [ BMI ⇒ P → P | _ ⇒ P ]
+ | BMS ⇒ match op2 with [ BMS ⇒ P → P | _ ⇒ P ]
+ | BNE ⇒ match op2 with [ BNE ⇒ P → P | _ ⇒ P ]
+ | BPL ⇒ match op2 with [ BPL ⇒ P → P | _ ⇒ P ]
+ | BRA ⇒ match op2 with [ BRA ⇒ P → P | _ ⇒ P ]
+ | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ]
+ | BRN ⇒ match op2 with [ BRN ⇒ P → P | _ ⇒ P ]
+ | BRSETn ⇒ match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ]
+ | BSETn ⇒ match op2 with [ BSETn ⇒ P → P | _ ⇒ P ]
+ | BSR ⇒ match op2 with [ BSR ⇒ P → P | _ ⇒ P ]
+ | CBEQA ⇒ match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ]
+ | CBEQX ⇒ match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ]
+ | CLC ⇒ match op2 with [ CLC ⇒ P → P | _ ⇒ P ]
+ | CLI ⇒ match op2 with [ CLI ⇒ P → P | _ ⇒ P ]
+ | CLR ⇒ match op2 with [ CLR ⇒ P → P | _ ⇒ P ]
+ | CMP ⇒ match op2 with [ CMP ⇒ P → P | _ ⇒ P ]
+ | COM ⇒ match op2 with [ COM ⇒ P → P | _ ⇒ P ]
+ | CPHX ⇒ match op2 with [ CPHX ⇒ P → P | _ ⇒ P ]
+ | CPX ⇒ match op2 with [ CPX ⇒ P → P | _ ⇒ P ]
+ | DAA ⇒ match op2 with [ DAA ⇒ P → P | _ ⇒ P ]
+ | DBNZ ⇒ match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ]
+ | DEC ⇒ match op2 with [ DEC ⇒ P → P | _ ⇒ P ]
+ | DIV ⇒ match op2 with [ DIV ⇒ P → P | _ ⇒ P ]
+ | EOR ⇒ match op2 with [ EOR ⇒ P → P | _ ⇒ P ]
+ | INC ⇒ match op2 with [ INC ⇒ P → P | _ ⇒ P ]
+ | JMP ⇒ match op2 with [ JMP ⇒ P → P | _ ⇒ P ]
+ | JSR ⇒ match op2 with [ JSR ⇒ P → P | _ ⇒ P ]
+ | LDA ⇒ match op2 with [ LDA ⇒ P → P | _ ⇒ P ]
+ | LDHX ⇒ match op2 with [ LDHX ⇒ P → P | _ ⇒ P ]
+ | LDX ⇒ match op2 with [ LDX ⇒ P → P | _ ⇒ P ]
+ | LSR ⇒ match op2 with [ LSR ⇒ P → P | _ ⇒ P ]
+ | MOV ⇒ match op2 with [ MOV ⇒ P → P | _ ⇒ P ]
+ | MUL ⇒ match op2 with [ MUL ⇒ P → P | _ ⇒ P ]
+ | NEG ⇒ match op2 with [ NEG ⇒ P → P | _ ⇒ P ]
+ | NOP ⇒ match op2 with [ NOP ⇒ P → P | _ ⇒ P ]
+ | NSA ⇒ match op2 with [ NSA ⇒ P → P | _ ⇒ P ]
+ | ORA ⇒ match op2 with [ ORA ⇒ P → P | _ ⇒ P ]
+ | PSHA ⇒ match op2 with [ PSHA ⇒ P → P | _ ⇒ P ]
+ | PSHH ⇒ match op2 with [ PSHH ⇒ P → P | _ ⇒ P ]
+ | PSHX ⇒ match op2 with [ PSHX ⇒ P → P | _ ⇒ P ]
+ | PULA ⇒ match op2 with [ PULA ⇒ P → P | _ ⇒ P ]
+ | PULH ⇒ match op2 with [ PULH ⇒ P → P | _ ⇒ P ]
+ | PULX ⇒ match op2 with [ PULX ⇒ P → P | _ ⇒ P ]
+ | ROL ⇒ match op2 with [ ROL ⇒ P → P | _ ⇒ P ]
+ | ROR ⇒ match op2 with [ ROR ⇒ P → P | _ ⇒ P ]
+ | RSP ⇒ match op2 with [ RSP ⇒ P → P | _ ⇒ P ]
+ | RTI ⇒ match op2 with [ RTI ⇒ P → P | _ ⇒ P ]
+ | RTS ⇒ match op2 with [ RTS ⇒ P → P | _ ⇒ P ]
+ | SBC ⇒ match op2 with [ SBC ⇒ P → P | _ ⇒ P ]
+ | SEC ⇒ match op2 with [ SEC ⇒ P → P | _ ⇒ P ]
+ | SEI ⇒ match op2 with [ SEI ⇒ P → P | _ ⇒ P ]
+ | SHA ⇒ match op2 with [ SHA ⇒ P → P | _ ⇒ P ]
+ | SLA ⇒ match op2 with [ SLA ⇒ P → P | _ ⇒ P ]
+ | STA ⇒ match op2 with [ STA ⇒ P → P | _ ⇒ P ]
+ | STHX ⇒ match op2 with [ STHX ⇒ P → P | _ ⇒ P ]
+ | STOP ⇒ match op2 with [ STOP ⇒ P → P | _ ⇒ P ]
+ | STX ⇒ match op2 with [ STX ⇒ P → P | _ ⇒ P ]
+ | SUB ⇒ match op2 with [ SUB ⇒ P → P | _ ⇒ P ]
+ | SWI ⇒ match op2 with [ SWI ⇒ P → P | _ ⇒ P ]
+ | TAP ⇒ match op2 with [ TAP ⇒ P → P | _ ⇒ P ]
+ | TAX ⇒ match op2 with [ TAX ⇒ P → P | _ ⇒ P ]
+ | TPA ⇒ match op2 with [ TPA ⇒ P → P | _ ⇒ P ]
+ | TST ⇒ match op2 with [ TST ⇒ P → P | _ ⇒ P ]
+ | TSX ⇒ match op2 with [ TSX ⇒ P → P | _ ⇒ P ]
+ | TXA ⇒ match op2 with [ TXA ⇒ P → P | _ ⇒ P ]
+ | TXS ⇒ match op2 with [ TXS ⇒ P → P | _ ⇒ P ]
+ | WAIT ⇒ match op2 with [ WAIT ⇒ P → P | _ ⇒ P ]
+ ].
+
+ndefinition opcode_destruct : opcode_destruct_aux.
+ #op1; ncases op1;
+ ##[ ##1: napply opcode_destruct1 ##| ##2: napply opcode_destruct2 ##| ##3: napply opcode_destruct3 ##| ##4: napply opcode_destruct4
+ ##| ##5: napply opcode_destruct5 ##| ##6: napply opcode_destruct6 ##| ##7: napply opcode_destruct7 ##| ##8: napply opcode_destruct8
+ ##| ##9: napply opcode_destruct9 ##| ##10: napply opcode_destruct10 ##| ##11: napply opcode_destruct11 ##| ##12: napply opcode_destruct12
+ ##| ##13: napply opcode_destruct13 ##| ##14: napply opcode_destruct14 ##| ##15: napply opcode_destruct15 ##| ##16: napply opcode_destruct16
+ ##| ##17: napply opcode_destruct17 ##| ##18: napply opcode_destruct18 ##| ##19: napply opcode_destruct19 ##| ##20: napply opcode_destruct20
+ ##| ##21: napply opcode_destruct21 ##| ##22: napply opcode_destruct22 ##| ##23: napply opcode_destruct23 ##| ##24: napply opcode_destruct24
+ ##| ##25: napply opcode_destruct25 ##| ##26: napply opcode_destruct26 ##| ##27: napply opcode_destruct27 ##| ##28: napply opcode_destruct28
+ ##| ##29: napply opcode_destruct29 ##| ##30: napply opcode_destruct30 ##| ##31: napply opcode_destruct31 ##| ##32: napply opcode_destruct32
+ ##| ##33: napply opcode_destruct33 ##| ##34: napply opcode_destruct34 ##| ##35: napply opcode_destruct35 ##| ##36: napply opcode_destruct36
+ ##| ##37: napply opcode_destruct37 ##| ##38: napply opcode_destruct38 ##| ##39: napply opcode_destruct39 ##| ##40: napply opcode_destruct40
+ ##| ##41: napply opcode_destruct41 ##| ##42: napply opcode_destruct42 ##| ##43: napply opcode_destruct43 ##| ##44: napply opcode_destruct44
+ ##| ##45: napply opcode_destruct45 ##| ##46: napply opcode_destruct46 ##| ##47: napply opcode_destruct47 ##| ##48: napply opcode_destruct48
+ ##| ##49: napply opcode_destruct49 ##| ##50: napply opcode_destruct50 ##| ##51: napply opcode_destruct51 ##| ##52: napply opcode_destruct52
+ ##| ##53: napply opcode_destruct53 ##| ##54: napply opcode_destruct54 ##| ##55: napply opcode_destruct55 ##| ##56: napply opcode_destruct56
+ ##| ##57: napply opcode_destruct57 ##| ##58: napply opcode_destruct58 ##| ##59: napply opcode_destruct59 ##| ##60: napply opcode_destruct60
+ ##| ##61: napply opcode_destruct61 ##| ##62: napply opcode_destruct62 ##| ##63: napply opcode_destruct63 ##| ##64: napply opcode_destruct64
+ ##| ##65: napply opcode_destruct65 ##| ##66: napply opcode_destruct66 ##| ##67: napply opcode_destruct67 ##| ##68: napply opcode_destruct68
+ ##| ##69: napply opcode_destruct69 ##| ##70: napply opcode_destruct70 ##| ##71: napply opcode_destruct71 ##| ##72: napply opcode_destruct72
+ ##| ##73: napply opcode_destruct73 ##| ##74: napply opcode_destruct74 ##| ##75: napply opcode_destruct75 ##| ##76: napply opcode_destruct76
+ ##| ##77: napply opcode_destruct77 ##| ##78: napply opcode_destruct78 ##| ##79: napply opcode_destruct79 ##| ##80: napply opcode_destruct80
+ ##| ##81: napply opcode_destruct81 ##| ##82: napply opcode_destruct82 ##| ##83: napply opcode_destruct83 ##| ##84: napply opcode_destruct84
+ ##| ##85: napply opcode_destruct85 ##| ##86: napply opcode_destruct86 ##| ##87: napply opcode_destruct87 ##| ##88: napply opcode_destruct88
+ ##| ##89: napply opcode_destruct89 ##| ##90: napply opcode_destruct90 ##| ##91: napply opcode_destruct91 ##]
+nqed.
projects / helm.git / blobdiff