freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode_base_lemmas_instrmode2.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma
index 06aa6c0401dc820c55373ff8c8b0b4e5563bbf9c..a80e96d2191312ad73674d6d8ffeaea92bfb8fad 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma
@@ -26,7 +26,7 @@ include "freescale/opcode_base_lemmas_instrmode1.ma".
 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
 (* ********************************************** *)
 
-nlemma symmetric_eqinstrmode : symmetricT instr_mode bool eq_instrmode.
+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
@@ -82,15 +82,15 @@ nlemma symmetric_eqinstrmode : symmetricT instr_mode bool eq_instrmode.
      nnormalize; napply refl_eq
  ##| ##34: ncases i2; #n1;
      ##[ ##34: #n2;
-               nchange with (eq_bitrig n2 n1 = eq_bitrig n1 n2);
-               nrewrite > (symmetric_eqbitrig n1 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 eqinstrmode_to_eq1 : ∀i2.eq_instrmode MODE_INH i2 = true → MODE_INH = i2.
+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)
@@ -98,7 +98,7 @@ nlemma eqinstrmode_to_eq1 : ∀i2.eq_instrmode MODE_INH i2 = true → MODE_INH =
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq2 : ∀i2.eq_instrmode MODE_INHA i2 = true → MODE_INHA = i2.
+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)
@@ -106,7 +106,7 @@ nlemma eqinstrmode_to_eq2 : ∀i2.eq_instrmode MODE_INHA i2 = true → MODE_INHA
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq3 : ∀i2.eq_instrmode MODE_INHX i2 = true → MODE_INHX = i2.
+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)
@@ -114,7 +114,7 @@ nlemma eqinstrmode_to_eq3 : ∀i2.eq_instrmode MODE_INHX i2 = true → MODE_INHX
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq4 : ∀i2.eq_instrmode MODE_INHH i2 = true → MODE_INHH = i2.
+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)
@@ -122,7 +122,7 @@ nlemma eqinstrmode_to_eq4 : ∀i2.eq_instrmode MODE_INHH i2 = true → MODE_INHH
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq5 : ∀i2.eq_instrmode MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
+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)
@@ -130,7 +130,7 @@ nlemma eqinstrmode_to_eq5 : ∀i2.eq_instrmode MODE_INHX0ADD i2 = true → MODE_
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq6 : ∀i2.eq_instrmode MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
+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)
@@ -138,7 +138,7 @@ nlemma eqinstrmode_to_eq6 : ∀i2.eq_instrmode MODE_INHX1ADD i2 = true → MODE_
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq7 : ∀i2.eq_instrmode MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
+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)
@@ -146,7 +146,7 @@ nlemma eqinstrmode_to_eq7 : ∀i2.eq_instrmode MODE_INHX2ADD i2 = true → MODE_
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq8 : ∀i2.eq_instrmode MODE_IMM1 i2 = true → MODE_IMM1 = i2.
+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)
@@ -154,7 +154,7 @@ nlemma eqinstrmode_to_eq8 : ∀i2.eq_instrmode MODE_IMM1 i2 = true → MODE_IMM1
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq9 : ∀i2.eq_instrmode MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
+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)
@@ -162,7 +162,7 @@ nlemma eqinstrmode_to_eq9 : ∀i2.eq_instrmode MODE_IMM1EXT i2 = true → MODE_I
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq10 : ∀i2.eq_instrmode MODE_IMM2 i2 = true → MODE_IMM2 = i2.
+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)
@@ -170,7 +170,7 @@ nlemma eqinstrmode_to_eq10 : ∀i2.eq_instrmode MODE_IMM2 i2 = true → MODE_IMM
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq11 : ∀i2.eq_instrmode MODE_DIR1 i2 = true → MODE_DIR1 = i2.
+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)
@@ -178,7 +178,7 @@ nlemma eqinstrmode_to_eq11 : ∀i2.eq_instrmode MODE_DIR1 i2 = true → MODE_DIR
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq12 : ∀i2.eq_instrmode MODE_DIR2 i2 = true → MODE_DIR2 = i2.
+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)
@@ -186,7 +186,7 @@ nlemma eqinstrmode_to_eq12 : ∀i2.eq_instrmode MODE_DIR2 i2 = true → MODE_DIR
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq13 : ∀i2.eq_instrmode MODE_IX0 i2 = true → MODE_IX0 = i2.
+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)
@@ -194,7 +194,7 @@ nlemma eqinstrmode_to_eq13 : ∀i2.eq_instrmode MODE_IX0 i2 = true → MODE_IX0
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq14 : ∀i2.eq_instrmode MODE_IX1 i2 = true → MODE_IX1 = i2.
+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)
@@ -202,7 +202,7 @@ nlemma eqinstrmode_to_eq14 : ∀i2.eq_instrmode MODE_IX1 i2 = true → MODE_IX1
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq15 : ∀i2.eq_instrmode MODE_IX2 i2 = true → MODE_IX2 = i2.
+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)
@@ -210,7 +210,7 @@ nlemma eqinstrmode_to_eq15 : ∀i2.eq_instrmode MODE_IX2 i2 = true → MODE_IX2
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq16 : ∀i2.eq_instrmode MODE_SP1 i2 = true → MODE_SP1 = i2.
+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)
@@ -218,7 +218,7 @@ nlemma eqinstrmode_to_eq16 : ∀i2.eq_instrmode MODE_SP1 i2 = true → MODE_SP1
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq17 : ∀i2.eq_instrmode MODE_SP2 i2 = true → MODE_SP2 = i2.
+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)
@@ -226,7 +226,7 @@ nlemma eqinstrmode_to_eq17 : ∀i2.eq_instrmode MODE_SP2 i2 = true → MODE_SP2
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq18 : ∀i2.eq_instrmode MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
+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)
@@ -234,7 +234,7 @@ nlemma eqinstrmode_to_eq18 : ∀i2.eq_instrmode MODE_DIR1_to_DIR1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq19 : ∀i2.eq_instrmode MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
+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)
@@ -242,7 +242,7 @@ nlemma eqinstrmode_to_eq19 : ∀i2.eq_instrmode MODE_IMM1_to_DIR1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq20 : ∀i2.eq_instrmode MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
+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)
@@ -250,7 +250,7 @@ nlemma eqinstrmode_to_eq20 : ∀i2.eq_instrmode MODE_IX0p_to_DIR1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq21 : ∀i2.eq_instrmode MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
+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)
@@ -258,7 +258,7 @@ nlemma eqinstrmode_to_eq21 : ∀i2.eq_instrmode MODE_DIR1_to_IX0p i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq22 : ∀i2.eq_instrmode MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
+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)
@@ -266,7 +266,7 @@ nlemma eqinstrmode_to_eq22 : ∀i2.eq_instrmode MODE_INHA_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq23 : ∀i2.eq_instrmode MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
+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)
@@ -274,7 +274,7 @@ nlemma eqinstrmode_to_eq23 : ∀i2.eq_instrmode MODE_INHX_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq24 : ∀i2.eq_instrmode MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
+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)
@@ -282,7 +282,7 @@ nlemma eqinstrmode_to_eq24 : ∀i2.eq_instrmode MODE_IMM1_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq25 : ∀i2.eq_instrmode MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
+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)
@@ -290,7 +290,7 @@ nlemma eqinstrmode_to_eq25 : ∀i2.eq_instrmode MODE_DIR1_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq26 : ∀i2.eq_instrmode MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
+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)
@@ -298,7 +298,7 @@ nlemma eqinstrmode_to_eq26 : ∀i2.eq_instrmode MODE_IX0_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq27 : ∀i2.eq_instrmode MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
+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)
@@ -306,7 +306,7 @@ nlemma eqinstrmode_to_eq27 : ∀i2.eq_instrmode MODE_IX0p_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq28 : ∀i2.eq_instrmode MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
+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)
@@ -314,7 +314,7 @@ nlemma eqinstrmode_to_eq28 : ∀i2.eq_instrmode MODE_IX1_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq29 : ∀i2.eq_instrmode MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
+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)
@@ -322,7 +322,7 @@ nlemma eqinstrmode_to_eq29 : ∀i2.eq_instrmode MODE_IX1p_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq30 : ∀i2.eq_instrmode MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
+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)
@@ -330,7 +330,7 @@ nlemma eqinstrmode_to_eq30 : ∀i2.eq_instrmode MODE_SP1_and_IMM1 i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq31 : ∀n1,i2.eq_instrmode (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
+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);
@@ -341,7 +341,7 @@ nlemma eqinstrmode_to_eq31 : ∀n1,i2.eq_instrmode (MODE_DIRn n1) i2 = true →
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq32 : ∀n1,i2.eq_instrmode (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
+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);
@@ -352,7 +352,7 @@ nlemma eqinstrmode_to_eq32 : ∀n1,i2.eq_instrmode (MODE_DIRn_and_IMM1 n1) i2 =
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq33 : ∀n1,i2.eq_instrmode (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
+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);
@@ -363,40 +363,40 @@ nlemma eqinstrmode_to_eq33 : ∀n1,i2.eq_instrmode (MODE_TNY n1) i2 = true → M
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq34 : ∀n1,i2.eq_instrmode (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
+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_bitrig n1 n2 = true);
-     nrewrite > (eqbitrig_to_eq … 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)
  ##]
 nqed.
 
