nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
ndefinition instr_mode_destruct31 :
ncases n2;
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
- ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn ?? H))
+ ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn … H))
##]
nqed.
nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
ndefinition instr_mode_destruct32 :
ncases n2;
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
- ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H))
+ ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn_and_IMM1 … H))
##]
nqed.
nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
ndefinition instr_mode_destruct33 :
ncases n2;
nnormalize;
##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
- ##| ##*: #H; napply (exadecim_destruct ??? (instr_mode_destruct_MODE_TNY ?? H))
+ ##| ##*: #H; napply (exadecim_destruct … (instr_mode_destruct_MODE_TNY … H))
##]
nqed.
nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
ndefinition instr_mode_destruct34 :
ncases n1;
##[ ##1: ncases n2; nnormalize;
##[ ##1: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##2: ncases n2; nnormalize;
##[ ##2: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##3: ncases n2; nnormalize;
##[ ##3: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##4: ncases n2; nnormalize;
##[ ##4: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##5: ncases n2; nnormalize;
##[ ##5: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##6: ncases n2; nnormalize;
##[ ##6: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##7: ncases n2; nnormalize;
##[ ##7: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##8: ncases n2; nnormalize;
##[ ##8: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##9: ncases n2; nnormalize;
##[ ##9: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##10: ncases n2; nnormalize;
##[ ##10: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##11: ncases n2; nnormalize;
##[ ##11: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##12: ncases n2; nnormalize;
##[ ##12: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##13: ncases n2; nnormalize;
##[ ##13: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##14: ncases n2; nnormalize;
##[ ##14: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##15: ncases n2; nnormalize;
##[ ##15: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##16: ncases n2; nnormalize;
##[ ##16: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##17: ncases n2; nnormalize;
##[ ##17: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##18: ncases n2; nnormalize;
##[ ##18: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##19: ncases n2; nnormalize;
##[ ##19: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##20: ncases n2; nnormalize;
##[ ##20: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##21: ncases n2; nnormalize;
##[ ##21: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##22: ncases n2; nnormalize;
##[ ##22: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##23: ncases n2; nnormalize;
##[ ##23: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##24: ncases n2; nnormalize;
##[ ##24: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##25: ncases n2; nnormalize;
##[ ##25: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##26: ncases n2; nnormalize;
##[ ##26: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##27: ncases n2; nnormalize;
##[ ##27: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##28: ncases n2; nnormalize;
##[ ##28: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##29: ncases n2; nnormalize;
##[ ##29: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##30: ncases n2; nnormalize;
##[ ##30: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##31: ncases n2; nnormalize;
##[ ##31: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##| ##32: ncases n2; nnormalize;
##[ ##32: #H; napply (λx:P.x)
- ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+ ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
##]
##]
##]