X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fopcode_base_lemmas_instrmode1.ma;h=ad383d2ab72567b38e03afbee6e8b7d285bbaff0;hb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;hp=9ef4d01b7075e28f7df0d781edaab753da20fd1b;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma index 9ef4d01b7..ad383d2ab 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma @@ -35,11 +35,11 @@ ndefinition instr_mode_destruct1 : nnormalize; ##[ ##1: #H; napply (λx:P.x) ##| ##2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -52,11 +52,11 @@ ndefinition instr_mode_destruct2 : nnormalize; ##[ ##2: #H; napply (λx:P.x) ##| ##1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -69,11 +69,11 @@ ndefinition instr_mode_destruct3 : nnormalize; ##[ ##3: #H; napply (λx:P.x) ##| ##1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -86,11 +86,11 @@ ndefinition instr_mode_destruct4 : nnormalize; ##[ ##4: #H; napply (λx:P.x) ##| ##1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -103,11 +103,11 @@ ndefinition instr_mode_destruct5 : nnormalize; ##[ ##5: #H; napply (λx:P.x) ##| ##1,2,3,4,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -120,11 +120,11 @@ ndefinition instr_mode_destruct6 : nnormalize; ##[ ##6: #H; napply (λx:P.x) ##| ##1,2,3,4,5,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -137,11 +137,11 @@ ndefinition instr_mode_destruct7 : nnormalize; ##[ ##7: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -154,11 +154,11 @@ ndefinition instr_mode_destruct8 : nnormalize; ##[ ##8: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -171,11 +171,11 @@ ndefinition instr_mode_destruct9 : nnormalize; ##[ ##9: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -188,11 +188,11 @@ ndefinition instr_mode_destruct10 : nnormalize; ##[ ##10: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -205,11 +205,11 @@ ndefinition instr_mode_destruct11 : nnormalize; ##[ ##11: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -222,11 +222,11 @@ ndefinition instr_mode_destruct12 : nnormalize; ##[ ##12: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -239,11 +239,11 @@ ndefinition instr_mode_destruct13 : nnormalize; ##[ ##13: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -256,11 +256,11 @@ ndefinition instr_mode_destruct14 : nnormalize; ##[ ##14: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -273,11 +273,11 @@ ndefinition instr_mode_destruct15 : nnormalize; ##[ ##15: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -290,11 +290,11 @@ ndefinition instr_mode_destruct16 : nnormalize; ##[ ##16: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -307,11 +307,11 @@ ndefinition instr_mode_destruct17 : nnormalize; ##[ ##17: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -324,11 +324,11 @@ ndefinition instr_mode_destruct18 : nnormalize; ##[ ##18: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -341,11 +341,11 @@ ndefinition instr_mode_destruct19 : nnormalize; ##[ ##19: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -358,11 +358,11 @@ ndefinition instr_mode_destruct20 : nnormalize; ##[ ##20: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -375,11 +375,11 @@ ndefinition instr_mode_destruct21 : nnormalize; ##[ ##21: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -392,11 +392,11 @@ ndefinition instr_mode_destruct22 : nnormalize; ##[ ##22: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -409,11 +409,11 @@ ndefinition instr_mode_destruct23 : nnormalize; ##[ ##23: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -426,11 +426,11 @@ ndefinition instr_mode_destruct24 : nnormalize; ##[ ##24: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -443,11 +443,11 @@ ndefinition instr_mode_destruct25 : nnormalize; ##[ ##25: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -460,11 +460,11 @@ ndefinition instr_mode_destruct26 : nnormalize; ##[ ##26: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -477,11 +477,11 @@ ndefinition instr_mode_destruct27 : nnormalize; ##[ ##27: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -494,11 +494,11 @@ ndefinition instr_mode_destruct28 : nnormalize; ##[ ##28: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -511,11 +511,11 @@ ndefinition instr_mode_destruct29 : nnormalize; ##[ ##29: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -528,11 +528,11 @@ ndefinition instr_mode_destruct30 : nnormalize; ##[ ##30: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -543,7 +543,7 @@ nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → 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 : @@ -559,11 +559,11 @@ ndefinition instr_mode_destruct31 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31: #n2; @@ -571,7 +571,7 @@ 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. @@ -580,7 +580,7 @@ nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = 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 : @@ -596,11 +596,11 @@ ndefinition instr_mode_destruct32 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##32: #n2; @@ -608,7 +608,7 @@ 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. @@ -617,7 +617,7 @@ nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1 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 : @@ -637,11 +637,11 @@ ndefinition instr_mode_destruct33 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##33: #n2; @@ -649,7 +649,7 @@ 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. @@ -658,7 +658,7 @@ nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1 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 : @@ -686,142 +686,142 @@ ndefinition instr_mode_destruct34 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##34: #n2; 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)) ##] ##] ##]