-nlemma eqinstrmode_to_eq : ∀i1,i2.eq_instrmode i1 i2 = true → i1 = i2.
+nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
  #i1; ncases i1;
- ##[ ##1: napply eqinstrmode_to_eq1 ##| ##2: napply eqinstrmode_to_eq2
- ##| ##3: napply eqinstrmode_to_eq3 ##| ##4: napply eqinstrmode_to_eq4
- ##| ##5: napply eqinstrmode_to_eq5 ##| ##6: napply eqinstrmode_to_eq6
- ##| ##7: napply eqinstrmode_to_eq7 ##| ##8: napply eqinstrmode_to_eq8
- ##| ##9: napply eqinstrmode_to_eq9 ##| ##10: napply eqinstrmode_to_eq10
- ##| ##11: napply eqinstrmode_to_eq11 ##| ##12: napply eqinstrmode_to_eq12
- ##| ##13: napply eqinstrmode_to_eq13 ##| ##14: napply eqinstrmode_to_eq14
- ##| ##15: napply eqinstrmode_to_eq15 ##| ##16: napply eqinstrmode_to_eq16
- ##| ##17: napply eqinstrmode_to_eq17 ##| ##18: napply eqinstrmode_to_eq18
- ##| ##19: napply eqinstrmode_to_eq19 ##| ##20: napply eqinstrmode_to_eq20
- ##| ##21: napply eqinstrmode_to_eq21 ##| ##22: napply eqinstrmode_to_eq22
- ##| ##23: napply eqinstrmode_to_eq23 ##| ##24: napply eqinstrmode_to_eq24
- ##| ##25: napply eqinstrmode_to_eq25 ##| ##26: napply eqinstrmode_to_eq26
- ##| ##27: napply eqinstrmode_to_eq27 ##| ##28: napply eqinstrmode_to_eq28
- ##| ##29: napply eqinstrmode_to_eq29 ##| ##30: napply eqinstrmode_to_eq30
- ##| ##31: napply eqinstrmode_to_eq31 ##| ##32: napply eqinstrmode_to_eq32
- ##| ##33: napply eqinstrmode_to_eq33 ##| ##34: napply eqinstrmode_to_eq34
- ##]
-nqed. 
-
-nlemma eq_to_eqinstrmode1 : ∀i2.MODE_INH = i2 → eq_instrmode MODE_INH i2 = true.
+ ##[ ##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
+ ##]
+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)
@@ -404,7 +404,7 @@ nlemma eq_to_eqinstrmode1 : ∀i2.MODE_INH = i2 → eq_instrmode MODE_INH i2 = t
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode2 : ∀i2.MODE_INHA = i2 → eq_instrmode MODE_INHA i2 = true.
+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)
@@ -412,7 +412,7 @@ nlemma eq_to_eqinstrmode2 : ∀i2.MODE_INHA = i2 → eq_instrmode MODE_INHA i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode3 : ∀i2.MODE_INHX = i2 → eq_instrmode MODE_INHX i2 = true.
+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)
@@ -420,7 +420,7 @@ nlemma eq_to_eqinstrmode3 : ∀i2.MODE_INHX = i2 → eq_instrmode MODE_INHX i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode4 : ∀i2.MODE_INHH = i2 → eq_instrmode MODE_INHH i2 = true.
+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)
@@ -428,7 +428,7 @@ nlemma eq_to_eqinstrmode4 : ∀i2.MODE_INHH = i2 → eq_instrmode MODE_INHH i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode5 : ∀i2.MODE_INHX0ADD = i2 → eq_instrmode MODE_INHX0ADD i2 = true.
+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)
@@ -436,7 +436,7 @@ nlemma eq_to_eqinstrmode5 : ∀i2.MODE_INHX0ADD = i2 → eq_instrmode MODE_INHX0
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode6 : ∀i2.MODE_INHX1ADD = i2 → eq_instrmode MODE_INHX1ADD i2 = true.
+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)
@@ -444,7 +444,7 @@ nlemma eq_to_eqinstrmode6 : ∀i2.MODE_INHX1ADD = i2 → eq_instrmode MODE_INHX1
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode7 : ∀i2.MODE_INHX2ADD = i2 → eq_instrmode MODE_INHX2ADD i2 = true.
+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)
@@ -452,7 +452,7 @@ nlemma eq_to_eqinstrmode7 : ∀i2.MODE_INHX2ADD = i2 → eq_instrmode MODE_INHX2
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode8 : ∀i2.MODE_IMM1 = i2 → eq_instrmode MODE_IMM1 i2 = true.
+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)
@@ -460,7 +460,7 @@ nlemma eq_to_eqinstrmode8 : ∀i2.MODE_IMM1 = i2 → eq_instrmode MODE_IMM1 i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode9 : ∀i2.MODE_IMM1EXT = i2 → eq_instrmode MODE_IMM1EXT i2 = true.
+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)
@@ -468,7 +468,7 @@ nlemma eq_to_eqinstrmode9 : ∀i2.MODE_IMM1EXT = i2 → eq_instrmode MODE_IMM1EX
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode10 : ∀i2.MODE_IMM2 = i2 → eq_instrmode MODE_IMM2 i2 = true.
+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)
@@ -476,7 +476,7 @@ nlemma eq_to_eqinstrmode10 : ∀i2.MODE_IMM2 = i2 → eq_instrmode MODE_IMM2 i2
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode11 : ∀i2.MODE_DIR1 = i2 → eq_instrmode MODE_DIR1 i2 = true.
+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)
@@ -484,7 +484,7 @@ nlemma eq_to_eqinstrmode11 : ∀i2.MODE_DIR1 = i2 → eq_instrmode MODE_DIR1 i2
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode12 : ∀i2.MODE_DIR2 = i2 → eq_instrmode MODE_DIR2 i2 = true.
+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)
@@ -492,7 +492,7 @@ nlemma eq_to_eqinstrmode12 : ∀i2.MODE_DIR2 = i2 → eq_instrmode MODE_DIR2 i2
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode13 : ∀i2.MODE_IX0 = i2 → eq_instrmode MODE_IX0 i2 = true.
+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)
@@ -500,7 +500,7 @@ nlemma eq_to_eqinstrmode13 : ∀i2.MODE_IX0 = i2 → eq_instrmode MODE_IX0 i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode14 : ∀i2.MODE_IX1 = i2 → eq_instrmode MODE_IX1 i2 = true.
+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)
@@ -508,7 +508,7 @@ nlemma eq_to_eqinstrmode14 : ∀i2.MODE_IX1 = i2 → eq_instrmode MODE_IX1 i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode15 : ∀i2.MODE_IX2 = i2 → eq_instrmode MODE_IX2 i2 = true.
+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)
@@ -516,7 +516,7 @@ nlemma eq_to_eqinstrmode15 : ∀i2.MODE_IX2 = i2 → eq_instrmode MODE_IX2 i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode16 : ∀i2.MODE_SP1 = i2 → eq_instrmode MODE_SP1 i2 = true.
+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)
@@ -524,7 +524,7 @@ nlemma eq_to_eqinstrmode16 : ∀i2.MODE_SP1 = i2 → eq_instrmode MODE_SP1 i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode17 : ∀i2.MODE_SP2 = i2 → eq_instrmode MODE_SP2 i2 = true.
+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)
@@ -532,7 +532,7 @@ nlemma eq_to_eqinstrmode17 : ∀i2.MODE_SP2 = i2 → eq_instrmode MODE_SP2 i2 =
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_instrmode MODE_DIR1_to_DIR1 i2 = true.
+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)
@@ -540,7 +540,7 @@ nlemma eq_to_eqinstrmode18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_instrmode MODE_IMM1_to_DIR1 i2 = true.
+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)
@@ -548,7 +548,7 @@ nlemma eq_to_eqinstrmode19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_instrmode MODE_IX0p_to_DIR1 i2 = true.
+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)
@@ -556,7 +556,7 @@ nlemma eq_to_eqinstrmode20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_instrmode MODE_DIR1_to_IX0p i2 = true.
+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)
@@ -564,7 +564,7 @@ nlemma eq_to_eqinstrmode21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_instrmode MODE_INHA_and_IMM1 i2 = true.
+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)
@@ -572,7 +572,7 @@ nlemma eq_to_eqinstrmode22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_instrmode MODE
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_instrmode MODE_INHX_and_IMM1 i2 = true.
+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)
@@ -580,7 +580,7 @@ nlemma eq_to_eqinstrmode23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_instrmode MODE
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_instrmode MODE_IMM1_and_IMM1 i2 = true.
+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)
@@ -588,7 +588,7 @@ nlemma eq_to_eqinstrmode24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_instrmode MODE
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_instrmode MODE_DIR1_and_IMM1 i2 = true.
+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)
@@ -596,7 +596,7 @@ nlemma eq_to_eqinstrmode25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_instrmode MODE
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_instrmode MODE_IX0_and_IMM1 i2 = true.
+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)
@@ -604,7 +604,7 @@ nlemma eq_to_eqinstrmode26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_instrmode MODE_IX0p_and_IMM1 i2 = true.
+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)
@@ -612,7 +612,7 @@ nlemma eq_to_eqinstrmode27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_instrmode MODE
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_instrmode MODE_IX1_and_IMM1 i2 = true.
+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)
@@ -620,7 +620,7 @@ nlemma eq_to_eqinstrmode28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_instrmode MODE_IX1p_and_IMM1 i2 = true.
+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)
@@ -628,7 +628,7 @@ nlemma eq_to_eqinstrmode29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_instrmode MODE
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_instrmode MODE_SP1_and_IMM1 i2 = true.
+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)
@@ -636,7 +636,7 @@ nlemma eq_to_eqinstrmode30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_instrmode MODE_
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_instrmode (MODE_DIRn n1) i2 = true.
+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);
@@ -648,7 +648,7 @@ nlemma eq_to_eqinstrmode31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_instrmode (MODE_D
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_instrmode (MODE_DIRn_and_IMM1 n1) i2 = true.
+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);
@@ -660,7 +660,7 @@ nlemma eq_to_eqinstrmode32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_instrmod
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_instrmode (MODE_TNY n1) i2 = true.
+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);
@@ -672,36 +672,36 @@ nlemma eq_to_eqinstrmode33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_instrmode (MODE_TN
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_instrmode (MODE_SRT n1) i2 = true.
+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_bitrig n1 n2 = true);
+     nchange with (eq_bit n1 n2 = true);
      nrewrite > (instr_mode_destruct_MODE_SRT … H);
