1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/word16_lemmas.ma".
24 include "freescale/opcode_base_lemmas1.ma".
25 include "freescale/status.ma".
26 include "common/option_lemmas.ma".
27 include "common/prod_lemmas.ma".
29 (* *********************************** *)
30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
31 (* *********************************** *)
33 nlemma aluHC05_destruct_1 :
34 ∀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.
35 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 →
37 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
38 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
39 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
40 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
46 nlemma aluHC05_destruct_2 :
47 ∀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.
48 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 →
50 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
51 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
52 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
53 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
59 nlemma aluHC05_destruct_3 :
60 ∀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.
61 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 →
63 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
64 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
65 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
66 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
72 nlemma aluHC05_destruct_4 :
73 ∀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.
74 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 →
76 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
77 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
78 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
79 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
85 nlemma aluHC05_destruct_5 :
86 ∀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.
87 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 →
89 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
90 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
91 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
92 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
98 nlemma aluHC05_destruct_6 :
99 ∀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.
100 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 →
102 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
103 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
104 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
105 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
111 nlemma aluHC05_destruct_7 :
112 ∀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.
113 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 →
115 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
116 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
117 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
118 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
124 nlemma aluHC05_destruct_8 :
125 ∀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.
126 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 →
128 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
129 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
130 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
131 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
137 nlemma aluHC05_destruct_9 :
138 ∀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.
139 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 →
141 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
142 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
143 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
144 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
150 nlemma aluHC05_destruct_10 :
151 ∀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.
152 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 →
154 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
155 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
156 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
157 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
163 nlemma aluHC05_destruct_11 :
164 ∀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.
165 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 →
167 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
168 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
169 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
170 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
176 nlemma aluHC05_destruct_12 :
177 ∀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.
178 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 →
180 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
181 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
182 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
183 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
189 nlemma aluHC05_destruct_13 :
190 ∀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.
191 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 →
193 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
194 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
195 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
196 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
202 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_aluHC05.
205 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
207 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
209 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
210 (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗ (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
211 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
212 (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
213 (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗ (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
214 (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
215 (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
216 nrewrite > (symmetric_eqb8 x1 y1);
217 nrewrite > (symmetric_eqb8 x2 y2);
218 nrewrite > (symmetric_eqw16 x3 y3);
219 nrewrite > (symmetric_eqw16 x4 y4);
220 nrewrite > (symmetric_eqw16 x5 y5);
221 nrewrite > (symmetric_eqw16 x6 y6);
222 nrewrite > (symmetric_eqw16 x7 y7);
223 nrewrite > (symmetric_eqbool x8 y8);
224 nrewrite > (symmetric_eqbool x9 y9);
225 nrewrite > (symmetric_eqbool x10 y10);
226 nrewrite > (symmetric_eqbool x11 y11);
227 nrewrite > (symmetric_eqbool x12 y12);
228 nrewrite > (symmetric_eqbool x13 y13);
232 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_aluHC05 alu1 alu2 = true → alu1 = alu2.
235 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
237 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
238 nchange in H:(%) with (
239 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
240 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
241 (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
242 (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
243 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
244 (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
245 (eq_bool x13 y13)) = true);
246 nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
247 nletin H1 ≝ (andb_true_true_l … H);
248 nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r … (andb_true_true_l … H)));
249 nletin H2 ≝ (andb_true_true_l … H1);
250 nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
251 nletin H3 ≝ (andb_true_true_l … H2);
252 nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
253 nletin H4 ≝ (andb_true_true_l … H3);
254 nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
255 nletin H5 ≝ (andb_true_true_l … H4);
256 nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
257 nletin H6 ≝ (andb_true_true_l … H5);
258 nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
259 nletin H7 ≝ (andb_true_true_l … H6);
260 nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
261 nletin H8 ≝ (andb_true_true_l … H7);
262 nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
263 nletin H9 ≝ (andb_true_true_l … H8);
264 nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
265 nletin H10 ≝ (andb_true_true_l … H9);
266 nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
267 nletin H11 ≝ (andb_true_true_l … H10);
268 nrewrite > (eqb8_to_eq … (andb_true_true_r … H11));
269 nrewrite > (eqb8_to_eq … (andb_true_true_l … H11));
273 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC05 alu1 alu2 = true.
276 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
278 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
279 nrewrite > (aluHC05_destruct_1 … H);
280 nrewrite > (aluHC05_destruct_2 … H);
281 nrewrite > (aluHC05_destruct_3 … H);
282 nrewrite > (aluHC05_destruct_4 … H);
283 nrewrite > (aluHC05_destruct_5 … H);
284 nrewrite > (aluHC05_destruct_6 … H);
285 nrewrite > (aluHC05_destruct_7 … H);
286 nrewrite > (aluHC05_destruct_8 … H);
287 nrewrite > (aluHC05_destruct_9 … H);
288 nrewrite > (aluHC05_destruct_10 … H);
289 nrewrite > (aluHC05_destruct_11 … H);
290 nrewrite > (aluHC05_destruct_12 … H);
291 nrewrite > (aluHC05_destruct_13 … H);
293 ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
294 (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
295 (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
296 (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
297 (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
298 (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
299 (eq_bool y13 y13)) = true);
300 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
301 nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
302 nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
303 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
304 nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
305 nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
306 nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
307 nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
308 nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
309 nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
310 nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
311 nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
312 nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
316 nlemma decidable_aluHC05_aux1
317 : ∀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.
319 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
320 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
321 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
322 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
324 napply (H (aluHC05_destruct_1 … H1)).
327 nlemma decidable_aluHC05_aux2
328 : ∀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.
330 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
331 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
332 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
333 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
335 napply (H (aluHC05_destruct_2 … H1)).
338 nlemma decidable_aluHC05_aux3
339 : ∀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.
341 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
342 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
343 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
344 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
346 napply (H (aluHC05_destruct_3 … H1)).
349 nlemma decidable_aluHC05_aux4
350 : ∀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.
352 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
353 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
354 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
355 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
357 napply (H (aluHC05_destruct_4 … H1)).
360 nlemma decidable_aluHC05_aux5
361 : ∀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.
363 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
364 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
365 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
366 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
368 napply (H (aluHC05_destruct_5 … H1)).
371 nlemma decidable_aluHC05_aux6
372 : ∀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.
374 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
375 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
376 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
377 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
379 napply (H (aluHC05_destruct_6 … H1)).
382 nlemma decidable_aluHC05_aux7
383 : ∀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.
385 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
386 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
387 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
388 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
390 napply (H (aluHC05_destruct_7 … H1)).
393 nlemma decidable_aluHC05_aux8
394 : ∀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.
396 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
397 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
398 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
399 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
401 napply (H (aluHC05_destruct_8 … H1)).
404 nlemma decidable_aluHC05_aux9
405 : ∀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.
407 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
408 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
409 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
410 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
412 napply (H (aluHC05_destruct_9 … H1)).
415 nlemma decidable_aluHC05_aux10
416 : ∀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.
418 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
419 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
420 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
421 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
423 napply (H (aluHC05_destruct_10 … H1)).
426 nlemma decidable_aluHC05_aux11
427 : ∀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.
429 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
430 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
431 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
432 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
434 napply (H (aluHC05_destruct_11 … H1)).
437 nlemma decidable_aluHC05_aux12
438 : ∀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.
440 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
441 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
442 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
443 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
445 napply (H (aluHC05_destruct_12 … H1)).
448 nlemma decidable_aluHC05_aux13
449 : ∀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.
451 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
452 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
453 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
454 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
456 napply (H (aluHC05_destruct_13 … H1)).
459 nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y).
460 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
461 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
463 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
464 ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC05_aux1 … H))
465 ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
466 ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC05_aux2 … H1))
467 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
468 ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC05_aux3 … H2))
469 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
470 ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC05_aux4 … H3))
471 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
472 ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC05_aux5 … H4))
473 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
474 ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC05_aux6 … H5))
475 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
476 ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC05_aux7 … H6))
477 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
478 ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC05_aux8 … H7))
479 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
480 ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC05_aux9 … H8))
481 ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
482 ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC05_aux10 … H9))
483 ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
484 ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC05_aux11 … H10))
485 ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
486 ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC05_aux12 … H11))
487 ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
488 ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluHC05_aux13 … H12))
489 ##| ##1: #H12; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
490 nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
491 nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
492 nrewrite > H12; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
508 nlemma aluHC08_destruct_1 :
509 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
510 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 →
512 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
513 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
514 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
515 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
521 nlemma aluHC08_destruct_2 :
522 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
523 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 →
525 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
526 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
527 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
528 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
534 nlemma aluHC08_destruct_3 :
535 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
536 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 →
538 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
539 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
540 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
541 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
547 nlemma aluHC08_destruct_4 :
548 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
549 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 →
551 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
552 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
553 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
554 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
560 nlemma aluHC08_destruct_5 :
561 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
562 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 →
564 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
565 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
566 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
567 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
573 nlemma aluHC08_destruct_6 :
574 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
575 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 →
577 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
578 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
579 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
580 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
586 nlemma aluHC08_destruct_7 :
587 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
588 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 →
590 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
591 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
592 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
593 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
599 nlemma aluHC08_destruct_8 :
600 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
601 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 →
603 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
604 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
605 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
606 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
612 nlemma aluHC08_destruct_9 :
613 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
614 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 →
616 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
617 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
618 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
619 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
625 nlemma aluHC08_destruct_10 :
626 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
627 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 →
629 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
630 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
631 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
632 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
638 nlemma aluHC08_destruct_11 :
639 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
640 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 →
642 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
643 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
644 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
645 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
651 nlemma aluHC08_destruct_12 :
652 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
653 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 →
655 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
656 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
657 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
658 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
664 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_aluHC08.
667 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
669 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
671 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
672 (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
673 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
674 ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
675 (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
676 (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
677 nrewrite > (symmetric_eqb8 x1 y1);
678 nrewrite > (symmetric_eqb8 x2 y2);
679 nrewrite > (symmetric_eqb8 x3 y3);
680 nrewrite > (symmetric_eqw16 x4 y4);
681 nrewrite > (symmetric_eqw16 x5 y5);
682 nrewrite > (symmetric_eqbool x6 y6);
683 nrewrite > (symmetric_eqbool x7 y7);
684 nrewrite > (symmetric_eqbool x8 y8);
685 nrewrite > (symmetric_eqbool x9 y9);
686 nrewrite > (symmetric_eqbool x10 y10);
687 nrewrite > (symmetric_eqbool x11 y11);
688 nrewrite > (symmetric_eqbool x12 y12);
692 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_aluHC08 alu1 alu2 = true → alu1 = alu2.
695 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
697 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
698 nchange in H:(%) with (
699 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
700 (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
701 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
702 nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
703 nletin H1 ≝ (andb_true_true_l … H);
704 nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
705 nletin H2 ≝ (andb_true_true_l … H1);
706 nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
707 nletin H3 ≝ (andb_true_true_l … H2);
708 nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
709 nletin H4 ≝ (andb_true_true_l … H3);
710 nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
711 nletin H5 ≝ (andb_true_true_l … H4);
712 nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
713 nletin H6 ≝ (andb_true_true_l … H5);
714 nrewrite > (eqbool_to_eq … (andb_true_true_r … H6));
715 nletin H7 ≝ (andb_true_true_l … H6);
716 nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
717 nletin H8 ≝ (andb_true_true_l … H7);
718 nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
719 nletin H9 ≝ (andb_true_true_l … H8);
720 nrewrite > (eqb8_to_eq … (andb_true_true_r … H9));
721 nletin H10 ≝ (andb_true_true_l … H9);
722 nrewrite > (eqb8_to_eq … (andb_true_true_r … H10));
723 nrewrite > (eqb8_to_eq … (andb_true_true_l … H10));
727 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC08 alu1 alu2 = true.
730 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
732 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
733 nrewrite > (aluHC08_destruct_1 … H);
734 nrewrite > (aluHC08_destruct_2 … H);
735 nrewrite > (aluHC08_destruct_3 … H);
736 nrewrite > (aluHC08_destruct_4 … H);
737 nrewrite > (aluHC08_destruct_5 … H);
738 nrewrite > (aluHC08_destruct_6 … H);
739 nrewrite > (aluHC08_destruct_7 … H);
740 nrewrite > (aluHC08_destruct_8 … H);
741 nrewrite > (aluHC08_destruct_9 … H);
742 nrewrite > (aluHC08_destruct_10 … H);
743 nrewrite > (aluHC08_destruct_11 … H);
744 nrewrite > (aluHC08_destruct_12 … H);
746 ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
747 (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
748 (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
749 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
750 nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
751 nrewrite > (eq_to_eqb8 y3 y3 (refl_eq …));
752 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
753 nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
754 nrewrite > (eq_to_eqbool y6 y6 (refl_eq …));
755 nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
756 nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
757 nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
758 nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
759 nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
760 nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
764 nlemma decidable_aluHC08_aux1
765 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
767 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
768 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
769 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
770 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
772 napply (H (aluHC08_destruct_1 … H1)).
775 nlemma decidable_aluHC08_aux2
776 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
778 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
779 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
780 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
781 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
783 napply (H (aluHC08_destruct_2 … H1)).
786 nlemma decidable_aluHC08_aux3
787 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
789 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
790 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
791 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
792 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
794 napply (H (aluHC08_destruct_3 … H1)).
797 nlemma decidable_aluHC08_aux4
798 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
800 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
801 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
802 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
803 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
805 napply (H (aluHC08_destruct_4 … H1)).
808 nlemma decidable_aluHC08_aux5
809 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
811 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
812 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
813 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
814 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
816 napply (H (aluHC08_destruct_5 … H1)).
819 nlemma decidable_aluHC08_aux6
820 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
822 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
823 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
824 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
825 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
827 napply (H (aluHC08_destruct_6 … H1)).
830 nlemma decidable_aluHC08_aux7
831 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
833 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
834 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
835 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
836 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
838 napply (H (aluHC08_destruct_7 … H1)).
841 nlemma decidable_aluHC08_aux8
842 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
844 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
845 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
846 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
847 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
849 napply (H (aluHC08_destruct_8 … H1)).
852 nlemma decidable_aluHC08_aux9
853 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
855 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
856 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
857 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
858 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
860 napply (H (aluHC08_destruct_9 … H1)).
863 nlemma decidable_aluHC08_aux10
864 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
866 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
867 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
868 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
869 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
871 napply (H (aluHC08_destruct_10 … H1)).
874 nlemma decidable_aluHC08_aux11
875 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
877 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
878 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
879 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
880 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
882 napply (H (aluHC08_destruct_11 … H1)).
885 nlemma decidable_aluHC08_aux12
886 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
888 (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
889 (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
890 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
891 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
893 napply (H (aluHC08_destruct_12 … H1)).
896 nlemma decidable_aluHC08 : ∀x,y:alu_HC08.decidable (x = y).
897 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
898 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
900 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
901 ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC08_aux1 … H))
902 ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
903 ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC08_aux2 … H1))
904 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …);
905 ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC08_aux3 … H2))
906 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
907 ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC08_aux4 … H3))
908 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
909 ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC08_aux5 … H4))
910 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x6 y6) …);
911 ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC08_aux6 … H5))
912 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
913 ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC08_aux7 … H6))
914 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
915 ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC08_aux8 … H7))
916 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
917 ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC08_aux9 … H8))
918 ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
919 ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC08_aux10 … H9))
920 ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
921 ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC08_aux11 … H10))
922 ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
923 ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC08_aux12 … H11))
924 ##| ##1: #H11; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
925 nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
926 nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
927 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
942 nlemma aluRS08_destruct_1 :
943 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
944 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
946 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
947 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
948 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
949 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
955 nlemma aluRS08_destruct_2 :
956 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
957 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
959 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
960 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
961 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
962 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
968 nlemma aluRS08_destruct_3 :
969 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
970 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
972 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
973 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
974 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
975 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
981 nlemma aluRS08_destruct_4 :
982 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
983 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
985 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
986 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
987 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
988 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
994 nlemma aluRS08_destruct_5 :
995 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
996 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
998 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
999 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1000 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1001 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
1007 nlemma aluRS08_destruct_6 :
1008 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1009 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
1011 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1012 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1013 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1014 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
1020 nlemma aluRS08_destruct_7 :
1021 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1022 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
1024 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1025 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1026 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1027 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
1033 nlemma aluRS08_destruct_8 :
1034 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1035 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
1037 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1038 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1039 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1040 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
1046 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_aluRS08.
1049 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1051 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1053 ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
1054 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
1055 (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
1056 (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
1057 ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
1058 (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
1059 (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
1060 (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
1061 nrewrite > (symmetric_eqb8 x1 y1);
1062 nrewrite > (symmetric_eqw16 x2 y2);
1063 nrewrite > (symmetric_eqw16 x3 y3);
1064 nrewrite > (symmetric_eqw16 x4 y4);
1065 nrewrite > (symmetric_eqb8 x5 y5);
1066 nrewrite > (symmetric_eqb8 x6 y6);
1067 nrewrite > (symmetric_eqbool x7 y7);
1068 nrewrite > (symmetric_eqbool x8 y8);
1072 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_aluRS08 alu1 alu2 = true → alu1 = alu2.
1075 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1077 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1078 nchange in H:(%) with (
1079 ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
1080 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
1081 (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
1082 (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
1083 nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
1084 nletin H1 ≝ (andb_true_true_l … H);
1085 nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
1086 nletin H2 ≝ (andb_true_true_l … H1);
1087 nrewrite > (eqb8_to_eq … (andb_true_true_r … H2));
1088 nletin H3 ≝ (andb_true_true_l … H2);
1089 nrewrite > (eqb8_to_eq … (andb_true_true_r … H3));
1090 nletin H4 ≝ (andb_true_true_l … H3);
1091 nrewrite > (eqw16_to_eq … (andb_true_true_r … H4));
1092 nletin H5 ≝ (andb_true_true_l … H4);
1093 nrewrite > (eqw16_to_eq … (andb_true_true_r … H5));
1094 nletin H6 ≝ (andb_true_true_l … H5);
1095 nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
1096 nrewrite > (eqb8_to_eq … (andb_true_true_l … H6));
1100 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_aluRS08 alu1 alu2 = true.
1103 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1105 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1106 nrewrite > (aluRS08_destruct_1 … H);
1107 nrewrite > (aluRS08_destruct_2 … H);
1108 nrewrite > (aluRS08_destruct_3 … H);
1109 nrewrite > (aluRS08_destruct_4 … H);
1110 nrewrite > (aluRS08_destruct_5 … H);
1111 nrewrite > (aluRS08_destruct_6 … H);
1112 nrewrite > (aluRS08_destruct_7 … H);
1113 nrewrite > (aluRS08_destruct_8 … H);
1115 ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
1116 (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
1117 (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
1118 (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
1119 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
1120 nrewrite > (eq_to_eqw16 y2 y2 (refl_eq …));
1121 nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
1122 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
1123 nrewrite > (eq_to_eqb8 y5 y5 (refl_eq …));
1124 nrewrite > (eq_to_eqb8 y6 y6 (refl_eq …));
1125 nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
1126 nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
1130 nlemma decidable_aluRS08_aux1
1131 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1133 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1134 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1135 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1136 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1137 nnormalize; #H; #H1;
1138 napply (H (aluRS08_destruct_1 … H1)).
1141 nlemma decidable_aluRS08_aux2
1142 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1144 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1145 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1146 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1147 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1148 nnormalize; #H; #H1;
1149 napply (H (aluRS08_destruct_2 … H1)).
1152 nlemma decidable_aluRS08_aux3
1153 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1155 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1156 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1157 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1158 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1159 nnormalize; #H; #H1;
1160 napply (H (aluRS08_destruct_3 … H1)).
1163 nlemma decidable_aluRS08_aux4
1164 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1166 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1167 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1168 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1169 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1170 nnormalize; #H; #H1;
1171 napply (H (aluRS08_destruct_4 … H1)).
1174 nlemma decidable_aluRS08_aux5
1175 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1177 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1178 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1179 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1180 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1181 nnormalize; #H; #H1;
1182 napply (H (aluRS08_destruct_5 … H1)).
1185 nlemma decidable_aluRS08_aux6
1186 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1188 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1189 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1190 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1191 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1192 nnormalize; #H; #H1;
1193 napply (H (aluRS08_destruct_6 … H1)).
1196 nlemma decidable_aluRS08_aux7
1197 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1199 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1200 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1201 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1202 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1203 nnormalize; #H; #H1;
1204 napply (H (aluRS08_destruct_7 … H1)).
1207 nlemma decidable_aluRS08_aux8
1208 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1210 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1211 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1212 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1213 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1214 nnormalize; #H; #H1;
1215 napply (H (aluRS08_destruct_8 … H1)).
1218 nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
1219 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1220 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1222 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
1223 ##[ ##2: #H; napply (or2_intro2 … (decidable_aluRS08_aux1 … H))
1224 ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x2 y2) …);
1225 ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluRS08_aux2 … H1))
1226 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
1227 ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluRS08_aux3 … H2))
1228 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
1229 ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluRS08_aux4 … H3))
1230 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x5 y5) …);
1231 ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluRS08_aux5 … H4))
1232 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x6 y6) …);
1233 ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluRS08_aux6 … H5))
1234 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
1235 ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluRS08_aux7 … H6))
1236 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
1237 ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluRS08_aux8 … H7))
1238 ##| ##1: #H7; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
1239 nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
1240 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
1251 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
1255 ##[ ##1: napply refl_eq
1256 ##| ##2,3: nnormalize; #H; napply refl_eq
1257 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
1258 #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
1260 ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
1261 ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_im x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
1262 nrewrite > (symmetric_eqb8 x1 y1);
1263 nrewrite > (symmetric_eqanyop ? x2 y2);
1264 nrewrite > (symmetric_eqim x3 y3);
1265 nrewrite > (symmetric_eqb8 x4 y4);
1266 nrewrite > (symmetric_eqw16 x5 y5);
1271 nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk2.
1275 ##[ ##1: nnormalize; #H; napply refl_eq
1276 ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct … H1)
1277 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
1278 #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
1279 nchange in H:(%) with (
1280 ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
1281 nrewrite > (eqw16_to_eq … (andb_true_true_r … H));
1282 nletin H1 ≝ (andb_true_true_l … H);
1283 nrewrite > (eqb8_to_eq … (andb_true_true_r … H1));
1284 nletin H2 ≝ (andb_true_true_l … H1);
1285 nrewrite > (eqim_to_eq … (andb_true_true_r … H2));
1286 nletin H3 ≝ (andb_true_true_l … H2);
1287 nrewrite > (eqanyop_to_eq … (andb_true_true_r … H3));
1288 nrewrite > (eqb8_to_eq … (andb_true_true_l … H3));
1293 nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = true.
1297 ##[ ##1: nnormalize; #H; napply refl_eq
1298 ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ? p … H1)
1299 ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ? p … H1)
1300 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
1301 #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
1302 nrewrite > (quintuple_destruct_1 … (option_destruct_some_some … H));
1303 nrewrite > (quintuple_destruct_2 … (option_destruct_some_some … H));
1304 nrewrite > (quintuple_destruct_3 … (option_destruct_some_some … H));
1305 nrewrite > (quintuple_destruct_4 … (option_destruct_some_some … H));
1306 nrewrite > (quintuple_destruct_5 … (option_destruct_some_some … H));
1308 ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_im x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
1309 nrewrite > (eq_to_eqb8 x1 x1 (refl_eq …));
1310 nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
1311 nrewrite > (eq_to_eqim x3 x3 (refl_eq …));
1312 nrewrite > (eq_to_eqb8 x4 x4 (refl_eq …));
1313 nrewrite > (eq_to_eqw16 x5 x5 (refl_eq …));
1319 nlemma symmetric_forallmemoryranged :
1320 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
1321 forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
1322 forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
1323 #t; #chk1; #chk2; #mem1; #mem2; #addrl;
1324 napply (list_ind word16 … addrl);
1325 ##[ ##1: nnormalize; napply refl_eq
1326 ##| ##2: #a; #l; #H;
1328 ((eq_option byte8 (mem_read t mem1 chk1 a)
1329 (mem_read t mem2 chk2 a) eq_b8) ⊗
1330 (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
1331 ((eq_option byte8 (mem_read t mem2 chk2 a)
1332 (mem_read t mem1 chk1 a) eq_b8) ⊗
1333 (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
1335 nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
1340 nlemma anystatus_destruct_1 :
1341 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1342 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1346 #y1; #y2; #y3; #y4; #H;
1347 nchange with (match mk_any_status m t y1 y2 y3 y4
1348 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
1354 nlemma anystatus_destruct_2 :
1355 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1356 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1360 #y1; #y2; #y3; #y4; #H;
1361 nchange with (match mk_any_status m t y1 y2 y3 y4
1362 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
1368 nlemma anystatus_destruct_3 :
1369 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1370 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1374 #y1; #y2; #y3; #y4; #H;
1375 nchange with (match mk_any_status m t y1 y2 y3 y4
1376 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
1382 nlemma anystatus_destruct_4 :
1383 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1384 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1388 #y1; #y2; #y3; #y4; #H;
1389 nchange with (match mk_any_status m t y1 y2 y3 y4
1390 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
1396 nlemma symmetric_eqanystatus :
1397 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1398 eq_anystatus m t s1 s2 addrl = eq_anystatus m t s2 s1 addrl.
1401 ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
1402 #s2; ncases s2; #y1; #y2; #y3; #y4;
1404 ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
1405 ((eq_aluHC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
1406 nrewrite > (symmetric_eqaluHC05 x1 y1)
1407 ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
1408 #s2; ncases s2; #y1; #y2; #y3; #y4;
1410 ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
1411 ((eq_aluHC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
1412 nrewrite > (symmetric_eqaluHC08 x1 y1)
1413 ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
1414 #s2; ncases s2; #y1; #y2; #y3; #y4;
1416 ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
1417 ((eq_aluRS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
1418 nrewrite > (symmetric_eqaluRS08 x1 y1)
1420 nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
1421 nrewrite > (symmetric_eqclk ? x4 y4);
1425 nlemma eqanystatus_to_eq :
1426 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1427 (eq_anystatus m t s1 s2 addrl = true) →
1428 And3 (alu m t s1 = alu m t s2)
1429 (clk_desc m t s1 = clk_desc m t s2)
1430 ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1431 (mem_desc m t s1) (mem_desc m t s2) addrl) = true).
1434 ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
1435 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1436 nchange in H:(%) with (
1437 ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1438 nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
1439 ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
1440 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1441 nchange in H:(%) with (
1442 ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1443 nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
1444 ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
1445 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1446 nchange in H:(%) with (
1447 ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1448 nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
1450 nchange with (And3 (y1 = y1) (x4 = y4) (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
1451 nrewrite > (andb_true_true_r … (andb_true_true_l … H));
1452 nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
1453 napply (conj3 … (refl_eq ? y1) (refl_eq ? y4) (refl_eq ? true)).
1456 nlemma eq_to_eqanystatus_strong :
1457 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1458 s1 = s2 → (eq_anystatus m t s1 s2 addrl = true).
1461 ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1462 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1464 ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1465 nrewrite > (anystatus_destruct_1 … H);
1466 nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
1467 ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
1468 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1470 ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1471 nrewrite > (anystatus_destruct_1 … H);
1472 nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
1473 ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1474 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1476 ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1477 nrewrite > (anystatus_destruct_1 … H);
1478 nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
1480 nrewrite > (anystatus_destruct_2 … H);
1481 nrewrite > (anystatus_destruct_3 … H);
1482 nrewrite > (anystatus_destruct_4 … H);
1483 nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
1484 nchange with ((forall_memory_ranged … ⊗ true) =true);
1485 nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
1486 nchange with ((forall_memory_ranged t y3 y3 y2 y2 ?) = true);
1487 napply (list_ind word16 … addrl);
1488 ##[ ##1,3,5,7: nnormalize; napply refl_eq
1489 ##| ##2,4,6,8: #a; #l'; #H;
1491 ((eq_option byte8 (mem_read t y2 y3 a)
1492 (mem_read t y2 y3 a) eq_b8) ⊗
1493 (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
1495 nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq …));
1501 nlemma eq_to_eqanystatus_weak :
1502 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1503 (alu m t s1 = alu m t s2) →
1504 (clk_desc m t s1 = clk_desc m t s2) →
1505 ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1506 (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
1507 (eq_anystatus m t s1 s2 addrl = true).
1510 ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1511 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1512 nchange with (((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1513 nchange in H:(%) with (x1 = y1);
1515 nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
1516 ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
1517 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1518 nchange with (((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1519 nchange in H:(%) with (x1 = y1);
1521 nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
1522 ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1523 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1524 nchange with (((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1525 nchange in H:(%) with (x1 = y1);
1527 nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
1529 nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
1531 nchange in H1:(%) with (x4 = y4);
1533 nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));