freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
index 9edad75cc6c025d7315a6a4e06d5dcc2e7c35184..0be7272dbaf48ba9da00e4682636e57bee5e0946 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
@@ -199,7 +199,7 @@ nlemma aluHC05_destruct_13 :
  napply refl_eq.
 nqed.
 
-nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
+nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_aluHC05.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
@@ -229,7 +229,7 @@ nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
  napply refl_eq.
 nqed.
 
-nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = alu2.
+nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_aluHC05 alu1 alu2 = true → alu1 = alu2.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
@@ -270,7 +270,7 @@ nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = al
  napply refl_eq.
 nqed.
 
-nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = true.
+nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC05 alu1 alu2 = true.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
@@ -313,6 +313,198 @@ nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = tr
  napply refl_eq.
 nqed.
 
+nlemma decidable_aluHC05_aux1
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x1 ≠ y1) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux2
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x2 ≠ y2) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux3
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x3 ≠ y3) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_3 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux4
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x4 ≠ y4) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_4 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux5
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x5 ≠ y5) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_5 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux6
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x6 ≠ y6) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_6 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux7
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x7 ≠ y7) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_7 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux8
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x8 ≠ y8) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_8 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux9
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x9 ≠ y9) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_9 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux10
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x10 ≠ y10) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_10 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux11
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x11 ≠ y11) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_11 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux12
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x12 ≠ y12) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_12 … H1)).
+nqed.
+
+nlemma decidable_aluHC05_aux13
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
+ (x13 ≠ y13) →
+ (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
+ (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize; #H; #H1;
+ napply (H (aluHC05_destruct_13 … H1)).
+nqed.
+
+nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y).
+ #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nnormalize;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC05_aux1 … H))
+ ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
+  ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC05_aux2 … H1))
+  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
+   ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC05_aux3 … H2))
+   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
+    ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC05_aux4 … H3))
+    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
+     ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC05_aux5 … H4))
+     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
+      ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC05_aux6 … H5))
+      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
+       ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC05_aux7 … H6))
+       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
+        ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC05_aux8 … H7))
+        ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
+         ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC05_aux9 … H8))
+         ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
+          ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC05_aux10 … H9))
+          ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
+           ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC05_aux11 … H10))
+           ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
+            ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC05_aux12 … H11))
+            ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
+             ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluHC05_aux13 … H12))
+             ##| ##1: #H12; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
+                      nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
+                      nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
+                      nrewrite > H12; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+             ##]
+            ##]
+           ##]
+          ##]
+         ##]
+        ##]
+       ##]
+      ##]
+     ##]
+    ##]
+   ##]
+  ##]
+ ##]
+nqed.
+
 nlemma aluHC08_destruct_1 :
 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
@@ -469,7 +661,7 @@ nlemma aluHC08_destruct_12 :
  napply refl_eq.
 nqed.
 
-nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
+nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_aluHC08.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
@@ -497,7 +689,7 @@ nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
  napply refl_eq.
 nqed.
 
-nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2.
+nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_aluHC08 alu1 alu2 = true → alu1 = alu2.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
@@ -532,7 +724,7 @@ nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = al
  napply refl_eq.
 nqed.
 
-nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true.
+nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC08 alu1 alu2 = true.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
@@ -569,6 +761,184 @@ nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = tr
  napply refl_eq.
 nqed.
 
+nlemma decidable_aluHC08_aux1
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x1 ≠ y1) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux2
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x2 ≠ y2) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux3
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x3 ≠ y3) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_3 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux4
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x4 ≠ y4) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_4 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux5
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x5 ≠ y5) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_5 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux6
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x6 ≠ y6) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_6 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux7
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x7 ≠ y7) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_7 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux8
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x8 ≠ y8) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_8 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux9
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x9 ≠ y9) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_9 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux10
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x10 ≠ y10) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_10 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux11
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x11 ≠ y11) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_11 … H1)).
+nqed.
+
+nlemma decidable_aluHC08_aux12
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
+ (x12 ≠ y12) →
+ (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
+ (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize; #H; #H1;
+ napply (H (aluHC08_destruct_12 … H1)).
+nqed.
+
+nlemma decidable_aluHC08 : ∀x,y:alu_HC08.decidable (x = y).
+ #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nnormalize;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC08_aux1 … H))
+ ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
+  ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC08_aux2 … H1))
+  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …);
+   ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC08_aux3 … H2))
+   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
+    ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC08_aux4 … H3))
+    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
+     ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC08_aux5 … H4))
+     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x6 y6) …);
+      ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC08_aux6 … H5))
+      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
+       ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC08_aux7 … H6))
+       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
+        ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC08_aux8 … H7))
+        ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
+         ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC08_aux9 … H8))
+         ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
+          ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC08_aux10 … H9))
+          ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
+           ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC08_aux11 … H10))
+           ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
+            ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC08_aux12 … H11))
+            ##| ##1: #H11; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
+                      nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
+                      nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
+                      napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+            ##]
+           ##]
+          ##]
+         ##]
+        ##]
+       ##]
+      ##]
+     ##]
+    ##]
+   ##]
+  ##]
+ ##]
+nqed.
+
 nlemma aluRS08_destruct_1 :
 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
@@ -673,7 +1043,7 @@ nlemma aluRS08_destruct_8 :
  napply refl_eq.
 nqed.
 
-nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
+nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_aluRS08.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
@@ -699,7 +1069,7 @@ nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
  napply refl_eq.
 nqed.
 
-nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2.
+nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_aluRS08 alu1 alu2 = true → alu1 = alu2.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
@@ -727,7 +1097,7 @@ nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = al
  napply refl_eq.
 nqed.
 
-nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true.
+nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_aluRS08 alu1 alu2 = true.
  #alu1; #alu2;
  ncases alu1;
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
@@ -757,6 +1127,127 @@ nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = tr
  napply refl_eq.
 nqed.
 
+nlemma decidable_aluRS08_aux1
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x1 ≠ y1) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux2
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x2 ≠ y2) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux3
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x3 ≠ y3) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_3 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux4
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x4 ≠ y4) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_4 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux5
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x5 ≠ y5) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_5 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux6
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x6 ≠ y6) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_6 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux7
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x7 ≠ y7) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_7 … H1)).
+nqed.
+
+nlemma decidable_aluRS08_aux8
+ : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
+ (x8 ≠ y8) →
+ (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
+ (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize; #H; #H1;
+ napply (H (aluRS08_destruct_8 … H1)).
+nqed.
+
+nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
+ #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nnormalize;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_aluRS08_aux1 … H))
+ ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x2 y2) …);
+  ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluRS08_aux2 … H1))
+  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
+   ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluRS08_aux3 … H2))
+   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
+    ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluRS08_aux4 … H3))
+    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x5 y5) …);
+     ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluRS08_aux5 … H4))
+     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x6 y6) …);
+      ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluRS08_aux6 … H5))
+      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
+       ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluRS08_aux7 … H6))
+       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
+        ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluRS08_aux8 … H7))
+        ##| ##1: #H7; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
+                      nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
+                      napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+        ##]
+       ##]
+      ##]
+     ##]
+    ##]
+   ##]
+  ##]
+ ##]
+nqed.
+
 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
  #mcu; #clk1; #clk2;
  ncases clk1;
@@ -902,28 +1393,28 @@ nlemma anystatus_destruct_4 :
  napply refl_eq.
 nqed.
 
-nlemma symmetric_eqstatus :
+nlemma symmetric_eqanystatus :
 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
- eq_status m t s1 s2 addrl = eq_status m t s2 s1 addrl.
+ eq_anystatus m t s1 s2 addrl = eq_anystatus m t s2 s1 addrl.
  #addrl; #m;
  ncases m; #t; #s1;
  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4;
           nchange with (
-           ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
-           ((eq_alu_HC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
+           ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
+           ((eq_aluHC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
            nrewrite > (symmetric_eqaluHC05 x1 y1)
  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4;
           nchange with (
-           ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
-           ((eq_alu_HC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
+           ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
+           ((eq_aluHC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
            nrewrite > (symmetric_eqaluHC08 x1 y1)
  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4;
           nchange with (
-           ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
-           ((eq_alu_RS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
+           ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
+           ((eq_aluRS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
            nrewrite > (symmetric_eqaluRS08 x1 y1)
  ##]
  nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
@@ -931,58 +1422,58 @@ nlemma symmetric_eqstatus :
  napply refl_eq.
 nqed.
 
-nlemma eqstatus_to_eq :
+nlemma eqanystatus_to_eq :
 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
- (eq_status m t s1 s2 addrl = true) →
-  ((alu m t s1 = alu m t s2) ∧
-   (clk_desc m t s1 = clk_desc m t s2) ∧
-   ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
-                            (mem_desc m t s1) (mem_desc m t s2) addrl) = true)).
+ (eq_anystatus m t s1 s2 addrl = true) →
+  And3 (alu m t s1 = alu m t s2) 
+       (clk_desc m t s1 = clk_desc m t s2)
+       ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
+                                (mem_desc m t s1) (mem_desc m t s2) addrl) = true).
  #addrl; #m; #t;
  ncases m; #s1;
  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange in H:(%) with (
-           ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+           ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
            nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange in H:(%) with (
-           ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+           ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
            nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange in H:(%) with (
-           ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+           ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
            nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
  ##]
- nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
+ nchange with (And3 (y1 = y1) (x4 = y4) (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
  nrewrite > (andb_true_true_r … (andb_true_true_l … H));
  nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
- napply (conj … (conj … (refl_eq ? y1) (refl_eq ? y4)) (refl_eq ? true)).
+ napply (conj3 … (refl_eq ? y1) (refl_eq ? y4) (refl_eq ? true)).
 nqed.
 
-nlemma eq_to_eqstatus_strong :
+nlemma eq_to_eqanystatus_strong :
 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
- s1 = s2 → (eq_status m t s1 s2 addrl = true).
+ s1 = s2 → (eq_anystatus m t s1 s2 addrl = true).
  #addrl; #m; #t;
  ncases m;
  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange with (
-           ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+           ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nrewrite > (anystatus_destruct_1 … H);
           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
  ##| ##2,3:  #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange with (
-           ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+           ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nrewrite > (anystatus_destruct_1 … H);
           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange with (
-           ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+           ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nrewrite > (anystatus_destruct_1 … H);
           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
  ##]
@@ -1007,30 +1498,30 @@ nlemma eq_to_eqstatus_strong :
  ##]
 nqed.
 
-nlemma eq_to_eqstatus_weak :
+nlemma eq_to_eqanystatus_weak :
 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
  (alu m t s1 = alu m t s2) →
  (clk_desc m t s1 = clk_desc m t s2) →
  ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
- (eq_status m t s1 s2 addrl = true).
+ (eq_anystatus m t s1 s2 addrl = true).
  #addrl; #m; #t;
  ncases m;
  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
-          nchange with (((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+          nchange with (((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nchange in H:(%) with (x1 = y1);
           nrewrite > H; 
           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
  ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
-          nchange with (((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+          nchange with (((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nchange in H:(%) with (x1 = y1);
           nrewrite > H; 
           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
-          nchange with (((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
+          nchange with (((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nchange in H:(%) with (x1 = y1);
           nrewrite > H; 
           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))