-     nrewrite > (eq_to_eqbitrig n2 n2 (refl_eq …));
+     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)
  ##]
 nqed.
 
-nlemma eq_to_eqinstrmode : ∀i1,i2.i1 = i2 → eq_instrmode i1 i2 = true.
+nlemma eq_to_eqim : ∀i1,i2.i1 = i2 → eq_im i1 i2 = true.
  #i1; ncases i1;
- ##[ ##1: napply eq_to_eqinstrmode1 ##| ##2: napply eq_to_eqinstrmode2
- ##| ##3: napply eq_to_eqinstrmode3 ##| ##4: napply eq_to_eqinstrmode4
- ##| ##5: napply eq_to_eqinstrmode5 ##| ##6: napply eq_to_eqinstrmode6
- ##| ##7: napply eq_to_eqinstrmode7 ##| ##8: napply eq_to_eqinstrmode8
- ##| ##9: napply eq_to_eqinstrmode9 ##| ##10: napply eq_to_eqinstrmode10 
- ##| ##11: napply eq_to_eqinstrmode11 ##| ##12: napply eq_to_eqinstrmode12
- ##| ##13: napply eq_to_eqinstrmode13 ##| ##14: napply eq_to_eqinstrmode14
- ##| ##15: napply eq_to_eqinstrmode15 ##| ##16: napply eq_to_eqinstrmode16
- ##| ##17: napply eq_to_eqinstrmode17 ##| ##18: napply eq_to_eqinstrmode18
- ##| ##19: napply eq_to_eqinstrmode19 ##| ##20: napply eq_to_eqinstrmode20
- ##| ##21: napply eq_to_eqinstrmode21 ##| ##22: napply eq_to_eqinstrmode22
- ##| ##23: napply eq_to_eqinstrmode23 ##| ##24: napply eq_to_eqinstrmode24
- ##| ##25: napply eq_to_eqinstrmode25 ##| ##26: napply eq_to_eqinstrmode26
- ##| ##27: napply eq_to_eqinstrmode27 ##| ##28: napply eq_to_eqinstrmode28
- ##| ##29: napply eq_to_eqinstrmode29 ##| ##30: napply eq_to_eqinstrmode30
- ##| ##31: napply eq_to_eqinstrmode31 ##| ##32: napply eq_to_eqinstrmode32
- ##| ##33: napply eq_to_eqinstrmode33 ##| ##34: napply eq_to_eqinstrmode34
+ ##[ ##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
  ##]
 nqed.