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 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/word16_lemmas.ma".
24 include "emulator/status/HC05_status.ma".
26 (* *********************************** *)
27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
28 (* *********************************** *)
30 nlemma aluHC05_destruct_1 :
31 ∀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.
32 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 →
34 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
35 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
36 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
37 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
43 nlemma aluHC05_destruct_2 :
44 ∀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.
45 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 →
47 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
48 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
49 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
50 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
56 nlemma aluHC05_destruct_3 :
57 ∀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.
58 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 →
60 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
61 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
62 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
63 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
69 nlemma aluHC05_destruct_4 :
70 ∀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.
71 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 →
73 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
74 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
75 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
76 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
82 nlemma aluHC05_destruct_5 :
83 ∀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.
84 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 →
86 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
87 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
88 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
89 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
95 nlemma aluHC05_destruct_6 :
96 ∀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.
97 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 →
99 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
100 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
101 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
102 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
108 nlemma aluHC05_destruct_7 :
109 ∀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.
110 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 →
112 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
113 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
114 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
115 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
121 nlemma aluHC05_destruct_8 :
122 ∀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.
123 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 →
125 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
126 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
127 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
128 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
134 nlemma aluHC05_destruct_9 :
135 ∀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.
136 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 →
138 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
139 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
140 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
141 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
147 nlemma aluHC05_destruct_10 :
148 ∀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.
149 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 →
151 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
152 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
153 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
154 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
160 nlemma aluHC05_destruct_11 :
161 ∀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.
162 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 →
164 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
165 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
166 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
167 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
173 nlemma aluHC05_destruct_12 :
174 ∀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.
175 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 →
177 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
178 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
179 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
180 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
186 nlemma aluHC05_destruct_13 :
187 ∀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.
188 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 →
190 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
191 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
192 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
193 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
199 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_HC05_alu.
202 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
204 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
206 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
207 (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗ (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
208 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
209 (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
210 (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗ (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
211 (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
212 (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
213 nrewrite > (symmetric_eqb8 x1 y1);
214 nrewrite > (symmetric_eqb8 x2 y2);
215 nrewrite > (symmetric_eqw16 x3 y3);
216 nrewrite > (symmetric_eqw16 x4 y4);
217 nrewrite > (symmetric_eqw16 x5 y5);
218 nrewrite > (symmetric_eqw16 x6 y6);
219 nrewrite > (symmetric_eqw16 x7 y7);
220 nrewrite > (symmetric_eqbool x8 y8);
221 nrewrite > (symmetric_eqbool x9 y9);
222 nrewrite > (symmetric_eqbool x10 y10);
223 nrewrite > (symmetric_eqbool x11 y11);
224 nrewrite > (symmetric_eqbool x12 y12);
225 nrewrite > (symmetric_eqbool x13 y13);
229 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_HC05_alu alu1 alu2 = true → alu1 = alu2.
232 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
234 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
235 nchange in H:(%) with (
236 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
237 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
238 (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
239 (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
240 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
241 (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
242 (eq_bool x13 y13)) = true);
243 nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
244 nletin H1 ≝ (andb_true_true_l … H);
245 nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r … (andb_true_true_l … H)));
246 nletin H2 ≝ (andb_true_true_l … H1);
247 nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
248 nletin H3 ≝ (andb_true_true_l … H2);
249 nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
250 nletin H4 ≝ (andb_true_true_l … H3);
251 nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
252 nletin H5 ≝ (andb_true_true_l … H4);
253 nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
254 nletin H6 ≝ (andb_true_true_l … H5);
255 nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
256 nletin H7 ≝ (andb_true_true_l … H6);
257 nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
258 nletin H8 ≝ (andb_true_true_l … H7);
259 nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
260 nletin H9 ≝ (andb_true_true_l … H8);
261 nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
262 nletin H10 ≝ (andb_true_true_l … H9);
263 nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
264 nletin H11 ≝ (andb_true_true_l … H10);
265 nrewrite > (eqb8_to_eq … (andb_true_true_r … H11));
266 nrewrite > (eqb8_to_eq … (andb_true_true_l … H11));
270 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_HC05_alu alu1 alu2 = true.
273 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
275 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
276 nrewrite > (aluHC05_destruct_1 … H);
277 nrewrite > (aluHC05_destruct_2 … H);
278 nrewrite > (aluHC05_destruct_3 … H);
279 nrewrite > (aluHC05_destruct_4 … H);
280 nrewrite > (aluHC05_destruct_5 … H);
281 nrewrite > (aluHC05_destruct_6 … H);
282 nrewrite > (aluHC05_destruct_7 … H);
283 nrewrite > (aluHC05_destruct_8 … H);
284 nrewrite > (aluHC05_destruct_9 … H);
285 nrewrite > (aluHC05_destruct_10 … H);
286 nrewrite > (aluHC05_destruct_11 … H);
287 nrewrite > (aluHC05_destruct_12 … H);
288 nrewrite > (aluHC05_destruct_13 … H);
290 ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
291 (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
292 (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
293 (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
294 (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
295 (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
296 (eq_bool y13 y13)) = true);
297 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
298 nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
299 nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
300 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
301 nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
302 nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
303 nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
304 nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
305 nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
306 nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
307 nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
308 nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
309 nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
313 nlemma decidable_aluHC05_aux1
314 : ∀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.
316 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
317 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
318 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
319 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
321 napply (H (aluHC05_destruct_1 … H1)).
324 nlemma decidable_aluHC05_aux2
325 : ∀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.
327 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
328 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
329 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
330 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
332 napply (H (aluHC05_destruct_2 … H1)).
335 nlemma decidable_aluHC05_aux3
336 : ∀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.
338 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
339 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
340 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
341 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
343 napply (H (aluHC05_destruct_3 … H1)).
346 nlemma decidable_aluHC05_aux4
347 : ∀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.
349 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
350 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
351 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
352 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
354 napply (H (aluHC05_destruct_4 … H1)).
357 nlemma decidable_aluHC05_aux5
358 : ∀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.
360 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
361 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
362 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
363 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
365 napply (H (aluHC05_destruct_5 … H1)).
368 nlemma decidable_aluHC05_aux6
369 : ∀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.
371 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
372 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
373 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
374 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
376 napply (H (aluHC05_destruct_6 … H1)).
379 nlemma decidable_aluHC05_aux7
380 : ∀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.
382 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
383 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
384 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
385 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
387 napply (H (aluHC05_destruct_7 … H1)).
390 nlemma decidable_aluHC05_aux8
391 : ∀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.
393 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
394 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
395 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
396 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
398 napply (H (aluHC05_destruct_8 … H1)).
401 nlemma decidable_aluHC05_aux9
402 : ∀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.
404 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
405 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
406 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
407 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
409 napply (H (aluHC05_destruct_9 … H1)).
412 nlemma decidable_aluHC05_aux10
413 : ∀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.
415 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
416 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
417 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
418 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
420 napply (H (aluHC05_destruct_10 … H1)).
423 nlemma decidable_aluHC05_aux11
424 : ∀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.
426 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
427 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
428 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
429 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
431 napply (H (aluHC05_destruct_11 … H1)).
434 nlemma decidable_aluHC05_aux12
435 : ∀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.
437 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
438 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
439 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
440 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
442 napply (H (aluHC05_destruct_12 … H1)).
445 nlemma decidable_aluHC05_aux13
446 : ∀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.
448 (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
449 (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
450 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
451 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
453 napply (H (aluHC05_destruct_13 … H1)).
456 nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y).
457 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
458 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
460 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
461 ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC05_aux1 … H))
462 ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
463 ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC05_aux2 … H1))
464 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
465 ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC05_aux3 … H2))
466 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
467 ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC05_aux4 … H3))
468 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
469 ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC05_aux5 … H4))
470 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
471 ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC05_aux6 … H5))
472 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
473 ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC05_aux7 … H6))
474 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
475 ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC05_aux8 … H7))
476 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
477 ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC05_aux9 … H8))
478 ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
479 ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC05_aux10 … H9))
480 ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
481 ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC05_aux11 … H10))
482 ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
483 ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC05_aux12 … H11))
484 ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
485 ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluHC05_aux13 … H12))
486 ##| ##1: #H12; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
487 nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
488 nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
489 nrewrite > H12; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))