(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
(* ********************************************** *)
-nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
- #i1; #i2;
- ncases i1;
- ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
- ##| ##31: ncases i2; #n1;
- ##[ ##31: #n2;
- nchange with (eq_oct n2 n1 = eq_oct n1 n2);
- nrewrite > (symmetric_eqoct n1 n2);
- ##| ##32,33,34: #n2; nnormalize
- ##]
- nnormalize; napply refl_eq
- ##| ##32: ncases i2; #n1;
- ##[ ##32: #n2;
- nchange with (eq_oct n2 n1 = eq_oct n1 n2);
- nrewrite > (symmetric_eqoct n1 n2);
- ##| ##31,33,34: #n2; nnormalize
- ##]
- nnormalize; napply refl_eq
- ##| ##33: ncases i2; #n1;
- ##[ ##33: #n2;
- nchange with (eq_ex n2 n1 = eq_ex n1 n2);
- nrewrite > (symmetric_eqex n1 n2);
- ##| ##31,32,34: #n2; nnormalize
- ##]
- nnormalize; napply refl_eq
- ##| ##34: ncases i2; #n1;
- ##[ ##34: #n2;
- nchange with (eq_bit n2 n1 = eq_bit n1 n2);
- nrewrite > (symmetric_eqbit n1 n2);
- ##| ##31,32,33: #n2; nnormalize
- ##]
- nnormalize; napply refl_eq
- ##]
-nqed.
-
-nlemma eqim_to_eq1 : ∀i2.eq_im MODE_INH i2 = true → MODE_INH = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##1: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma decidable_im1 : ∀x:instr_mode.decidable (MODE_INH = x).
+ #x; nnormalize; nelim x;
+ ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im2 : ∀x:instr_mode.decidable (MODE_INHA = x).
+ #x; nnormalize; nelim x;
+ ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im3 : ∀x:instr_mode.decidable (MODE_INHX = x).
+ #x; nnormalize; nelim x;
+ ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im4 : ∀x:instr_mode.decidable (MODE_INHH = x).
+ #x; nnormalize; nelim x;
+ ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im5 : ∀x:instr_mode.decidable (MODE_INHX0ADD = x).
+ #x; nnormalize; nelim x;
+ ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im6 : ∀x:instr_mode.decidable (MODE_INHX1ADD = x).
+ #x; nnormalize; nelim x;
+ ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im7 : ∀x:instr_mode.decidable (MODE_INHX2ADD = x).
+ #x; nnormalize; nelim x;
+ ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im8 : ∀x:instr_mode.decidable (MODE_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im9 : ∀x:instr_mode.decidable (MODE_IMM1EXT = x).
+ #x; nnormalize; nelim x;
+ ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im10 : ∀x:instr_mode.decidable (MODE_IMM2 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im11 : ∀x:instr_mode.decidable (MODE_DIR1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im12 : ∀x:instr_mode.decidable (MODE_DIR2 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im13 : ∀x:instr_mode.decidable (MODE_IX0 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im14 : ∀x:instr_mode.decidable (MODE_IX1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im15 : ∀x:instr_mode.decidable (MODE_IX2 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im16 : ∀x:instr_mode.decidable (MODE_SP1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im17 : ∀x:instr_mode.decidable (MODE_SP2 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im18 : ∀x:instr_mode.decidable (MODE_DIR1_to_DIR1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im19 : ∀x:instr_mode.decidable (MODE_IMM1_to_DIR1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im20 : ∀x:instr_mode.decidable (MODE_IX0p_to_DIR1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im21 : ∀x:instr_mode.decidable (MODE_DIR1_to_IX0p = x).
+ #x; nnormalize; nelim x;
+ ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im22 : ∀x:instr_mode.decidable (MODE_INHA_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im23 : ∀x:instr_mode.decidable (MODE_INHX_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im24 : ∀x:instr_mode.decidable (MODE_IMM1_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im25 : ∀x:instr_mode.decidable (MODE_DIR1_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im26 : ∀x:instr_mode.decidable (MODE_IX0_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im27 : ∀x:instr_mode.decidable (MODE_IX0p_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im28 : ∀x:instr_mode.decidable (MODE_IX1_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im29 : ∀x:instr_mode.decidable (MODE_IX1p_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im30 : ∀x:instr_mode.decidable (MODE_SP1_and_IMM1 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im31 : ∀n.∀x:instr_mode.decidable ((MODE_DIRn n) = x).
+ #n1; #x; nnormalize; nelim x;
+ ##[ ##31: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct n1 n2) …);
+ ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_DIRn … H1))
+ ##]
+ ##| ##32,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im32 : ∀n.∀x:instr_mode.decidable ((MODE_DIRn_and_IMM1 n) = x).
+ #n1; #x; nnormalize; nelim x;
+ ##[ ##32: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct n1 n2) …);
+ ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_DIRn_and_IMM1 … H1))
+ ##]
+ ##| ##31,33,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im33 : ∀n.∀x:instr_mode.decidable ((MODE_TNY n) = x).
+ #n1; #x; nnormalize; nelim x;
+ ##[ ##33: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ex n1 n2) …);
+ ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_TNY … H1))
+ ##]
+ ##| ##31,32,34: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im34 : ∀n.∀x:instr_mode.decidable ((MODE_SRT n) = x).
+ #n1; #x; nnormalize; nelim x;
+ ##[ ##34: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bit n1 n2) …);
+ ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_SRT … H1))
+ ##]
+ ##| ##31,32,33: #n; ##]
+ ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
+nqed.
+
+nlemma decidable_im : ∀x,y:instr_mode.decidable (x = y).
+ #x; nelim x;
+ ##[ ##1: napply decidable_im1 ##| ##2: napply decidable_im2
+ ##| ##3: napply decidable_im3 ##| ##4: napply decidable_im4
+ ##| ##5: napply decidable_im5 ##| ##6: napply decidable_im6
+ ##| ##7: napply decidable_im7 ##| ##8: napply decidable_im8
+ ##| ##9: napply decidable_im9 ##| ##10: napply decidable_im10
+ ##| ##11: napply decidable_im11 ##| ##12: napply decidable_im12
+ ##| ##13: napply decidable_im13 ##| ##14: napply decidable_im14
+ ##| ##15: napply decidable_im15 ##| ##16: napply decidable_im16
+ ##| ##17: napply decidable_im17 ##| ##18: napply decidable_im18
+ ##| ##19: napply decidable_im19 ##| ##20: napply decidable_im20
+ ##| ##21: napply decidable_im21 ##| ##22: napply decidable_im22
+ ##| ##23: napply decidable_im23 ##| ##24: napply decidable_im24
+ ##| ##25: napply decidable_im25 ##| ##26: napply decidable_im26
+ ##| ##27: napply decidable_im27 ##| ##28: napply decidable_im28
+ ##| ##29: napply decidable_im29 ##| ##30: napply decidable_im30
+ ##| ##31: napply decidable_im31 ##| ##32: napply decidable_im32
+ ##| ##33: napply decidable_im33 ##| ##34: napply decidable_im34
##]
nqed.
-
-nlemma eqim_to_eq2 : ∀i2.eq_im MODE_INHA i2 = true → MODE_INHA = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##2: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+
+nlemma neqim_to_neq1 : ∀i2.(eq_im MODE_INH i2 = false) → (MODE_INH ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqim_to_neq2 : ∀i2.(eq_im MODE_INHA i2 = false) → (MODE_INHA ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##2: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq3 : ∀i2.eq_im MODE_INHX i2 = true → MODE_INHX = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##3: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq3 : ∀i2.(eq_im MODE_INHX i2 = false) → (MODE_INHX ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##3: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq4 : ∀i2.eq_im MODE_INHH i2 = true → MODE_INHH = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq4 : ∀i2.(eq_im MODE_INHH i2 = false) → (MODE_INHH ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##4: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq5 : ∀i2.eq_im MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##5: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq5 : ∀i2.(eq_im MODE_INHX0ADD i2 = false) → (MODE_INHX0ADD ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##5: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq6 : ∀i2.eq_im MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##6: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq6 : ∀i2.(eq_im MODE_INHX1ADD i2 = false) → (MODE_INHX1ADD ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##6: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq7 : ∀i2.eq_im MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##7: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq7 : ∀i2.(eq_im MODE_INHX2ADD i2 = false) → (MODE_INHX2ADD ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##7: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq8 : ∀i2.eq_im MODE_IMM1 i2 = true → MODE_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##8: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq8 : ∀i2.(eq_im MODE_IMM1 i2 = false) → (MODE_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##8: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq9 : ∀i2.eq_im MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##9: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq9 : ∀i2.(eq_im MODE_IMM1EXT i2 = false) → (MODE_IMM1EXT ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##9: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq10 : ∀i2.eq_im MODE_IMM2 i2 = true → MODE_IMM2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##10: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq10 : ∀i2.(eq_im MODE_IMM2 i2 = false) → (MODE_IMM2 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##10: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq11 : ∀i2.eq_im MODE_DIR1 i2 = true → MODE_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##11: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq11 : ∀i2.(eq_im MODE_DIR1 i2 = false) → (MODE_DIR1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##11: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq12 : ∀i2.eq_im MODE_DIR2 i2 = true → MODE_DIR2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##12: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq12 : ∀i2.(eq_im MODE_DIR2 i2 = false) → (MODE_DIR2 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##12: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq13 : ∀i2.eq_im MODE_IX0 i2 = true → MODE_IX0 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##13: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq13 : ∀i2.(eq_im MODE_IX0 i2 = false) → (MODE_IX0 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##13: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq14 : ∀i2.eq_im MODE_IX1 i2 = true → MODE_IX1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##14: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq14 : ∀i2.(eq_im MODE_IX1 i2 = false) → (MODE_IX1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##14: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq15 : ∀i2.eq_im MODE_IX2 i2 = true → MODE_IX2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##15: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq15 : ∀i2.(eq_im MODE_IX2 i2 = false) → (MODE_IX2 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##15: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq16 : ∀i2.eq_im MODE_SP1 i2 = true → MODE_SP1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##16: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq16 : ∀i2.(eq_im MODE_SP1 i2 = false) → (MODE_SP1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##16: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq17 : ∀i2.eq_im MODE_SP2 i2 = true → MODE_SP2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##17: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq17 : ∀i2.(eq_im MODE_SP2 i2 = false) → (MODE_SP2 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##17: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq18 : ∀i2.eq_im MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##18: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq18 : ∀i2.(eq_im MODE_DIR1_to_DIR1 i2 = false) → (MODE_DIR1_to_DIR1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##18: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq19 : ∀i2.eq_im MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##19: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq19 : ∀i2.(eq_im MODE_IMM1_to_DIR1 i2 = false) → (MODE_IMM1_to_DIR1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##19: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq20 : ∀i2.eq_im MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##20: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq20 : ∀i2.(eq_im MODE_IX0p_to_DIR1 i2 = false) → (MODE_IX0p_to_DIR1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##20: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq21 : ∀i2.eq_im MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##21: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq21 : ∀i2.(eq_im MODE_DIR1_to_IX0p i2 = false) → (MODE_DIR1_to_IX0p ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##21: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq22 : ∀i2.eq_im MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##22: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq22 : ∀i2.(eq_im MODE_INHA_and_IMM1 i2 = false) → (MODE_INHA_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##22: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq23 : ∀i2.eq_im MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##23: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq23 : ∀i2.(eq_im MODE_INHX_and_IMM1 i2 = false) → (MODE_INHX_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##23: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq24 : ∀i2.eq_im MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##24: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq24 : ∀i2.(eq_im MODE_IMM1_and_IMM1 i2 = false) → (MODE_IMM1_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##24: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq25 : ∀i2.eq_im MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##25: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq25 : ∀i2.(eq_im MODE_DIR1_and_IMM1 i2 = false) → (MODE_DIR1_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##25: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq26 : ∀i2.eq_im MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##26: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq26 : ∀i2.(eq_im MODE_IX0_and_IMM1 i2 = false) → (MODE_IX0_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##26: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq27 : ∀i2.eq_im MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##27: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq27 : ∀i2.(eq_im MODE_IX0p_and_IMM1 i2 = false) → (MODE_IX0p_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##27: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq28 : ∀i2.eq_im MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##28: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq28 : ∀i2.(eq_im MODE_IX1_and_IMM1 i2 = false) → (MODE_IX1_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##28: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq29 : ∀i2.eq_im MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##29: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq29 : ∀i2.(eq_im MODE_IX1p_and_IMM1 i2 = false) → (MODE_IX1p_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##29: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq30 : ∀i2.eq_im MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##30: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma neqim_to_neq30 : ∀i2.(eq_im MODE_SP1_and_IMM1 i2 = false) → (MODE_SP1_and_IMM1 ≠ i2).
+ #i2; nelim i2; nnormalize;
+ ##[ ##30: #H; napply (bool_destruct … H)
+ ##| ##31,32,33,34: #n ##]
+ ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##31: #n2; #H;
- nchange in H:(%) with (eq_oct n1 n2 = true);
- nrewrite > (eqoct_to_eq … H);
- napply refl_eq
- ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
+nlemma neqim_to_neq31 : ∀n.∀i2.(eq_im (MODE_DIRn n) i2 = false) → ((MODE_DIRn n) ≠ i2).
+ #n1; #i2; nelim i2;
+ ##[ ##31: #n2; #H; nchange in H:(%) with (eq_oct n1 n2 = false);
+ nnormalize; #H1; napply (neqoct_to_neq … H); napply (instrmode_destruct_MODE_DIRn … H1)
+ ##| ##32,33,34: #n ##]
+ ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##32: #n2; #H;
- nchange in H:(%) with (eq_oct n1 n2 = true);
- nrewrite > (eqoct_to_eq … H);
- napply refl_eq
- ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
+nlemma neqim_to_neq32 : ∀n.∀i2.(eq_im (MODE_DIRn_and_IMM1 n) i2 = false) → ((MODE_DIRn_and_IMM1 n) ≠ i2).
+ #n1; #i2; nelim i2;
+ ##[ ##32: #n2; #H; nchange in H:(%) with (eq_oct n1 n2 = false);
+ nnormalize; #H1; napply (neqoct_to_neq … H); napply (instrmode_destruct_MODE_DIRn_and_IMM1 … H1)
+ ##| ##31,33,34: #n ##]
+ ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##33: #n2; #H;
- nchange in H:(%) with (eq_ex n1 n2 = true);
- nrewrite > (eqex_to_eq … H);
- napply refl_eq
- ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
+nlemma neqim_to_neq33 : ∀n.∀i2.(eq_im (MODE_TNY n) i2 = false) → ((MODE_TNY n) ≠ i2).
+ #n1; #i2; nelim i2;
+ ##[ ##33: #n2; #H; nchange in H:(%) with (eq_ex n1 n2 = false);
+ nnormalize; #H1; napply (neqex_to_neq … H); napply (instrmode_destruct_MODE_TNY … H1)
+ ##| ##31,32,34: #n ##]
+ ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##34: #n2; #H;
- nchange in H:(%) with (eq_bit n1 n2 = true);
- nrewrite > (eqbit_to_eq … H);
- napply refl_eq
- ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
+nlemma neqim_to_neq34 : ∀n.∀i2.(eq_im (MODE_SRT n) i2 = false) → ((MODE_SRT n) ≠ i2).
+ #n1; #i2; nelim i2;
+ ##[ ##34: #n2; #H; nchange in H:(%) with (eq_bit n1 n2 = false);
+ nnormalize; #H1; napply (neqbit_to_neq … H); napply (instrmode_destruct_MODE_SRT … H1)
+ ##| ##31,32,33: #n ##]
+ ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
##]
nqed.
-nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
- #i1; ncases i1;
- ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
- ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
- ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
- ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
- ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
- ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
- ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
- ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
- ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
- ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
- ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
- ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
- ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
- ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
- ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
- ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
- ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
+nlemma neqim_to_neq : ∀i1,i2.(eq_im i1 i2 = false) → (i1 ≠ i2).
+ #i1; nelim i1;
+ ##[ ##1: napply neqim_to_neq1 ##| ##2: napply neqim_to_neq2
+ ##| ##3: napply neqim_to_neq3 ##| ##4: napply neqim_to_neq4
+ ##| ##5: napply neqim_to_neq5 ##| ##6: napply neqim_to_neq6
+ ##| ##7: napply neqim_to_neq7 ##| ##8: napply neqim_to_neq8
+ ##| ##9: napply neqim_to_neq9 ##| ##10: napply neqim_to_neq10
+ ##| ##11: napply neqim_to_neq11 ##| ##12: napply neqim_to_neq12
+ ##| ##13: napply neqim_to_neq13 ##| ##14: napply neqim_to_neq14
+ ##| ##15: napply neqim_to_neq15 ##| ##16: napply neqim_to_neq16
+ ##| ##17: napply neqim_to_neq17 ##| ##18: napply neqim_to_neq18
+ ##| ##19: napply neqim_to_neq19 ##| ##20: napply neqim_to_neq20
+ ##| ##21: napply neqim_to_neq21 ##| ##22: napply neqim_to_neq22
+ ##| ##23: napply neqim_to_neq23 ##| ##24: napply neqim_to_neq24
+ ##| ##25: napply neqim_to_neq25 ##| ##26: napply neqim_to_neq26
+ ##| ##27: napply neqim_to_neq27 ##| ##28: napply neqim_to_neq28
+ ##| ##29: napply neqim_to_neq29 ##| ##30: napply neqim_to_neq30
+ ##| ##31: napply neqim_to_neq31 ##| ##32: napply neqim_to_neq32
+ ##| ##33: napply neqim_to_neq33 ##| ##34: napply neqim_to_neq34
##]
nqed.
-nlemma eq_to_eqim1 : ∀i2.MODE_INH = i2 → eq_im MODE_INH i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##1: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim1 : ∀i2.MODE_INH ≠ i2 → eq_im MODE_INH i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##1: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim2 : ∀i2.MODE_INHA = i2 → eq_im MODE_INHA i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##2: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim2 : ∀i2.MODE_INHA ≠ i2 → eq_im MODE_INHA i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##2: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim3 : ∀i2.MODE_INHX = i2 → eq_im MODE_INHX i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##3: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim3 : ∀i2.MODE_INHX ≠ i2 → eq_im MODE_INHX i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##3: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim4 : ∀i2.MODE_INHH = i2 → eq_im MODE_INHH i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim4 : ∀i2.MODE_INHH ≠ i2 → eq_im MODE_INHH i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##4: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim5 : ∀i2.MODE_INHX0ADD = i2 → eq_im MODE_INHX0ADD i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##5: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim5 : ∀i2.MODE_INHX0ADD ≠ i2 → eq_im MODE_INHX0ADD i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##5: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim6 : ∀i2.MODE_INHX1ADD = i2 → eq_im MODE_INHX1ADD i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##6: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim6 : ∀i2.MODE_INHX1ADD ≠ i2 → eq_im MODE_INHX1ADD i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##6: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim7 : ∀i2.MODE_INHX2ADD = i2 → eq_im MODE_INHX2ADD i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##7: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim7 : ∀i2.MODE_INHX2ADD ≠ i2 → eq_im MODE_INHX2ADD i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##7: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim8 : ∀i2.MODE_IMM1 = i2 → eq_im MODE_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##8: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim8 : ∀i2.MODE_IMM1 ≠ i2 → eq_im MODE_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##8: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim9 : ∀i2.MODE_IMM1EXT = i2 → eq_im MODE_IMM1EXT i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##9: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim9 : ∀i2.MODE_IMM1EXT ≠ i2 → eq_im MODE_IMM1EXT i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##9: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim10 : ∀i2.MODE_IMM2 = i2 → eq_im MODE_IMM2 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##10: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim10 : ∀i2.MODE_IMM2 ≠ i2 → eq_im MODE_IMM2 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##10: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim11 : ∀i2.MODE_DIR1 = i2 → eq_im MODE_DIR1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##11: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim11 : ∀i2.MODE_DIR1 ≠ i2 → eq_im MODE_DIR1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##11: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim12 : ∀i2.MODE_DIR2 = i2 → eq_im MODE_DIR2 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##12: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim12 : ∀i2.MODE_DIR2 ≠ i2 → eq_im MODE_DIR2 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##12: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim13 : ∀i2.MODE_IX0 = i2 → eq_im MODE_IX0 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##13: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim13 : ∀i2.MODE_IX0 ≠ i2 → eq_im MODE_IX0 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##13: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim14 : ∀i2.MODE_IX1 = i2 → eq_im MODE_IX1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##14: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim14 : ∀i2.MODE_IX1 ≠ i2 → eq_im MODE_IX1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##14: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim15 : ∀i2.MODE_IX2 = i2 → eq_im MODE_IX2 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##15: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim15 : ∀i2.MODE_IX2 ≠ i2 → eq_im MODE_IX2 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##15: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim16 : ∀i2.MODE_SP1 = i2 → eq_im MODE_SP1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##16: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim16 : ∀i2.MODE_SP1 ≠ i2 → eq_im MODE_SP1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##16: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim17 : ∀i2.MODE_SP2 = i2 → eq_im MODE_SP2 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##17: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim17 : ∀i2.MODE_SP2 ≠ i2 → eq_im MODE_SP2 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##17: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_im MODE_DIR1_to_DIR1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##18: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim18 : ∀i2.MODE_DIR1_to_DIR1 ≠ i2 → eq_im MODE_DIR1_to_DIR1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##18: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_im MODE_IMM1_to_DIR1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##19: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim19 : ∀i2.MODE_IMM1_to_DIR1 ≠ i2 → eq_im MODE_IMM1_to_DIR1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##19: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_im MODE_IX0p_to_DIR1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##20: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim20 : ∀i2.MODE_IX0p_to_DIR1 ≠ i2 → eq_im MODE_IX0p_to_DIR1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##20: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_im MODE_DIR1_to_IX0p i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##21: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim21 : ∀i2.MODE_DIR1_to_IX0p ≠ i2 → eq_im MODE_DIR1_to_IX0p i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##21: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_im MODE_INHA_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##22: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim22 : ∀i2.MODE_INHA_and_IMM1≠ i2 → eq_im MODE_INHA_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##22: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_im MODE_INHX_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##23: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim23 : ∀i2.MODE_INHX_and_IMM1 ≠ i2 → eq_im MODE_INHX_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##23: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_im MODE_IMM1_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##24: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim24 : ∀i2.MODE_IMM1_and_IMM1 ≠ i2 → eq_im MODE_IMM1_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##24: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_im MODE_DIR1_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##25: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim25 : ∀i2.MODE_DIR1_and_IMM1 ≠ i2 → eq_im MODE_DIR1_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##25: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_im MODE_IX0_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##26: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim26 : ∀i2.MODE_IX0_and_IMM1 ≠ i2 → eq_im MODE_IX0_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##26: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_im MODE_IX0p_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##27: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim27 : ∀i2.MODE_IX0p_and_IMM1 ≠ i2 → eq_im MODE_IX0p_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##27: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_im MODE_IX1_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##28: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim28 : ∀i2.MODE_IX1_and_IMM1 ≠ i2 → eq_im MODE_IX1_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##28: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_im MODE_IX1p_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##29: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim29 : ∀i2.MODE_IX1p_and_IMM1 ≠ i2 → eq_im MODE_IX1p_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##29: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_im MODE_SP1_and_IMM1 i2 = true.
- #t2; ncases t2; nnormalize;
- ##[ ##30: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
- ##| ##*: #H; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim30 : ∀i2.MODE_SP1_and_IMM1 ≠ i2 → eq_im MODE_SP1_and_IMM1 i2 = false.
+ #i2; nelim i2; nnormalize;
+ ##[ ##30: #H; nelim (H (refl_eq …))
+ ##| ##31,32,33,34: #n; ##]
+ ##[ ##*: #H; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_im (MODE_DIRn n1) i2 = true.
- #n1; #t2; ncases t2;
- ##[ ##31: #n2; #H;
- nchange with (eq_oct n1 n2 = true);
- nrewrite > (instr_mode_destruct_MODE_DIRn … H);
- nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
- napply refl_eq
- ##| ##32,33,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim31 : ∀n.∀i2.(MODE_DIRn n) ≠ i2 → eq_im (MODE_DIRn n) i2 = false.
+ #n1; #i2; nelim i2;
+ ##[ ##31: #n2; #H; nchange with (eq_oct n1 n2 = false); napply (neq_to_neqoct n1 n2 ?);
+ nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
+ ##| ##32,33,34: #n; ##]
+ ##[ ##*: #H; nnormalize; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_im (MODE_DIRn_and_IMM1 n1) i2 = true.
- #n1; #t2; ncases t2;
- ##[ ##32: #n2; #H;
- nchange with (eq_oct n1 n2 = true);
- nrewrite > (instr_mode_destruct_MODE_DIRn_and_IMM1 … H);
- nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
- napply refl_eq
- ##| ##31,33,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim32 : ∀n.∀i2.(MODE_DIRn_and_IMM1 n) ≠ i2 → eq_im (MODE_DIRn_and_IMM1 n) i2 = false.
+ #n1; #i2; nelim i2;
+ ##[ ##32: #n2; #H; nchange with (eq_oct n1 n2 = false); napply (neq_to_neqoct n1 n2 ?);
+ nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
+ ##| ##31,33,34: #n; ##]
+ ##[ ##*: #H; nnormalize; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_im (MODE_TNY n1) i2 = true.
- #n1; #t2; ncases t2;
- ##[ ##33: #n2; #H;
- nchange with (eq_ex n1 n2 = true);
- nrewrite > (instr_mode_destruct_MODE_TNY … H);
- nrewrite > (eq_to_eqex n2 n2 (refl_eq …));
- napply refl_eq
- ##| ##31,32,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim33 : ∀n.∀i2.(MODE_TNY n) ≠ i2 → eq_im (MODE_TNY n) i2 = false.
+ #n1; #i2; nelim i2;
+ ##[ ##33: #n2; #H; nchange with (eq_ex n1 n2 = false); napply (neq_to_neqex n1 n2 ?);
+ nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
+ ##| ##31,32,34: #n; ##]
+ ##[ ##*: #H; nnormalize; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_im (MODE_SRT n1) i2 = true.
- #n1; #t2; ncases t2;
- ##[ ##34: #n2; #H;
- nchange with (eq_bit n1 n2 = true);
- nrewrite > (instr_mode_destruct_MODE_SRT … H);
- nrewrite > (eq_to_eqbit n2 n2 (refl_eq …));
- napply refl_eq
- ##| ##31,32,33: #n; #H; nnormalize; napply (instr_mode_destruct … H)
- ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
+nlemma neq_to_neqim34 : ∀n.∀i2.(MODE_SRT n) ≠ i2 → eq_im (MODE_SRT n) i2 = false.
+ #n1; #i2; nelim i2;
+ ##[ ##34: #n2; #H; nchange with (eq_bit n1 n2 = false); napply (neq_to_neqbit n1 n2 ?);
+ nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
+ ##| ##31,32,33: #n; ##]
+ ##[ ##*: #H; nnormalize; napply refl_eq
##]
nqed.
-nlemma eq_to_eqim : ∀i1,i2.i1 = i2 → eq_im i1 i2 = true.
- #i1; ncases i1;
- ##[ ##1: napply eq_to_eqim1 ##| ##2: napply eq_to_eqim2
- ##| ##3: napply eq_to_eqim3 ##| ##4: napply eq_to_eqim4
- ##| ##5: napply eq_to_eqim5 ##| ##6: napply eq_to_eqim6
- ##| ##7: napply eq_to_eqim7 ##| ##8: napply eq_to_eqim8
- ##| ##9: napply eq_to_eqim9 ##| ##10: napply eq_to_eqim10
- ##| ##11: napply eq_to_eqim11 ##| ##12: napply eq_to_eqim12
- ##| ##13: napply eq_to_eqim13 ##| ##14: napply eq_to_eqim14
- ##| ##15: napply eq_to_eqim15 ##| ##16: napply eq_to_eqim16
- ##| ##17: napply eq_to_eqim17 ##| ##18: napply eq_to_eqim18
- ##| ##19: napply eq_to_eqim19 ##| ##20: napply eq_to_eqim20
- ##| ##21: napply eq_to_eqim21 ##| ##22: napply eq_to_eqim22
- ##| ##23: napply eq_to_eqim23 ##| ##24: napply eq_to_eqim24
- ##| ##25: napply eq_to_eqim25 ##| ##26: napply eq_to_eqim26
- ##| ##27: napply eq_to_eqim27 ##| ##28: napply eq_to_eqim28
- ##| ##29: napply eq_to_eqim29 ##| ##30: napply eq_to_eqim30
- ##| ##31: napply eq_to_eqim31 ##| ##32: napply eq_to_eqim32
- ##| ##33: napply eq_to_eqim33 ##| ##34: napply eq_to_eqim34
+nlemma neq_to_neqim : ∀i1,i2.i1 ≠ i2 → eq_im i1 i2 = false.
+ #i1; nelim i1;
+ ##[ ##1: napply neq_to_neqim1 ##| ##2: napply neq_to_neqim2
+ ##| ##3: napply neq_to_neqim3 ##| ##4: napply neq_to_neqim4
+ ##| ##5: napply neq_to_neqim5 ##| ##6: napply neq_to_neqim6
+ ##| ##7: napply neq_to_neqim7 ##| ##8: napply neq_to_neqim8
+ ##| ##9: napply neq_to_neqim9 ##| ##10: napply neq_to_neqim10
+ ##| ##11: napply neq_to_neqim11 ##| ##12: napply neq_to_neqim12
+ ##| ##13: napply neq_to_neqim13 ##| ##14: napply neq_to_neqim14
+ ##| ##15: napply neq_to_neqim15 ##| ##16: napply neq_to_neqim16
+ ##| ##17: napply neq_to_neqim17 ##| ##18: napply neq_to_neqim18
+ ##| ##19: napply neq_to_neqim19 ##| ##20: napply neq_to_neqim20
+ ##| ##21: napply neq_to_neqim21 ##| ##22: napply neq_to_neqim22
+ ##| ##23: napply neq_to_neqim23 ##| ##24: napply neq_to_neqim24
+ ##| ##25: napply neq_to_neqim25 ##| ##26: napply neq_to_neqim26
+ ##| ##27: napply neq_to_neqim27 ##| ##28: napply neq_to_neqim28
+ ##| ##29: napply neq_to_neqim29 ##| ##30: napply neq_to_neqim30
+ ##| ##31: napply neq_to_neqim31 ##| ##32: napply neq_to_neqim32
+ ##| ##33: napply neq_to_neqim33 ##| ##34: napply neq_to_neqim34
##]
nqed.
projects / helm.git / blobdiff