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/oct_lemmas.ma".
24 include "num/word16_lemmas.ma".
25 include "num/word24_lemmas.ma".
26 include "emulator/status/IP2022_status.ma".
27 include "emulator/memory/memory_struct_lemmas.ma".
29 (* *********************************** *)
30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
31 (* *********************************** *)
33 nlemma aluIP2022_destruct_1 :
34 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
35 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
36 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
38 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
39 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
40 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
41 with [ mk_alu_IP2022 a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
47 nlemma aluIP2022_destruct_2 :
48 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
49 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
50 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
52 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
53 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
54 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
55 with [ mk_alu_IP2022 _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
61 nlemma aluIP2022_destruct_3 :
62 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
63 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
64 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
66 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
67 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
68 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
69 with [ mk_alu_IP2022 _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
75 nlemma aluIP2022_destruct_4 :
76 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
77 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
78 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
80 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
81 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
82 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
83 with [ mk_alu_IP2022 _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
89 nlemma aluIP2022_destruct_5 :
90 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
91 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
92 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
94 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
95 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
96 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
97 with [ mk_alu_IP2022 _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
103 nlemma aluIP2022_destruct_6 :
104 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
105 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
106 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
108 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
109 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
110 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
111 with [ mk_alu_IP2022 _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
117 nlemma aluIP2022_destruct_7 :
118 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
119 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
120 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
122 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
123 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
124 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
125 with [ mk_alu_IP2022 _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
131 nlemma aluIP2022_destruct_8 :
132 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
133 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
134 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
136 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
137 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
138 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
139 with [ mk_alu_IP2022 _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
145 nlemma aluIP2022_destruct_9 :
146 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
147 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
148 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
150 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
151 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
152 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
153 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
159 nlemma aluIP2022_destruct_10 :
160 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
161 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
162 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
164 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
165 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
166 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
167 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
173 nlemma aluIP2022_destruct_11 :
174 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
175 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
176 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
178 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
179 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
180 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
181 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
187 nlemma aluIP2022_destruct_12 :
188 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
189 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
190 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
192 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
193 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
194 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
195 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
201 nlemma aluIP2022_destruct_13 :
202 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
203 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
204 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
206 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
207 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
208 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
209 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
215 nlemma aluIP2022_destruct_14 :
216 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
217 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
218 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
220 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
221 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
222 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
223 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
229 nlemma aluIP2022_destruct_15 :
230 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
231 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
232 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
234 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
235 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
236 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
237 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
243 nlemma aluIP2022_destruct_16 :
244 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
245 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
246 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
248 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
249 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
250 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
251 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
257 naxiom symmetric_eqaluIP2022 : symmetricT alu_IP2022 bool eq_IP2022_alu.
258 (* !!! la compilazione avviene ma il tempo e' troppo lungo...
260 #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
262 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
264 ((eq_b8 z1 y1) ⊗ (eq_b8 z2 y2) ⊗ (eq_b8 z3 y3) ⊗ (eq_ar8 ? eq_w24 z4 y4) ⊗
265 (eq_ar16 ? eq_w16 z5 y5) ⊗ (eq_w16 z6 y6) ⊗ (eq_w16 z7 y7) ⊗ (eq_w16 z8 y8) ⊗
266 (eq_w16 z9 y9) ⊗ (eq_w16 z10 y10) ⊗ (eq_ex z11 y11) ⊗ (eq_oct z12 y12) ⊗
267 (eq_bool z13 y13) ⊗ (eq_bool z14 y14) ⊗ (eq_bool z15 y15) ⊗ (eq_bool z16 y16)) =
268 ((eq_b8 y1 z1) ⊗ (eq_b8 y2 z2) ⊗ (eq_b8 y3 z3) ⊗ (eq_ar8 ? eq_w24 y4 z4) ⊗
269 (eq_ar16 ? eq_w16 y5 z5) ⊗ (eq_w16 y6 z6) ⊗ (eq_w16 y7 z7) ⊗ (eq_w16 y8 z8) ⊗
270 (eq_w16 y9 z9) ⊗ (eq_w16 y10 z10) ⊗ (eq_ex y11 z11) ⊗ (eq_oct y12 z12) ⊗
271 (eq_bool y13 z13) ⊗ (eq_bool y14 z14) ⊗ (eq_bool y15 z15) ⊗ (eq_bool y16 z16)));
272 nrewrite > (symmetric_eqb8 z1 y1);
273 nrewrite > (symmetric_eqb8 z2 y2);
274 nrewrite > (symmetric_eqb8 z3 y3);
275 nrewrite > (symmetric_eqar8 ? eq_w24 symmetric_eqw24 z4 y4);
276 nrewrite > (symmetric_eqar16 ? eq_w16 symmetric_eqw16 z5 y5);
277 nrewrite > (symmetric_eqw16 z6 y6);
278 nrewrite > (symmetric_eqw16 z7 y7);
279 nrewrite > (symmetric_eqw16 z8 y8);
280 nrewrite > (symmetric_eqw16 z9 y9);
281 nrewrite > (symmetric_eqw16 z10 y10);
282 nrewrite > (symmetric_eqex z11 y11);
283 nrewrite > (symmetric_eqoct z12 y12);
284 nrewrite > (symmetric_eqbool z13 y13);
285 nrewrite > (symmetric_eqbool z14 y14);
286 nrewrite > (symmetric_eqbool z15 y15);
287 nrewrite > (symmetric_eqbool z16 y16);
292 nlemma eqaluIP2022_to_eq : ∀alu1,alu2.eq_IP2022_alu alu1 alu2 = true → alu1 = alu2.
294 #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
296 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
297 nchange in H:(%) with (
298 ((eq_b8 z1 y1) ⊗ (eq_b8 z2 y2) ⊗ (eq_b8 z3 y3) ⊗ (eq_ar8 ? eq_w24 z4 y4) ⊗
299 (eq_ar16 ? eq_w16 z5 y5) ⊗ (eq_w16 z6 y6) ⊗ (eq_w16 z7 y7) ⊗ (eq_w16 z8 y8) ⊗
300 (eq_w16 z9 y9) ⊗ (eq_w16 z10 y10) ⊗ (eq_ex z11 y11) ⊗ (eq_oct z12 y12) ⊗
301 (eq_bool z13 y13) ⊗ (eq_bool z14 y14) ⊗ (eq_bool z15 y15) ⊗ (eq_bool z16 y16)) = true);
302 nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
303 nletin H1 ≝ (andb_true_true_l … H);
304 nrewrite > (eqbool_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
305 nletin H2 ≝ (andb_true_true_l … H1);
306 nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
307 nletin H3 ≝ (andb_true_true_l … H2);
308 nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
309 nletin H4 ≝ (andb_true_true_l … H3);
310 nrewrite > (eqoct_to_eq … (andb_true_true_r … H4));
311 nletin H5 ≝ (andb_true_true_l … H4);
312 nrewrite > (eqex_to_eq … (andb_true_true_r … H5));
313 nletin H6 ≝ (andb_true_true_l … H5);
314 nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
315 nletin H7 ≝ (andb_true_true_l … H6);
316 nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
317 nletin H8 ≝ (andb_true_true_l … H7);
318 nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
319 nletin H9 ≝ (andb_true_true_l … H8);
320 nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
321 nletin H10 ≝ (andb_true_true_l … H9);
322 nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
323 nletin H11 ≝ (andb_true_true_l … H10);
324 nrewrite > (eqar16_to_eq ? eq_w16 eqw16_to_eq … (andb_true_true_r … H11));
325 nletin H12 ≝ (andb_true_true_l … H11);
326 nrewrite > (eqar8_to_eq ? eq_w24 eqw24_to_eq … (andb_true_true_r … H12));
327 nletin H13 ≝ (andb_true_true_l … H12);
328 nrewrite > (eqb8_to_eq … (andb_true_true_r … H13));
329 nletin H14 ≝ (andb_true_true_l … H13);
330 nrewrite > (eqb8_to_eq … (andb_true_true_r … H14));
331 nrewrite > (eqb8_to_eq … (andb_true_true_l … H14));
335 naxiom eq_to_eqaluIP2022 : ∀alu1,alu2.alu1 = alu2 → eq_IP2022_alu alu1 alu2 = true.
336 (* !!! la compilazione avviene ma il tempo e' troppo lungo...
338 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
340 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
341 nrewrite > (aluIP2022_destruct_1 … H);
342 nrewrite > (aluIP2022_destruct_2 … H);
343 nrewrite > (aluIP2022_destruct_3 … H);
344 nrewrite > (aluIP2022_destruct_4 … H);
345 nrewrite > (aluIP2022_destruct_5 … H);
346 nrewrite > (aluIP2022_destruct_6 … H);
347 nrewrite > (aluIP2022_destruct_7 … H);
348 nrewrite > (aluIP2022_destruct_8 … H);
349 nrewrite > (aluIP2022_destruct_9 … H);
350 nrewrite > (aluIP2022_destruct_10 … H);
351 nrewrite > (aluIP2022_destruct_11 … H);
352 nrewrite > (aluIP2022_destruct_12 … H);
353 nrewrite > (aluIP2022_destruct_13 … H);
354 nrewrite > (aluIP2022_destruct_14 … H);
355 nrewrite > (aluIP2022_destruct_15 … H);
356 nrewrite > (aluIP2022_destruct_16 … H);
358 ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_ar8 ? eq_w24 y4 y4) ⊗
359 (eq_ar16 ? eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗ (eq_w16 y7 y7) ⊗ (eq_w16 y8 y8) ⊗
360 (eq_w16 y9 y9) ⊗ (eq_w16 y10 y10) ⊗ (eq_ex y11 y11) ⊗ (eq_oct y12 y12) ⊗
361 (eq_bool y13 y13) ⊗ (eq_bool y14 y14) ⊗ (eq_bool y15 y15) ⊗ (eq_bool y16 y16)) = true);
362 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
363 nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
364 nrewrite > (eq_to_eqb8 y3 y3 (refl_eq …));
365 nrewrite > (eq_to_eqar8 ? eq_w24 eq_to_eqw24 y4 y4 (refl_eq …));
366 nrewrite > (eq_to_eqar16 ? eq_w16 eq_to_eqw16 y5 y5 (refl_eq …));
367 nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
368 nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
369 nrewrite > (eq_to_eqw16 y8 y8 (refl_eq …));
370 nrewrite > (eq_to_eqw16 y9 y9 (refl_eq …));
371 nrewrite > (eq_to_eqw16 y10 y10 (refl_eq …));
372 nrewrite > (eq_to_ex y11 y11 (refl_eq …));
373 nrewrite > (eq_to_oct y12 y12 (refl_eq …));
374 nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
375 nrewrite > (eq_to_eqbool y14 y14 (refl_eq …));
376 nrewrite > (eq_to_eqbool y15 y15 (refl_eq …));
377 nrewrite > (eq_to_eqbool y16 y16 (refl_eq …));
382 nlemma decidable_aluIP2022_aux1
383 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
385 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
386 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
387 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
388 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
390 napply (H (aluIP2022_destruct_1 … H1)).
393 nlemma decidable_aluIP2022_aux2
394 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
396 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
397 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
398 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
399 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
401 napply (H (aluIP2022_destruct_2 … H1)).
404 nlemma decidable_aluIP2022_aux3
405 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
407 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
408 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
409 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
410 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
412 napply (H (aluIP2022_destruct_3 … H1)).
415 nlemma decidable_aluIP2022_aux4
416 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
418 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
419 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
420 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
421 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
423 napply (H (aluIP2022_destruct_4 … H1)).
426 nlemma decidable_aluIP2022_aux5
427 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
429 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
430 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
431 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
432 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
434 napply (H (aluIP2022_destruct_5 … H1)).
437 nlemma decidable_aluIP2022_aux6
438 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
440 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
441 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
442 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
443 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
445 napply (H (aluIP2022_destruct_6 … H1)).
448 nlemma decidable_aluIP2022_aux7
449 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
451 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
452 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
453 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
454 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
456 napply (H (aluIP2022_destruct_7 … H1)).
459 nlemma decidable_aluIP2022_aux8
460 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
462 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
463 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
464 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
465 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
467 napply (H (aluIP2022_destruct_8 … H1)).
470 nlemma decidable_aluIP2022_aux9
471 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
473 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
474 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
475 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
476 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
478 napply (H (aluIP2022_destruct_9 … H1)).
481 nlemma decidable_aluIP2022_aux10
482 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
484 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
485 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
486 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
487 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
489 napply (H (aluIP2022_destruct_10 … H1)).
492 nlemma decidable_aluIP2022_aux11
493 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
495 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
496 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
497 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
498 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
500 napply (H (aluIP2022_destruct_11 … H1)).
503 nlemma decidable_aluIP2022_aux12
504 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
506 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
507 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
508 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
509 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
511 napply (H (aluIP2022_destruct_12 … H1)).
514 nlemma decidable_aluIP2022_aux13
515 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
517 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
518 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
519 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
520 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
522 napply (H (aluIP2022_destruct_13 … H1)).
525 nlemma decidable_aluIP2022_aux14
526 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
528 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
529 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
530 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
531 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
533 napply (H (aluIP2022_destruct_14 … H1)).
536 nlemma decidable_aluIP2022_aux15
537 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
539 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
540 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
541 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
542 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
544 napply (H (aluIP2022_destruct_15 … H1)).
547 nlemma decidable_aluIP2022_aux16
548 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
550 (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
551 (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
552 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
553 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
555 napply (H (aluIP2022_destruct_16 … H1)).
558 nlemma decidable_aluIP2022 : ∀x,y:alu_IP2022.decidable (x = y).
559 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
560 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
562 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
563 ##[ ##2: #H; napply (or2_intro2 … (decidable_aluIP2022_aux1 … H))
564 ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
565 ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluIP2022_aux2 … H1))
566 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …);
567 ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluIP2022_aux3 … H2))
568 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ar8 ? decidable_w24 x4 y4) …);
569 ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluIP2022_aux4 … H3))
570 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ar16 ? decidable_w16 x5 y5) …);
571 ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluIP2022_aux5 … H4))
572 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
573 ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluIP2022_aux6 … H5))
574 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
575 ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluIP2022_aux7 … H6))
576 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x8 y8) …);
577 ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluIP2022_aux8 … H7))
578 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x9 y9) …);
579 ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluIP2022_aux9 … H8))
580 ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x10 y10) …);
581 ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluIP2022_aux10 … H9))
582 ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ex x11 y11) …);
583 ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluIP2022_aux11 … H10))
584 ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct x12 y12) …);
585 ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluIP2022_aux12 … H11))
586 ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
587 ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluIP2022_aux13 … H12))
588 ##| ##1: #H12; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x14 y14) …);
589 ##[ ##2: #H13; napply (or2_intro2 … (decidable_aluIP2022_aux14 … H13))
590 ##| ##1: #H13; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x15 y15) …);
591 ##[ ##2: #H14; napply (or2_intro2 … (decidable_aluIP2022_aux15 … H14))
592 ##| ##1: #H14; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x16 y16) …);
593 ##[ ##2: #H15; napply (or2_intro2 … (decidable_aluIP2022_aux16 … H15))
594 ##| ##1: #H15; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
595 nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
596 nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
597 nrewrite > H12; nrewrite > H13; nrewrite > H14; nrewrite > H15;
598 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …));