--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* Questo materiale fa parte della tesi: *)
+(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
+(* *)
+(* data ultima modifica 15/11/2007 *)
+(* ********************************************************************** *)
+
+include "freescale/word16_lemmas.ma".
+include "freescale/opcode_base_lemmas1.ma".
+include "freescale/status.ma".
+include "freescale/option_lemmas.ma".
+include "freescale/prod_lemmas.ma".
+
+(* *********************************** *)
+(* STATUS INTERNO DEL PROCESSORE (ALU) *)
+(* *********************************** *)
+
+nlemma aluHC05_destruct_1 :
+∀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.
+ 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 = y1.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_2 :
+∀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.
+ 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 →
+ x2 = y2.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_3 :
+∀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.
+ 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 →
+ x3 = y3.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_4 :
+∀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.
+ 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 →
+ x4 = y4.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_5 :
+∀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.
+ 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 →
+ x5 = y5.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_6 :
+∀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.
+ 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 →
+ x6 = y6.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_7 :
+∀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.
+ 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 →
+ x7 = y7.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_8 :
+∀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.
+ 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 →
+ x8 = y8.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_9 :
+∀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.
+ 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 →
+ x9 = y9.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_10 :
+∀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.
+ 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 →
+ x10 = y10.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_11 :
+∀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.
+ 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 →
+ x11 = y11.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_12 :
+∀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.
+ 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 →
+ x12 = y12.
+ #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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC05_destruct_13 :
+∀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.
+ 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 →
+ x13 = 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; #H;
+ nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
+ with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
+ nchange with (
+ ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
+ (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗ (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
+ (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
+ (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
+ (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗ (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
+ (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
+ (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
+ nrewrite > (symmetric_eqb8 x1 y1);
+ nrewrite > (symmetric_eqb8 x2 y2);
+ nrewrite > (symmetric_eqw16 x3 y3);
+ nrewrite > (symmetric_eqw16 x4 y4);
+ nrewrite > (symmetric_eqw16 x5 y5);
+ nrewrite > (symmetric_eqw16 x6 y6);
+ nrewrite > (symmetric_eqw16 x7 y7);
+ nrewrite > (symmetric_eqbool x8 y8);
+ nrewrite > (symmetric_eqbool x9 y9);
+ nrewrite > (symmetric_eqbool x10 y10);
+ nrewrite > (symmetric_eqbool x11 y11);
+ nrewrite > (symmetric_eqbool x12 y12);
+ nrewrite > (symmetric_eqbool x13 y13);
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = alu2.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
+ nchange in H:(%) with (
+ ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
+ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
+ (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
+ (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
+ (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
+ (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
+ (eq_bool x13 y13)) = true);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
+ nletin H1 ≝ (andb_true_true_l ?? H);
+ nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r ?? (andb_true_true_l ?? H)));
+ nletin H2 ≝ (andb_true_true_l ?? H1);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
+ nletin H3 ≝ (andb_true_true_l ?? H2);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
+ nletin H4 ≝ (andb_true_true_l ?? H3);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
+ nletin H5 ≝ (andb_true_true_l ?? H4);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
+ nletin H6 ≝ (andb_true_true_l ?? H5);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
+ nletin H7 ≝ (andb_true_true_l ?? H6);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
+ nletin H8 ≝ (andb_true_true_l ?? H7);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
+ nletin H9 ≝ (andb_true_true_l ?? H8);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H9));
+ nletin H10 ≝ (andb_true_true_l ?? H9);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H10));
+ nletin H11 ≝ (andb_true_true_l ?? H10);
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H11));
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H11));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = true.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
+ nrewrite > (aluHC05_destruct_1 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_2 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_3 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_4 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_5 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_6 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_7 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_8 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_9 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_10 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_11 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_12 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_13 ?????????????????????????? H);
+ nchange with (
+ ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
+ (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
+ (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
+ (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
+ (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
+ (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
+ (eq_bool y13 y13)) = true);
+ nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
+ nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y6 y6 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y7 y7 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y13 y13 (refl_eq ??));
+ napply (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 →
+ x1 = y1.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_2 :
+∀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 →
+ x2 = y2.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_3 :
+∀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 →
+ x3 = y3.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_4 :
+∀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 →
+ x4 = y4.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_5 :
+∀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 →
+ x5 = y5.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_6 :
+∀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 →
+ x6 = y6.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_7 :
+∀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 →
+ x7 = y7.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_8 :
+∀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 →
+ x8 = y8.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_9 :
+∀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 →
+ x9 = y9.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_10 :
+∀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 →
+ x10 = y10.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_11 :
+∀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 →
+ x11 = y11.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluHC08_destruct_12 :
+∀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 →
+ x12 = 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; #H;
+ nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
+ with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
+ nchange with (
+ ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
+ (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
+ (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
+ ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
+ (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
+ (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
+ nrewrite > (symmetric_eqb8 x1 y1);
+ nrewrite > (symmetric_eqb8 x2 y2);
+ nrewrite > (symmetric_eqb8 x3 y3);
+ nrewrite > (symmetric_eqw16 x4 y4);
+ nrewrite > (symmetric_eqw16 x5 y5);
+ nrewrite > (symmetric_eqbool x6 y6);
+ nrewrite > (symmetric_eqbool x7 y7);
+ nrewrite > (symmetric_eqbool x8 y8);
+ nrewrite > (symmetric_eqbool x9 y9);
+ nrewrite > (symmetric_eqbool x10 y10);
+ nrewrite > (symmetric_eqbool x11 y11);
+ nrewrite > (symmetric_eqbool x12 y12);
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nchange in H:(%) with (
+ ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
+ (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
+ (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
+ nletin H1 ≝ (andb_true_true_l ?? H);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
+ nletin H2 ≝ (andb_true_true_l ?? H1);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
+ nletin H3 ≝ (andb_true_true_l ?? H2);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
+ nletin H4 ≝ (andb_true_true_l ?? H3);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
+ nletin H5 ≝ (andb_true_true_l ?? H4);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
+ nletin H6 ≝ (andb_true_true_l ?? H5);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H6));
+ nletin H7 ≝ (andb_true_true_l ?? H6);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
+ nletin H8 ≝ (andb_true_true_l ?? H7);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
+ nletin H9 ≝ (andb_true_true_l ?? H8);
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H9));
+ nletin H10 ≝ (andb_true_true_l ?? H9);
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H10));
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H10));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
+ nrewrite > (aluHC08_destruct_1 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_2 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_3 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_4 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_5 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_6 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_7 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_8 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_9 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_10 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_11 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_12 ???????????????????????? H);
+ nchange with (
+ ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
+ (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
+ (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
+ nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
+ nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
+ nrewrite > (eq_to_eqb8 y3 y3 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y6 y6 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
+ napply (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 →
+ x1 = y1.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_2 :
+∀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 →
+ x2 = y2.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_3 :
+∀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 →
+ x3 = y3.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_4 :
+∀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 →
+ x4 = y4.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_5 :
+∀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 →
+ x5 = y5.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_6 :
+∀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 →
+ x6 = y6.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_7 :
+∀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 →
+ x7 = y7.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma aluRS08_destruct_8 :
+∀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 →
+ x8 = y8.
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
+ with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
+ nchange with (
+ ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
+ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
+ (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
+ (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
+ ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
+ (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
+ (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
+ (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
+ nrewrite > (symmetric_eqb8 x1 y1);
+ nrewrite > (symmetric_eqw16 x2 y2);
+ nrewrite > (symmetric_eqw16 x3 y3);
+ nrewrite > (symmetric_eqw16 x4 y4);
+ nrewrite > (symmetric_eqb8 x5 y5);
+ nrewrite > (symmetric_eqb8 x6 y6);
+ nrewrite > (symmetric_eqbool x7 y7);
+ nrewrite > (symmetric_eqbool x8 y8);
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nchange in H:(%) with (
+ ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
+ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
+ (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
+ (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
+ nletin H1 ≝ (andb_true_true_l ?? H);
+ nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
+ nletin H2 ≝ (andb_true_true_l ?? H1);
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H2));
+ nletin H3 ≝ (andb_true_true_l ?? H2);
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H3));
+ nletin H4 ≝ (andb_true_true_l ?? H3);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H4));
+ nletin H5 ≝ (andb_true_true_l ?? H4);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H5));
+ nletin H6 ≝ (andb_true_true_l ?? H5);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H6));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true.
+ #alu1; #alu2;
+ ncases alu1;
+ #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
+ ncases alu2;
+ #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
+ nrewrite > (aluRS08_destruct_1 ???????????????? H);
+ nrewrite > (aluRS08_destruct_2 ???????????????? H);
+ nrewrite > (aluRS08_destruct_3 ???????????????? H);
+ nrewrite > (aluRS08_destruct_4 ???????????????? H);
+ nrewrite > (aluRS08_destruct_5 ???????????????? H);
+ nrewrite > (aluRS08_destruct_6 ???????????????? H);
+ nrewrite > (aluRS08_destruct_7 ???????????????? H);
+ nrewrite > (aluRS08_destruct_8 ???????????????? H);
+ nchange with (
+ ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
+ (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
+ (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
+ (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
+ nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y2 y2 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
+ nrewrite > (eq_to_eqb8 y5 y5 (refl_eq ??));
+ nrewrite > (eq_to_eqb8 y6 y6 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
+ nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
+ napply (refl_eq ??).
+nqed.
+
+nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
+ #mcu; #clk1; #clk2;
+ ncases clk1;
+ ncases clk2;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##2,3: nnormalize; #H; napply (refl_eq ??)
+ ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
+ #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
+ nchange with (
+ ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
+ ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
+ nrewrite > (symmetric_eqb8 x1 y1);
+ nrewrite > (symmetric_eqanyop ? x2 y2);
+ nrewrite > (symmetric_eqinstrmode x3 y3);
+ nrewrite > (symmetric_eqb8 x4 y4);
+ nrewrite > (symmetric_eqw16 x5 y5);
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk2.
+ #mcu; #clk1; #clk2;
+ ncases clk1;
+ ncases clk2;
+ ##[ ##1: nnormalize; #H; napply (refl_eq ??)
+ ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct ??? H1)
+ ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
+ #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
+ nchange in H:(%) with (
+ ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
+ nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H));
+ nletin H1 ≝ (andb_true_true_l ?? H);
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H1));
+ nletin H2 ≝ (andb_true_true_l ?? H1);
+ nrewrite > (eqinstrmode_to_eq ?? (andb_true_true_r ?? H2));
+ nletin H3 ≝ (andb_true_true_l ?? H2);
+ nrewrite > (eqanyop_to_eq ??? (andb_true_true_r ?? H3));
+ nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H3));
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = true.
+ #mcu; #clk1; #clk2;
+ ncases clk1;
+ ncases clk2;
+ ##[ ##1: nnormalize; #H; napply (refl_eq ??)
+ ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ?? H1)
+ ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ?? H1)
+ ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
+ #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
+ nrewrite > (quintuple_destruct_1 ??????????????? (option_destruct_some_some ??? H));
+ nrewrite > (quintuple_destruct_2 ??????????????? (option_destruct_some_some ??? H));
+ nrewrite > (quintuple_destruct_3 ??????????????? (option_destruct_some_some ??? H));
+ nrewrite > (quintuple_destruct_4 ??????????????? (option_destruct_some_some ??? H));
+ nrewrite > (quintuple_destruct_5 ??????????????? (option_destruct_some_some ??? H));
+ nchange with (
+ ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
+ nrewrite > (eq_to_eqb8 x1 x1 (refl_eq ??));
+ nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
+ nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq ??));
+ nrewrite > (eq_to_eqb8 x4 x4 (refl_eq ??));
+ nrewrite > (eq_to_eqw16 x5 x5 (refl_eq ??));
+ nnormalize;
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma symmetric_forallmemoryranged :
+∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
+ forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
+ forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
+ #t; #chk1; #chk2; #mem1; #mem2; #addrl;
+ napply (list_ind word16 ??? addrl);
+ ##[ ##1: nnormalize; napply (refl_eq ??)
+ ##| ##2: #a; #l; #H;
+ nchange with (
+ ((eq_option byte8 (mem_read t mem1 chk1 a)
+ (mem_read t mem2 chk2 a) eq_b8) ⊗
+ (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
+ ((eq_option byte8 (mem_read t mem2 chk2 a)
+ (mem_read t mem1 chk1 a) eq_b8) ⊗
+ (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
+ nrewrite > H;
+ nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma anystatus_destruct_1 :
+∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
+ mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
+ x1 = y1.
+ #m; #t;
+ #x1; #x2; #x3; #x4;
+ #y1; #y2; #y3; #y4; #H;
+ nchange with (match mk_any_status m t y1 y2 y3 y4
+ with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma anystatus_destruct_2 :
+∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
+ mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
+ x2 = y2.
+ #m; #t;
+ #x1; #x2; #x3; #x4;
+ #y1; #y2; #y3; #y4; #H;
+ nchange with (match mk_any_status m t y1 y2 y3 y4
+ with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma anystatus_destruct_3 :
+∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
+ mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
+ x3 = y3.
+ #m; #t;
+ #x1; #x2; #x3; #x4;
+ #y1; #y2; #y3; #y4; #H;
+ nchange with (match mk_any_status m t y1 y2 y3 y4
+ with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma anystatus_destruct_4 :
+∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
+ mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
+ x4 = y4.
+ #m; #t;
+ #x1; #x2; #x3; #x4;
+ #y1; #y2; #y3; #y4; #H;
+ nchange with (match mk_any_status m t y1 y2 y3 y4
+ with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma symmetric_eqstatus :
+∀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.
+ #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)));
+ 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)));
+ 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)));
+ nrewrite > (symmetric_eqaluRS08 x1 y1)
+ ##]
+ nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
+ nrewrite > (symmetric_eqclk ? x4 y4);
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqstatus_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)).
+ #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);
+ 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);
+ 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);
+ 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));
+ nrewrite > (andb_true_true_r ?? (andb_true_true_l ?? H));
+ nrewrite > (eqclk_to_eq ??? (andb_true_true_r ?? H));
+ napply (conj ?? (conj ?? (refl_eq ??) (refl_eq ??)) (refl_eq ??)).
+nqed.
+
+nlemma eq_to_eqstatus_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).
+ #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);
+ 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);
+ 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);
+ nrewrite > (anystatus_destruct_1 ?????????? H);
+ nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
+ ##]
+ nrewrite > (anystatus_destruct_2 ?????????? H);
+ nrewrite > (anystatus_destruct_3 ?????????? H);
+ nrewrite > (anystatus_destruct_4 ?????????? H);
+ nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
+ nchange with ((forall_memory_ranged ?????? ⊗ true) =true);
+ nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
+ nchange with (forall_memory_ranged ?????? = true);
+ napply (list_ind word16 ??? addrl);
+ ##[ ##1,3,5,7: nnormalize; napply (refl_eq ??)
+ ##| ##2,4,6,8: #a; #l'; #H;
+ nchange with (
+ ((eq_option byte8 (mem_read t y2 y3 a)
+ (mem_read t y2 y3 a) eq_b8) ⊗
+ (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
+ nrewrite > H;
+ nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq ??));
+ nnormalize;
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqstatus_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).
+ #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 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 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 in H:(%) with (x1 = y1);
+ nrewrite > H;
+ nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
+ ##]
+ nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
+ nrewrite > H2;
+ nchange in H1:(%) with (x4 = y4);
+ nrewrite > H1;
+ nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
projects / helm.git / blobdiff