]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/emulator/status/HC05_status_lemmas.ma
mod change (-x)
[helm.git] / matita / matita / contribs / ng_assembly / emulator / status / HC05_status_lemmas.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/word16_lemmas.ma".
24 include "emulator/status/HC05_status.ma".
25
26 (* *********************************** *)
27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
28 (* *********************************** *)
29
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 →
33  x1 = y1.
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 ]);
38  nrewrite < H;
39  nnormalize;
40  napply refl_eq.
41 nqed.
42
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 →
46  x2 = y2.
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 ]);
51  nrewrite < H;
52  nnormalize;
53  napply refl_eq.
54 nqed.
55
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 →
59  x3 = y3.
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 ]);
64  nrewrite < H;
65  nnormalize;
66  napply refl_eq.
67 nqed.
68
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 →
72  x4 = y4.
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 ]);
77  nrewrite < H;
78  nnormalize;
79  napply refl_eq.
80 nqed.
81
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 →
85  x5 = y5.
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 ]);
90  nrewrite < H;
91  nnormalize;
92  napply refl_eq.
93 nqed.
94
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 →
98  x6 = y6.
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 ]);
103  nrewrite < H;
104  nnormalize;
105  napply refl_eq.
106 nqed.
107
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 →
111  x7 = y7.
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 ]);
116  nrewrite < H;
117  nnormalize;
118  napply refl_eq.
119 nqed.
120
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 →
124  x8 = y8.
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 ]);
129  nrewrite < H;
130  nnormalize;
131  napply refl_eq.
132 nqed.
133
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 →
137  x9 = y9.
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 ]);
142  nrewrite < H;
143  nnormalize;
144  napply refl_eq.
145 nqed.
146
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 →
150  x10 = y10.
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 ]);
155  nrewrite < H;
156  nnormalize;
157  napply refl_eq.
158 nqed.
159
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 →
163  x11 = y11.
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 ]);
168  nrewrite < H;
169  nnormalize;
170  napply refl_eq.
171 nqed.
172
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 →
176  x12 = y12.
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 ]);
181  nrewrite < H;
182  nnormalize;
183  napply refl_eq.
184 nqed.
185
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 →
189  x13 = 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 ]);
194  nrewrite < H;
195  nnormalize;
196  napply refl_eq.
197 nqed.
198
199 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_HC05_alu.
200  #alu1; #alu2;
201  ncases alu1;
202  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
203  ncases alu2;
204  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
205  nchange with (
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);
226  napply refl_eq.
227 nqed.
228
229 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_HC05_alu alu1 alu2 = true → alu1 = alu2.
230  #alu1; #alu2;
231  ncases alu1;
232  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
233  ncases alu2;
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));
267  napply refl_eq.
268 nqed.
269
270 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_HC05_alu alu1 alu2 = true.
271  #alu1; #alu2;
272  ncases alu1;
273  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
274  ncases alu2;
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);
289  nchange with (
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 …));
310  napply refl_eq.
311 nqed.
312
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.
315  (x1 ≠ y1) →
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;
320  nnormalize; #H; #H1;
321  napply (H (aluHC05_destruct_1 … H1)).
322 nqed.
323
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.
326  (x2 ≠ y2) →
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;
331  nnormalize; #H; #H1;
332  napply (H (aluHC05_destruct_2 … H1)).
333 nqed.
334
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.
337  (x3 ≠ y3) →
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;
342  nnormalize; #H; #H1;
343  napply (H (aluHC05_destruct_3 … H1)).
344 nqed.
345
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.
348  (x4 ≠ y4) →
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;
353  nnormalize; #H; #H1;
354  napply (H (aluHC05_destruct_4 … H1)).
355 nqed.
356
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.
359  (x5 ≠ y5) →
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;
364  nnormalize; #H; #H1;
365  napply (H (aluHC05_destruct_5 … H1)).
366 nqed.
367
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.
370  (x6 ≠ y6) →
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;
375  nnormalize; #H; #H1;
376  napply (H (aluHC05_destruct_6 … H1)).
377 nqed.
378
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.
381  (x7 ≠ y7) →
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;
386  nnormalize; #H; #H1;
387  napply (H (aluHC05_destruct_7 … H1)).
388 nqed.
389
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.
392  (x8 ≠ y8) →
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;
397  nnormalize; #H; #H1;
398  napply (H (aluHC05_destruct_8 … H1)).
399 nqed.
400
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.
403  (x9 ≠ y9) →
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;
408  nnormalize; #H; #H1;
409  napply (H (aluHC05_destruct_9 … H1)).
410 nqed.
411
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.
414  (x10 ≠ y10) →
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;
419  nnormalize; #H; #H1;
420  napply (H (aluHC05_destruct_10 … H1)).
421 nqed.
422
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.
425  (x11 ≠ y11) →
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;
430  nnormalize; #H; #H1;
431  napply (H (aluHC05_destruct_11 … H1)).
432 nqed.
433
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.
436  (x12 ≠ y12) →
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;
441  nnormalize; #H; #H1;
442  napply (H (aluHC05_destruct_12 … H1)).
443 nqed.
444
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.
447  (x13 ≠ 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;
452  nnormalize; #H; #H1;
453  napply (H (aluHC05_destruct_13 … H1)).
454 nqed.
455
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;
459  nnormalize;
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 …))
490              ##]
491             ##]
492            ##]
493           ##]
494          ##]
495         ##]
496        ##]
497       ##]
498      ##]
499     ##]
500    ##]
501   ##]
502  ##]
503 nqed.