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 "emulator/status/IP2022_status_base.ma".
25 (* *********************************** *)
26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
27 (* *********************************** *)
29 nlemma aluIP2022_destruct_1 :
30 ∀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.
31 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
32 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
34 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
35 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
36 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
37 with [ mk_alu_IP2022 a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
43 nlemma aluIP2022_destruct_2 :
44 ∀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.
45 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
46 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
48 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
49 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
50 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
51 with [ mk_alu_IP2022 _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
57 nlemma aluIP2022_destruct_3 :
58 ∀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.
59 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
60 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
62 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
63 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
64 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
65 with [ mk_alu_IP2022 _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
71 nlemma aluIP2022_destruct_4 :
72 ∀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.
73 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
74 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
76 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
77 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
78 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
79 with [ mk_alu_IP2022 _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
85 nlemma aluIP2022_destruct_5 :
86 ∀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.
87 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
88 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
90 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
91 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
92 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
93 with [ mk_alu_IP2022 _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
99 nlemma aluIP2022_destruct_6 :
100 ∀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.
101 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
102 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
104 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
105 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
106 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
107 with [ mk_alu_IP2022 _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
113 nlemma aluIP2022_destruct_7 :
114 ∀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.
115 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
116 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
118 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
119 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
120 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
121 with [ mk_alu_IP2022 _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
127 nlemma aluIP2022_destruct_8 :
128 ∀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.
129 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
130 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
132 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
133 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
134 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
135 with [ mk_alu_IP2022 _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
141 nlemma aluIP2022_destruct_9 :
142 ∀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.
143 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
144 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
146 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
147 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
148 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
149 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
155 nlemma aluIP2022_destruct_10 :
156 ∀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.
157 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
158 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
160 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
161 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
162 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
163 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
169 nlemma aluIP2022_destruct_11 :
170 ∀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.
171 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
172 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
174 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
175 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
176 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
177 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
183 nlemma aluIP2022_destruct_12 :
184 ∀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.
185 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
186 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
188 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
189 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
190 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
191 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
197 nlemma aluIP2022_destruct_13 :
198 ∀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.
199 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
200 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
202 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
203 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
204 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
205 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
211 nlemma aluIP2022_destruct_14 :
212 ∀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.
213 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
214 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
216 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
217 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
218 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
219 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
225 nlemma aluIP2022_destruct_15 :
226 ∀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.
227 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
228 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
230 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
231 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
232 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
233 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
239 nlemma aluIP2022_destruct_16 :
240 ∀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.
241 mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
242 mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
244 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
245 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
246 nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
247 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
253 (* !!! ci mette troppo tempo a compilare *)
254 naxiom eq_to_eqaluIP2022 : ∀alu1,alu2.alu1 = alu2 → eq_IP2022_alu alu1 alu2 = true.
255 (* #alu1; ncases alu1;
256 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
258 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
259 nrewrite > (aluIP2022_destruct_1 … H);
260 nrewrite > (aluIP2022_destruct_2 … H);
261 nrewrite > (aluIP2022_destruct_3 … H);
262 nrewrite > (aluIP2022_destruct_4 … H);
263 nrewrite > (aluIP2022_destruct_5 … H);
264 nrewrite > (aluIP2022_destruct_6 … H);
265 nrewrite > (aluIP2022_destruct_7 … H);
266 nrewrite > (aluIP2022_destruct_8 … H);
267 nrewrite > (aluIP2022_destruct_9 … H);
268 nrewrite > (aluIP2022_destruct_10 … H);
269 nrewrite > (aluIP2022_destruct_11 … H);
270 nrewrite > (aluIP2022_destruct_12 … H);
271 nrewrite > (aluIP2022_destruct_13 … H);
272 nrewrite > (aluIP2022_destruct_14 … H);
273 nrewrite > (aluIP2022_destruct_15 … H);
274 nrewrite > (aluIP2022_destruct_16 … H);
276 ((eqc ? y1 y1) ⊗ (eqc ? y2 y2) ⊗ (eqc ? y3 y3) ⊗ (eqc ? y4 y4) ⊗
277 (eqc ? y5 y5) ⊗ (eqc ? y6 y6) ⊗ (eqc ? y7 y7) ⊗ (eqc ? y8 y8) ⊗
278 (eqc ? y9 y9) ⊗ (eqc ? y10 y10) ⊗ (eqc ? y11 y11) ⊗ (eqc ? y12 y12) ⊗
279 (eqc ? y13 y13) ⊗ (eqc ? y14 y14) ⊗ (eqc ? y15 y15) ⊗ (eqc ? y16 y16)) = true);
280 nrewrite > (eq_to_eqc ? y1 y1 (refl_eq …));
281 nrewrite > (eq_to_eqc ? y2 y2 (refl_eq …));
282 nrewrite > (eq_to_eqc ? y3 y3 (refl_eq …));
283 nrewrite > (eq_to_eqc ? y4 y4 (refl_eq …));
284 nrewrite > (eq_to_eqc ? y5 y5 (refl_eq …));
285 nrewrite > (eq_to_eqc ? y6 y6 (refl_eq …));
286 nrewrite > (eq_to_eqc ? y7 y7 (refl_eq …));
287 nrewrite > (eq_to_eqc ? y8 y8 (refl_eq …));
288 nrewrite > (eq_to_eqc ? y9 y9 (refl_eq …));
289 nrewrite > (eq_to_eqc ? y10 y10 (refl_eq …));
290 nrewrite > (eq_to_eqc ? y11 y11 (refl_eq …));
291 nrewrite > (eq_to_eqc ? y12 y12 (refl_eq …));
292 nrewrite > (eq_to_eqc ? y13 y13 (refl_eq …));
293 nrewrite > (eq_to_eqc ? y14 y14 (refl_eq …));
294 nrewrite > (eq_to_eqc ? y15 y15 (refl_eq …));
295 nrewrite > (eq_to_eqc ? y16 y16 (refl_eq …));
299 nlemma neqaluIP2022_to_neq : ∀alu1,alu2.eq_IP2022_alu alu1 alu2 = false → alu1 ≠ alu2.
301 napply (not_to_not (s1 = s2) (eq_IP2022_alu s1 s2 = true) …);
302 ##[ ##1: napply (eq_to_eqaluIP2022 s1 s2)
303 ##| ##2: napply (eqfalse_to_neqtrue … H)
307 nlemma eqaluIP2022_to_eq : ∀alu1,alu2.eq_IP2022_alu alu1 alu2 = true → alu1 = alu2.
309 #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
311 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
312 nchange in H:(%) with (
313 ((eqc ? z1 y1) ⊗ (eqc ? z2 y2) ⊗ (eqc ? z3 y3) ⊗ (eqc ? z4 y4) ⊗
314 (eqc ? z5 y5) ⊗ (eqc ? z6 y6) ⊗ (eqc ? z7 y7) ⊗ (eqc ? z8 y8) ⊗
315 (eqc ? z9 y9) ⊗ (eqc ? z10 y10) ⊗ (eqc ? z11 y11) ⊗ (eqc ? z12 y12) ⊗
316 (eqc ? z13 y13) ⊗ (eqc ? z14 y14) ⊗ (eqc ? z15 y15) ⊗ (eqc ? z16 y16)) = true);
317 nrewrite > (eqc_to_eq … (andb_true_true_r … H));
318 nletin H1 ≝ (andb_true_true_l … H);
319 nrewrite > (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
320 nletin H2 ≝ (andb_true_true_l … H1);
321 nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
322 nletin H3 ≝ (andb_true_true_l … H2);
323 nrewrite > (eqc_to_eq … (andb_true_true_r … H3));
324 nletin H4 ≝ (andb_true_true_l … H3);
325 nrewrite > (eqc_to_eq … (andb_true_true_r … H4));
326 nletin H5 ≝ (andb_true_true_l … H4);
327 nrewrite > (eqc_to_eq … (andb_true_true_r … H5));
328 nletin H6 ≝ (andb_true_true_l … H5);
329 nrewrite > (eqc_to_eq … (andb_true_true_r … H6));
330 nletin H7 ≝ (andb_true_true_l … H6);
331 nrewrite > (eqc_to_eq … (andb_true_true_r … H7));
332 nletin H8 ≝ (andb_true_true_l … H7);
333 nrewrite > (eqc_to_eq … (andb_true_true_r … H8));
334 nletin H9 ≝ (andb_true_true_l … H8);
335 nrewrite > (eqc_to_eq … (andb_true_true_r … H9));
336 nletin H10 ≝ (andb_true_true_l … H9);
337 nrewrite > (eqc_to_eq … (andb_true_true_r … H10));
338 nletin H11 ≝ (andb_true_true_l … H10);
339 nrewrite > (eqc_to_eq … (andb_true_true_r … H11));
340 nletin H12 ≝ (andb_true_true_l … H11);
341 nrewrite > (eqc_to_eq … (andb_true_true_r … H12));
342 nletin H13 ≝ (andb_true_true_l … H12);
343 nrewrite > (eqc_to_eq … (andb_true_true_r … H13));
344 nletin H14 ≝ (andb_true_true_l … H13);
345 nrewrite > (eqc_to_eq … (andb_true_true_r … H14));
346 nrewrite > (eqc_to_eq … (andb_true_true_l … H14));
350 nlemma neq_to_neqaluIP2022 : ∀alu1,alu2.alu1 ≠ alu2 → eq_IP2022_alu alu1 alu2 = false.
352 napply (neqtrue_to_eqfalse (eq_IP2022_alu s1 s2));
353 napply (not_to_not (eq_IP2022_alu s1 s2 = true) (s1 = s2) ? H);
354 napply (eqaluIP2022_to_eq s1 s2).
357 nlemma decidable_aluIP2022 : ∀x,y:alu_IP2022.decidable (x = y).
359 napply (or2_elim (eq_IP2022_alu x y = true) (eq_IP2022_alu x y = false) ? (decidable_bexpr ?));
360 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqaluIP2022_to_eq … H))
361 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqaluIP2022_to_neq … H))
365 (* !!! ci mette troppo tempo a compilare *)
366 naxiom symmetric_eqaluIP2022 : symmetricT alu_IP2022 bool eq_IP2022_alu.
367 (* #alu1; ncases alu1;
368 #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
370 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
372 ((eqc ? z1 y1) ⊗ (eqc ? z2 y2) ⊗ (eqc ? z3 y3) ⊗ (eqc ? z4 y4) ⊗
373 (eqc ? z5 y5) ⊗ (eqc ? z6 y6) ⊗ (eqc ? z7 y7) ⊗ (eqc ? z8 y8) ⊗
374 (eqc ? z9 y9) ⊗ (eqc ? z10 y10) ⊗ (eqc ? z11 y11) ⊗ (eqc ? z12 y12) ⊗
375 (eqc ? z13 y13) ⊗ (eqc ? z14 y14) ⊗ (eqc ? z15 y15) ⊗ (eqc ? z16 y16)) =
376 ((eqc ? y1 z1) ⊗ (eqc ? y2 z2) ⊗ (eqc ? y3 z3) ⊗ (eqc ? y4 z4) ⊗
377 (eqc ? y5 z5) ⊗ (eqc ? y6 z6) ⊗ (eqc ? y7 z7) ⊗ (eqc ? y8 z8) ⊗
378 (eqc ? y9 z9) ⊗ (eqc ? y10 z10) ⊗ (eqc ? y11 z11) ⊗ (eqc ? y12 z12) ⊗
379 (eqc ? y13 z13) ⊗ (eqc ? y14 z14) ⊗ (eqc ? y15 z15) ⊗ (eqc ? y16 z16)));
380 nrewrite > (symmetric_eqc ? z1 y1);
381 nrewrite > (symmetric_eqc ? z2 y2);
382 nrewrite > (symmetric_eqc ? z3 y3);
383 nrewrite > (symmetric_eqc ? z4 y4);
384 nrewrite > (symmetric_eqc ? z5 y5);
385 nrewrite > (symmetric_eqc ? z6 y6);
386 nrewrite > (symmetric_eqc ? z7 y7);
387 nrewrite > (symmetric_eqc ? z8 y8);
388 nrewrite > (symmetric_eqc ? z9 y9);
389 nrewrite > (symmetric_eqc ? z10 y10);
390 nrewrite > (symmetric_eqc ? z11 y11);
391 nrewrite > (symmetric_eqc ? z12 y12);
392 nrewrite > (symmetric_eqc ? z13 y13);
393 nrewrite > (symmetric_eqc ? z14 y14);
394 nrewrite > (symmetric_eqc ? z15 y15);
395 nrewrite > (symmetric_eqc ? z16 y16);
399 nlemma aluIP2022_is_comparable : comparable.
401 ##[ napply (mk_alu_IP2022 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
402 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
403 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
404 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
405 ##| napply forall_IP2022_alu
406 ##| napply eq_IP2022_alu
407 ##| napply eqaluIP2022_to_eq
408 ##| napply eq_to_eqaluIP2022
409 ##| napply neqaluIP2022_to_neq
410 ##| napply neq_to_neqaluIP2022
411 ##| napply decidable_aluIP2022
412 ##| napply symmetric_eqaluIP2022
416 unification hint 0 ≔ ⊢ carr aluIP2022_is_comparable ≡ alu_IP2022.