-ndefinition instr_mode_destruct1 :
- Πi2.ΠP:Prop.MODE_INH = i2 → match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct2 :
- Πi2.ΠP:Prop.MODE_INHA = i2 → match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct3 :
- Πi2.ΠP:Prop.MODE_INHX = i2 → match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct4 :
- Πi2.ΠP:Prop.MODE_INHH = i2 → match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct5 :
- Πi2.ΠP:Prop.MODE_INHX0ADD = i2 → match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct6 :
- Πi2.ΠP:Prop.MODE_INHX1ADD = i2 → match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct7 :
- Πi2.ΠP:Prop.MODE_INHX2ADD = i2 → match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct8 :
- Πi2.ΠP:Prop.MODE_IMM1 = i2 → match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct9 :
- Πi2.ΠP:Prop.MODE_IMM1EXT = i2 → match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct10 :
- Πi2.ΠP:Prop.MODE_IMM2 = i2 → match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct11 :
- Πi2.ΠP:Prop.MODE_DIR1 = i2 → match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct12 :
- Πi2.ΠP:Prop.MODE_DIR2 = i2 → match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct13 :
- Πi2.ΠP:Prop.MODE_IX0 = i2 → match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct14 :
- Πi2.ΠP:Prop.MODE_IX1 = i2 → match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct15 :
- Πi2.ΠP:Prop.MODE_IX2 = i2 → match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct16 :
- Πi2.ΠP:Prop.MODE_SP1 = i2 → match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct17 :
- Πi2.ΠP:Prop.MODE_SP2 = i2 → match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##| ##31,32,33,34: #n; #H;
- napply False_ind;
- nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct18 :
- Πi2.ΠP:Prop.MODE_DIR1_to_DIR1 = i2 → match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct19 :
- Πi2.ΠP:Prop.MODE_IMM1_to_DIR1 = i2 → match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct20 :
- Πi2.ΠP:Prop.MODE_IX0p_to_DIR1 = i2 → match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct21 :
- Πi2.ΠP:Prop.MODE_DIR1_to_IX0p = i2 → match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct22 :
- Πi2.ΠP:Prop.MODE_INHA_and_IMM1 = i2 → match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct23 :
- Πi2.ΠP:Prop.MODE_INHX_and_IMM1 = i2 → match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct24 :
- Πi2.ΠP:Prop.MODE_IMM1_and_IMM1 = i2 → match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct25 :
- Πi2.ΠP:Prop.MODE_DIR1_and_IMM1 = i2 → match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct26 :
- Πi2.ΠP:Prop.MODE_IX0_and_IMM1 = i2 → match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct27 :
- Πi2.ΠP:Prop.MODE_IX0p_and_IMM1 = i2 → match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct28 :
- Πi2.ΠP:Prop.MODE_IX1_and_IMM1 = i2 → match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct29 :
- Πi2.ΠP:Prop.MODE_IX1p_and_IMM1 = i2 → match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition instr_mode_destruct30 :
- Πi2.ΠP:Prop.MODE_SP1_and_IMM1 = i2 → match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ].
- #i2; #P;
- ncases i2;
- 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;
- 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;
- nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.