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/memory/memory_struct_base.ma".
25 (* **************** *)
26 (* TIPO ARRAY DA 16 *)
27 (* **************** *)
29 nlemma ar16_destruct_1 :
31 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
32 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
33 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
34 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
36 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
37 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
38 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
39 with [ mk_Array16T a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
45 nlemma ar16_destruct_2 :
47 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
48 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
49 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
50 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
52 #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
55 with [ mk_Array16T _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
61 nlemma ar16_destruct_3 :
63 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
64 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
65 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
66 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
68 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
69 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
70 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
71 with [ mk_Array16T _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
77 nlemma ar16_destruct_4 :
79 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
80 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
81 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
82 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
84 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
85 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
86 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
87 with [ mk_Array16T _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
93 nlemma ar16_destruct_5 :
95 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
96 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
97 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
98 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
100 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
101 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
102 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
103 with [ mk_Array16T _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
109 nlemma ar16_destruct_6 :
111 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
112 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
113 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
114 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
116 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
117 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
118 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
119 with [ mk_Array16T _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
125 nlemma ar16_destruct_7 :
127 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
128 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
129 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
130 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
132 #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
135 with [ mk_Array16T _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
141 nlemma ar16_destruct_8 :
143 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
144 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
145 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
146 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
148 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
149 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
150 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
151 with [ mk_Array16T _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
157 nlemma ar16_destruct_9 :
159 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
160 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
161 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
162 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
164 #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
167 with [ mk_Array16T _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
173 nlemma ar16_destruct_10 :
175 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
176 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
177 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
178 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
180 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
181 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
182 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
183 with [ mk_Array16T _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
189 nlemma ar16_destruct_11 :
191 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
192 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
193 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
194 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
196 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
197 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
198 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
199 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
205 nlemma ar16_destruct_12 :
207 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
208 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
209 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
210 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
212 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
213 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
214 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
215 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
221 nlemma ar16_destruct_13 :
223 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
224 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
225 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
226 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
228 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
229 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
230 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
231 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
237 nlemma ar16_destruct_14 :
239 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
240 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
241 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
242 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
244 #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
247 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
253 nlemma ar16_destruct_15 :
255 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
256 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
257 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
258 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
260 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
261 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
262 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
263 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
269 nlemma ar16_destruct_16 :
271 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
272 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
273 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
274 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
276 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
277 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
278 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
279 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
285 nlemma symmetric_eqar16 :
287 (symmetricT T bool f) →
288 (symmetricT (Array16T T) bool (eq_ar16 T f)).
291 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
293 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
295 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
296 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
297 (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
298 (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) =
299 ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
300 (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8) ⊗
301 (f y9 x9) ⊗ (f y10 x10) ⊗ (f y11 x11) ⊗ (f y12 x12) ⊗
302 (f y13 x13) ⊗ (f y14 x14) ⊗ (f y15 x15) ⊗ (f y16 x16)));
303 nrewrite > (H x1 y1);
304 nrewrite > (H x2 y2);
305 nrewrite > (H x3 y3);
306 nrewrite > (H x4 y4);
307 nrewrite > (H x5 y5);
308 nrewrite > (H x6 y6);
309 nrewrite > (H x7 y7);
310 nrewrite > (H x8 y8);
311 nrewrite > (H x9 y9);
312 nrewrite > (H x10 y10);
313 nrewrite > (H x11 y11);
314 nrewrite > (H x12 y12);
315 nrewrite > (H x13 y13);
316 nrewrite > (H x14 y14);
317 nrewrite > (H x15 y15);
318 nrewrite > (H x16 y16);
322 nlemma eqar16_to_eq :
324 (∀x,y.(f x y = true) → (x = y)) →
325 (∀a1,a2:Array16T T.(eq_ar16 T f a1 a2 = true) → (a1 = a2)).
328 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
330 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
331 nchange in H1:(%) with (
332 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
333 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
334 (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
335 (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) = true);
336 nrewrite > (H … (andb_true_true_r … H1));
337 nletin H2 ≝ (andb_true_true_l … H1);
338 nrewrite > (H … (andb_true_true_r … H2));
339 nletin H3 ≝ (andb_true_true_l … H2);
340 nrewrite > (H … (andb_true_true_r … H3));
341 nletin H4 ≝ (andb_true_true_l … H3);
342 nrewrite > (H … (andb_true_true_r … H4));
343 nletin H5 ≝ (andb_true_true_l … H4);
344 nrewrite > (H … (andb_true_true_r … H5));
345 nletin H6 ≝ (andb_true_true_l … H5);
346 nrewrite > (H … (andb_true_true_r … H6));
347 nletin H7 ≝ (andb_true_true_l … H6);
348 nrewrite > (H … (andb_true_true_r … H7));
349 nletin H8 ≝ (andb_true_true_l … H7);
350 nrewrite > (H … (andb_true_true_r … H8));
351 nletin H9 ≝ (andb_true_true_l … H8);
352 nrewrite > (H … (andb_true_true_r … H9));
353 nletin H10 ≝ (andb_true_true_l … H9);
354 nrewrite > (H … (andb_true_true_r … H10));
355 nletin H11 ≝ (andb_true_true_l … H10);
356 nrewrite > (H … (andb_true_true_r … H11));
357 nletin H12 ≝ (andb_true_true_l … H11);
358 nrewrite > (H … (andb_true_true_r … H12));
359 nletin H13 ≝ (andb_true_true_l … H12);
360 nrewrite > (H … (andb_true_true_r … H13));
361 nletin H14 ≝ (andb_true_true_l … H13);
362 nrewrite > (H … (andb_true_true_r … H14));
363 nletin H15 ≝ (andb_true_true_l … H14);
364 nrewrite > (H … (andb_true_true_r … H15));
365 nrewrite > (H … (andb_true_true_l … H15));
369 nlemma eq_to_eqar16 :
371 (∀x,y.(x = y) → (f x y = true)) →
372 (∀a1,a2:Array16T T.(a1 = a2) → (eq_ar16 T f a1 a2 = true)).
375 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
377 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
378 nrewrite > (ar16_destruct_1 … H1);
379 nrewrite > (ar16_destruct_2 … H1);
380 nrewrite > (ar16_destruct_3 … H1);
381 nrewrite > (ar16_destruct_4 … H1);
382 nrewrite > (ar16_destruct_5 … H1);
383 nrewrite > (ar16_destruct_6 … H1);
384 nrewrite > (ar16_destruct_7 … H1);
385 nrewrite > (ar16_destruct_8 … H1);
386 nrewrite > (ar16_destruct_9 … H1);
387 nrewrite > (ar16_destruct_10 … H1);
388 nrewrite > (ar16_destruct_11 … H1);
389 nrewrite > (ar16_destruct_12 … H1);
390 nrewrite > (ar16_destruct_13 … H1);
391 nrewrite > (ar16_destruct_14 … H1);
392 nrewrite > (ar16_destruct_15 … H1);
393 nrewrite > (ar16_destruct_16 … H1);
395 ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
396 (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8) ⊗
397 (f y9 y9) ⊗ (f y10 y10) ⊗ (f y11 y11) ⊗ (f y12 y12) ⊗
398 (f y13 y13) ⊗ (f y14 y14) ⊗ (f y15 y15) ⊗ (f y16 y16)) = true);
399 nrewrite > (H … (refl_eq …));
400 nrewrite > (H … (refl_eq …));
401 nrewrite > (H … (refl_eq …));
402 nrewrite > (H … (refl_eq …));
403 nrewrite > (H … (refl_eq …));
404 nrewrite > (H … (refl_eq …));
405 nrewrite > (H … (refl_eq …));
406 nrewrite > (H … (refl_eq …));
407 nrewrite > (H … (refl_eq …));
408 nrewrite > (H … (refl_eq …));
409 nrewrite > (H … (refl_eq …));
410 nrewrite > (H … (refl_eq …));
411 nrewrite > (H … (refl_eq …));
412 nrewrite > (H … (refl_eq …));
413 nrewrite > (H … (refl_eq …));
414 nrewrite > (H … (refl_eq …));
418 nlemma decidable_ar16_aux1 :
420 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
421 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
423 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
424 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
425 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
426 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
428 napply (H (ar16_destruct_1 … H1)).
431 nlemma decidable_ar16_aux2 :
433 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
434 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
436 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
437 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
438 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
439 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
441 napply (H (ar16_destruct_2 … H1)).
444 nlemma decidable_ar16_aux3 :
446 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
447 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
449 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
450 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
451 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
452 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
454 napply (H (ar16_destruct_3 … H1)).
457 nlemma decidable_ar16_aux4 :
459 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
460 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
462 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
463 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
464 #T; #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 (ar16_destruct_4 … H1)).
470 nlemma decidable_ar16_aux5 :
472 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
473 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
475 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
476 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
477 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
478 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
480 napply (H (ar16_destruct_5 … H1)).
483 nlemma decidable_ar16_aux6 :
485 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
486 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
488 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
489 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
490 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
491 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
493 napply (H (ar16_destruct_6 … H1)).
496 nlemma decidable_ar16_aux7 :
498 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
499 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
501 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
502 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
503 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
504 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
506 napply (H (ar16_destruct_7 … H1)).
509 nlemma decidable_ar16_aux8 :
511 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
512 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
514 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
515 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
516 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
517 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
519 napply (H (ar16_destruct_8 … H1)).
522 nlemma decidable_ar16_aux9 :
524 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
525 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
527 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
528 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
529 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
530 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
532 napply (H (ar16_destruct_9 … H1)).
535 nlemma decidable_ar16_aux10 :
537 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
538 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
540 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
541 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
542 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
543 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
545 napply (H (ar16_destruct_10 … H1)).
548 nlemma decidable_ar16_aux11 :
550 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
551 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
553 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
554 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
555 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
556 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
558 napply (H (ar16_destruct_11 … H1)).
561 nlemma decidable_ar16_aux12 :
563 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
564 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
566 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
567 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
568 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
569 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
571 napply (H (ar16_destruct_12 … H1)).
574 nlemma decidable_ar16_aux13 :
576 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
577 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
579 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
580 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
581 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
582 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
584 napply (H (ar16_destruct_13 … H1)).
587 nlemma decidable_ar16_aux14 :
589 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
590 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
592 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
593 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
594 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
595 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
597 napply (H (ar16_destruct_14 … H1)).
600 nlemma decidable_ar16_aux15 :
602 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
603 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
605 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
606 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
607 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
608 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
610 napply (H (ar16_destruct_15 … H1)).
613 nlemma decidable_ar16_aux16 :
615 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
616 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
618 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
619 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
620 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
621 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
623 napply (H (ar16_destruct_16 … H1)).
626 nlemma decidable_ar16 :
627 ∀T.(∀x,y:T.decidable (x = y)) →
628 (∀a1,a2:Array16T T.decidable (a1 = a2)).
630 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
631 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
633 napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
634 ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar16_aux1 T … H1))
635 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
636 ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar16_aux2 T … H2))
637 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
638 ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar16_aux3 T … H3))
639 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
640 ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar16_aux4 T … H4))
641 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
642 ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar16_aux5 T … H5))
643 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
644 ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar16_aux6 T … H6))
645 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
646 ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar16_aux7 T … H7))
647 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
648 ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar16_aux8 T … H8))
649 ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (H x9 y9) …);
650 ##[ ##2: #H9; napply (or2_intro2 … (decidable_ar16_aux9 T … H9))
651 ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (H x10 y10) …);
652 ##[ ##2: #H10; napply (or2_intro2 … (decidable_ar16_aux10 T … H10))
653 ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (H x11 y11) …);
654 ##[ ##2: #H11; napply (or2_intro2 … (decidable_ar16_aux11 T … H11))
655 ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (H x12 y12) …);
656 ##[ ##2: #H12; napply (or2_intro2 … (decidable_ar16_aux12 T … H12))
657 ##| ##1: #H12; napply (or2_elim (? = ?) (? ≠ ?) ? (H x13 y13) …);
658 ##[ ##2: #H13; napply (or2_intro2 … (decidable_ar16_aux13 T … H13))
659 ##| ##1: #H13; napply (or2_elim (? = ?) (? ≠ ?) ? (H x14 y14) …);
660 ##[ ##2: #H14; napply (or2_intro2 … (decidable_ar16_aux14 T … H14))
661 ##| ##1: #H14; napply (or2_elim (? = ?) (? ≠ ?) ? (H x15 y15) …);
662 ##[ ##2: #H15; napply (or2_intro2 … (decidable_ar16_aux15 T … H15))
663 ##| ##1: #H15; napply (or2_elim (? = ?) (? ≠ ?) ? (H x16 y16) …);
664 ##[ ##2: #H16; napply (or2_intro2 … (decidable_ar16_aux16 T … H16))
665 ##| ##1: #H16; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
666 nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
667 nrewrite > H9; nrewrite > H10; nrewrite > H11; nrewrite > H12;
668 nrewrite > H13; nrewrite > H14; nrewrite > H15; nrewrite > H16;
669 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
688 (* !!! per brevita *)
689 naxiom neqar16_to_neq :
691 (∀x,y:T.f x y = false → x ≠ y) →
692 (∀p1,p2:Array16T T.(eq_ar16 T f p1 p2 = false → p1 ≠ p2)).
694 (* !!! per brevita *)
695 naxiom neq_to_neqar16 :
697 (∀x,y:T.decidable (x = y)) →
698 (∀x,y:T.x ≠ y → f x y = false) →
699 (∀p1,p2:Array16T T.(p1 ≠ p2 → eq_ar16 T f p1 p2 = false)).
701 nlemma ar16_is_comparable : comparable → comparable.
703 ##[ napply (mk_Array16T ? (zeroc T) (zeroc T) (zeroc T) (zeroc T)
704 (zeroc T) (zeroc T) (zeroc T) (zeroc T)
705 (zeroc T) (zeroc T) (zeroc T) (zeroc T)
706 (zeroc T) (zeroc T) (zeroc T) (zeroc T))
707 ##| napply (λP.(forallc T)
723 (λe16.P (mk_Array16T T e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 e11 e12 e13 e14 e15 e16))))))))))))))))))
724 ##| napply (eq_ar16 … (eqc T))
725 ##| napply eqar16_to_eq;
727 ##| napply eq_to_eqar16;
729 ##| napply neqar16_to_neq;
730 napply (neqc_to_neq T)
731 ##| napply neq_to_neqar16;
732 ##[ napply (decidable_c T)
733 ##| napply (neq_to_neqc T) ##]
734 ##| napply decidable_ar16;
735 napply (decidable_c T)
736 ##| napply symmetric_eqar16;
737 napply (symmetric_eqc T)
741 unification hint 0 ≔ S: comparable ;
743 X ≟ (ar16_is_comparable S)
744 (*********************************************) ⊢
747 (* *************** *)
748 (* TIPO ARRAY DA 8 *)
749 (* *************** *)
751 nlemma ar8_destruct_1 :
752 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
753 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
755 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
756 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
757 with [ mk_Array8T a _ _ _ _ _ _ _ ⇒ x1 = a ]);
763 nlemma ar8_destruct_2 :
764 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
765 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
767 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
768 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
769 with [ mk_Array8T _ a _ _ _ _ _ _ ⇒ x2 = a ]);
775 nlemma ar8_destruct_3 :
776 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
777 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
779 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
780 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
781 with [ mk_Array8T _ _ a _ _ _ _ _ ⇒ x3 = a ]);
787 nlemma ar8_destruct_4 :
788 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
789 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
791 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
792 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
793 with [ mk_Array8T _ _ _ a _ _ _ _ ⇒ x4 = a ]);
799 nlemma ar8_destruct_5 :
800 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
801 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
803 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
804 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
805 with [ mk_Array8T _ _ _ _ a _ _ _ ⇒ x5 = a ]);
811 nlemma ar8_destruct_6 :
812 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
813 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
815 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
816 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
817 with [ mk_Array8T _ _ _ _ _ a _ _ ⇒ x6 = a ]);
823 nlemma ar8_destruct_7 :
824 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
825 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
827 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
828 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
829 with [ mk_Array8T _ _ _ _ _ _ a _ ⇒ x7 = a ]);
835 nlemma ar8_destruct_8 :
836 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
837 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
839 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
840 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
841 with [ mk_Array8T _ _ _ _ _ _ _ a ⇒ x8 = a ]);
847 nlemma symmetric_eqar8 :
849 (symmetricT T bool f) →
850 (symmetricT (Array8T T) bool (eq_ar8 T f)).
853 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
855 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
857 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
858 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) =
859 ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
860 (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8)));
861 nrewrite > (H x1 y1);
862 nrewrite > (H x2 y2);
863 nrewrite > (H x3 y3);
864 nrewrite > (H x4 y4);
865 nrewrite > (H x5 y5);
866 nrewrite > (H x6 y6);
867 nrewrite > (H x7 y7);
868 nrewrite > (H x8 y8);
874 (∀x,y.(f x y = true) → (x = y)) →
875 (∀a1,a2:Array8T T.(eq_ar8 T f a1 a2 = true) → (a1 = a2)).
878 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
880 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
881 nchange in H1:(%) with (
882 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
883 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) = true);
884 nrewrite > (H … (andb_true_true_r … H1));
885 nletin H2 ≝ (andb_true_true_l … H1);
886 nrewrite > (H … (andb_true_true_r … H2));
887 nletin H3 ≝ (andb_true_true_l … H2);
888 nrewrite > (H … (andb_true_true_r … H3));
889 nletin H4 ≝ (andb_true_true_l … H3);
890 nrewrite > (H … (andb_true_true_r … H4));
891 nletin H5 ≝ (andb_true_true_l … H4);
892 nrewrite > (H … (andb_true_true_r … H5));
893 nletin H6 ≝ (andb_true_true_l … H5);
894 nrewrite > (H … (andb_true_true_r … H6));
895 nletin H7 ≝ (andb_true_true_l … H6);
896 nrewrite > (H … (andb_true_true_r … H7));
897 nrewrite > (H … (andb_true_true_l … H7));
903 (∀x,y.(x = y) → (f x y = true)) →
904 (∀a1,a2:Array8T T.(a1 = a2) → (eq_ar8 T f a1 a2 = true)).
907 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
909 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
910 nrewrite > (ar8_destruct_1 … H1);
911 nrewrite > (ar8_destruct_2 … H1);
912 nrewrite > (ar8_destruct_3 … H1);
913 nrewrite > (ar8_destruct_4 … H1);
914 nrewrite > (ar8_destruct_5 … H1);
915 nrewrite > (ar8_destruct_6 … H1);
916 nrewrite > (ar8_destruct_7 … H1);
917 nrewrite > (ar8_destruct_8 … H1);
919 ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
920 (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8)) = true);
921 nrewrite > (H … (refl_eq …));
922 nrewrite > (H … (refl_eq …));
923 nrewrite > (H … (refl_eq …));
924 nrewrite > (H … (refl_eq …));
925 nrewrite > (H … (refl_eq …));
926 nrewrite > (H … (refl_eq …));
927 nrewrite > (H … (refl_eq …));
928 nrewrite > (H … (refl_eq …));
932 nlemma decidable_ar8_aux1 :
933 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
935 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
936 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
938 napply (H (ar8_destruct_1 … H1)).
941 nlemma decidable_ar8_aux2 :
942 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
944 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
945 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
947 napply (H (ar8_destruct_2 … H1)).
950 nlemma decidable_ar8_aux3 :
951 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
953 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
954 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
956 napply (H (ar8_destruct_3 … H1)).
959 nlemma decidable_ar8_aux4 :
960 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
962 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
963 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
965 napply (H (ar8_destruct_4 … H1)).
968 nlemma decidable_ar8_aux5 :
969 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
971 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
972 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
974 napply (H (ar8_destruct_5 … H1)).
977 nlemma decidable_ar8_aux6 :
978 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
980 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
981 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
983 napply (H (ar8_destruct_6 … H1)).
986 nlemma decidable_ar8_aux7 :
987 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
989 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
990 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
992 napply (H (ar8_destruct_7 … H1)).
995 nlemma decidable_ar8_aux8 :
996 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
998 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
999 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1000 nnormalize; #H; #H1;
1001 napply (H (ar8_destruct_8 … H1)).
1004 nlemma decidable_ar8 :
1005 ∀T.(∀x,y:T.decidable (x = y)) →
1006 (∀a1,a2:Array8T T.decidable (a1 = a2)).
1008 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1009 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1011 napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
1012 ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar8_aux1 T … H1))
1013 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
1014 ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar8_aux2 T … H2))
1015 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
1016 ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar8_aux3 T … H3))
1017 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
1018 ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar8_aux4 T … H4))
1019 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
1020 ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar8_aux5 T … H5))
1021 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
1022 ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar8_aux6 T … H6))
1023 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
1024 ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar8_aux7 T … H7))
1025 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
1026 ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar8_aux8 T … H8))
1027 ##| ##1: #H8; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
1028 nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
1029 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
1040 (* !!! per brevita *)
1041 naxiom neqar8_to_neq :
1043 (∀x,y:T.f x y = false → x ≠ y) →
1044 (∀p1,p2:Array8T T.(eq_ar8 T f p1 p2 = false → p1 ≠ p2)).
1046 (* !!! per brevita *)
1047 naxiom neq_to_neqar8 :
1049 (∀x,y:T.decidable (x = y)) →
1050 (∀x,y:T.x ≠ y → f x y = false) →
1051 (∀p1,p2:Array8T T.(p1 ≠ p2 → eq_ar8 T f p1 p2 = false)).
1053 nlemma ar8_is_comparable : comparable → comparable.
1055 ##[ napply (mk_Array8T ? (zeroc T) (zeroc T) (zeroc T) (zeroc T)
1056 (zeroc T) (zeroc T) (zeroc T) (zeroc T))
1057 ##| napply (λP.(forallc T)
1065 (λe8.P (mk_Array8T T e1 e2 e3 e4 e5 e6 e7 e8))))))))))
1066 ##| napply (eq_ar8 … (eqc T))
1067 ##| napply eqar8_to_eq;
1068 napply (eqc_to_eq T)
1069 ##| napply eq_to_eqar8;
1070 napply (eq_to_eqc T)
1071 ##| napply neqar8_to_neq;
1072 napply (neqc_to_neq T)
1073 ##| napply neq_to_neqar8;
1074 ##[ napply (decidable_c T)
1075 ##| napply (neq_to_neqc T) ##]
1076 ##| napply decidable_ar8;
1077 napply (decidable_c T)
1078 ##| napply symmetric_eqar8;
1079 napply (symmetric_eqc T)
1083 unification hint 0 ≔ S: comparable ;
1085 X ≟ (ar8_is_comparable S)
1086 (*********************************************) ⊢