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.ma".
24 include "num/bool_lemmas.ma".
26 (* **************** *)
27 (* TIPO ARRAY DA 16 *)
28 (* **************** *)
30 nlemma ar16_destruct_1 :
32 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
33 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
34 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
35 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
37 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
38 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
39 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
40 with [ mk_Array16T a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
46 nlemma ar16_destruct_2 :
48 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
49 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
50 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
51 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
53 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
54 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
55 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
56 with [ mk_Array16T _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
62 nlemma ar16_destruct_3 :
64 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
65 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
66 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
67 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
69 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
70 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
71 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
72 with [ mk_Array16T _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
78 nlemma ar16_destruct_4 :
80 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
81 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
82 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
83 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
85 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
86 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
87 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
88 with [ mk_Array16T _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
94 nlemma ar16_destruct_5 :
96 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
97 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
98 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
99 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
101 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
102 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
103 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
104 with [ mk_Array16T _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
110 nlemma ar16_destruct_6 :
112 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
113 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
114 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
115 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
117 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
118 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
119 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
120 with [ mk_Array16T _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
126 nlemma ar16_destruct_7 :
128 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
129 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
130 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
131 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
133 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
134 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
135 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
136 with [ mk_Array16T _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
142 nlemma ar16_destruct_8 :
144 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
145 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
146 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
147 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
149 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
150 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
151 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
152 with [ mk_Array16T _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
158 nlemma ar16_destruct_9 :
160 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
161 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
162 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
163 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
165 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
166 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
167 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
168 with [ mk_Array16T _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
174 nlemma ar16_destruct_10 :
176 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
177 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
178 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
179 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
181 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
182 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
183 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
184 with [ mk_Array16T _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
190 nlemma ar16_destruct_11 :
192 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
193 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
194 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
195 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
197 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
198 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
199 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
200 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
206 nlemma ar16_destruct_12 :
208 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
209 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
210 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
211 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
213 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
214 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
215 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
216 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
222 nlemma ar16_destruct_13 :
224 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
225 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
226 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
227 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
229 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
230 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
231 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
232 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
238 nlemma ar16_destruct_14 :
240 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
241 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
242 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
243 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
245 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
246 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
247 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
248 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
254 nlemma ar16_destruct_15 :
256 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
257 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
258 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
259 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
261 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
262 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
263 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
264 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
270 nlemma ar16_destruct_16 :
272 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
273 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
274 mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
275 mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
277 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
278 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
279 nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
280 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
286 nlemma symmetric_eqar16 :
288 (symmetricT T bool f) →
289 (symmetricT (Array16T T) bool (eq_ar16 T f)).
292 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
294 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
296 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
297 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
298 (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
299 (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) =
300 ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
301 (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8) ⊗
302 (f y9 x9) ⊗ (f y10 x10) ⊗ (f y11 x11) ⊗ (f y12 x12) ⊗
303 (f y13 x13) ⊗ (f y14 x14) ⊗ (f y15 x15) ⊗ (f y16 x16)));
304 nrewrite > (H x1 y1);
305 nrewrite > (H x2 y2);
306 nrewrite > (H x3 y3);
307 nrewrite > (H x4 y4);
308 nrewrite > (H x5 y5);
309 nrewrite > (H x6 y6);
310 nrewrite > (H x7 y7);
311 nrewrite > (H x8 y8);
312 nrewrite > (H x9 y9);
313 nrewrite > (H x10 y10);
314 nrewrite > (H x11 y11);
315 nrewrite > (H x12 y12);
316 nrewrite > (H x13 y13);
317 nrewrite > (H x14 y14);
318 nrewrite > (H x15 y15);
319 nrewrite > (H x16 y16);
323 nlemma eqar16_to_eq :
325 (∀x,y.(f x y = true) → (x = y)) →
326 (∀a1,a2:Array16T T.(eq_ar16 T f a1 a2 = true) → (a1 = a2)).
329 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
331 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
332 nchange in H1:(%) with (
333 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
334 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
335 (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
336 (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) = true);
337 nrewrite > (H … (andb_true_true_r … H1));
338 nletin H2 ≝ (andb_true_true_l … H1);
339 nrewrite > (H … (andb_true_true_r … H2));
340 nletin H3 ≝ (andb_true_true_l … H2);
341 nrewrite > (H … (andb_true_true_r … H3));
342 nletin H4 ≝ (andb_true_true_l … H3);
343 nrewrite > (H … (andb_true_true_r … H4));
344 nletin H5 ≝ (andb_true_true_l … H4);
345 nrewrite > (H … (andb_true_true_r … H5));
346 nletin H6 ≝ (andb_true_true_l … H5);
347 nrewrite > (H … (andb_true_true_r … H6));
348 nletin H7 ≝ (andb_true_true_l … H6);
349 nrewrite > (H … (andb_true_true_r … H7));
350 nletin H8 ≝ (andb_true_true_l … H7);
351 nrewrite > (H … (andb_true_true_r … H8));
352 nletin H9 ≝ (andb_true_true_l … H8);
353 nrewrite > (H … (andb_true_true_r … H9));
354 nletin H10 ≝ (andb_true_true_l … H9);
355 nrewrite > (H … (andb_true_true_r … H10));
356 nletin H11 ≝ (andb_true_true_l … H10);
357 nrewrite > (H … (andb_true_true_r … H11));
358 nletin H12 ≝ (andb_true_true_l … H11);
359 nrewrite > (H … (andb_true_true_r … H12));
360 nletin H13 ≝ (andb_true_true_l … H12);
361 nrewrite > (H … (andb_true_true_r … H13));
362 nletin H14 ≝ (andb_true_true_l … H13);
363 nrewrite > (H … (andb_true_true_r … H14));
364 nletin H15 ≝ (andb_true_true_l … H14);
365 nrewrite > (H … (andb_true_true_r … H15));
366 nrewrite > (H … (andb_true_true_l … H15));
370 nlemma eq_to_eqar16 :
372 (∀x,y.(x = y) → (f x y = true)) →
373 (∀a1,a2:Array16T T.(a1 = a2) → (eq_ar16 T f a1 a2 = true)).
376 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
378 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
379 nrewrite > (ar16_destruct_1 … H1);
380 nrewrite > (ar16_destruct_2 … H1);
381 nrewrite > (ar16_destruct_3 … H1);
382 nrewrite > (ar16_destruct_4 … H1);
383 nrewrite > (ar16_destruct_5 … H1);
384 nrewrite > (ar16_destruct_6 … H1);
385 nrewrite > (ar16_destruct_7 … H1);
386 nrewrite > (ar16_destruct_8 … H1);
387 nrewrite > (ar16_destruct_9 … H1);
388 nrewrite > (ar16_destruct_10 … H1);
389 nrewrite > (ar16_destruct_11 … H1);
390 nrewrite > (ar16_destruct_12 … H1);
391 nrewrite > (ar16_destruct_13 … H1);
392 nrewrite > (ar16_destruct_14 … H1);
393 nrewrite > (ar16_destruct_15 … H1);
394 nrewrite > (ar16_destruct_16 … H1);
396 ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
397 (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8) ⊗
398 (f y9 y9) ⊗ (f y10 y10) ⊗ (f y11 y11) ⊗ (f y12 y12) ⊗
399 (f y13 y13) ⊗ (f y14 y14) ⊗ (f y15 y15) ⊗ (f y16 y16)) = true);
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 …));
415 nrewrite > (H … (refl_eq …));
419 nlemma decidable_ar16_aux1 :
421 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
422 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
424 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
425 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
426 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
427 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
429 napply (H (ar16_destruct_1 … H1)).
432 nlemma decidable_ar16_aux2 :
434 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
435 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
437 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
438 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
439 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
440 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
442 napply (H (ar16_destruct_2 … H1)).
445 nlemma decidable_ar16_aux3 :
447 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
448 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
450 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
451 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
452 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
453 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
455 napply (H (ar16_destruct_3 … H1)).
458 nlemma decidable_ar16_aux4 :
460 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
461 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
463 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
464 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
465 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
466 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
468 napply (H (ar16_destruct_4 … H1)).
471 nlemma decidable_ar16_aux5 :
473 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
474 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
476 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
477 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
478 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
479 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
481 napply (H (ar16_destruct_5 … H1)).
484 nlemma decidable_ar16_aux6 :
486 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
487 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
489 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
490 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
491 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
492 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
494 napply (H (ar16_destruct_6 … H1)).
497 nlemma decidable_ar16_aux7 :
499 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
500 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
502 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
503 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
504 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
505 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
507 napply (H (ar16_destruct_7 … H1)).
510 nlemma decidable_ar16_aux8 :
512 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
513 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
515 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
516 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
517 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
518 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
520 napply (H (ar16_destruct_8 … H1)).
523 nlemma decidable_ar16_aux9 :
525 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
526 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
528 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
529 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
530 #T; #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 (ar16_destruct_9 … H1)).
536 nlemma decidable_ar16_aux10 :
538 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
539 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
541 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
542 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
543 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
544 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
546 napply (H (ar16_destruct_10 … H1)).
549 nlemma decidable_ar16_aux11 :
551 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
552 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
554 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
555 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
556 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
557 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
559 napply (H (ar16_destruct_11 … H1)).
562 nlemma decidable_ar16_aux12 :
564 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
565 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
567 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
568 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
569 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
570 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
572 napply (H (ar16_destruct_12 … H1)).
575 nlemma decidable_ar16_aux13 :
577 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
578 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
580 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
581 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
582 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
583 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
585 napply (H (ar16_destruct_13 … H1)).
588 nlemma decidable_ar16_aux14 :
590 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
591 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
593 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
594 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
595 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
596 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
598 napply (H (ar16_destruct_14 … H1)).
601 nlemma decidable_ar16_aux15 :
603 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
604 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
606 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
607 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
608 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
609 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
611 napply (H (ar16_destruct_15 … H1)).
614 nlemma decidable_ar16_aux16 :
616 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
617 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
619 (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
620 (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
621 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
622 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
624 napply (H (ar16_destruct_16 … H1)).
627 nlemma decidable_ar16 :
628 ∀T.(∀x,y:T.decidable (x = y)) →
629 (∀a1,a2:Array16T T.decidable (a1 = a2)).
631 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
632 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
634 napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
635 ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar16_aux1 T … H1))
636 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
637 ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar16_aux2 T … H2))
638 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
639 ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar16_aux3 T … H3))
640 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
641 ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar16_aux4 T … H4))
642 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
643 ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar16_aux5 T … H5))
644 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
645 ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar16_aux6 T … H6))
646 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
647 ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar16_aux7 T … H7))
648 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
649 ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar16_aux8 T … H8))
650 ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (H x9 y9) …);
651 ##[ ##2: #H9; napply (or2_intro2 … (decidable_ar16_aux9 T … H9))
652 ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (H x10 y10) …);
653 ##[ ##2: #H10; napply (or2_intro2 … (decidable_ar16_aux10 T … H10))
654 ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (H x11 y11) …);
655 ##[ ##2: #H11; napply (or2_intro2 … (decidable_ar16_aux11 T … H11))
656 ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (H x12 y12) …);
657 ##[ ##2: #H12; napply (or2_intro2 … (decidable_ar16_aux12 T … H12))
658 ##| ##1: #H12; napply (or2_elim (? = ?) (? ≠ ?) ? (H x13 y13) …);
659 ##[ ##2: #H13; napply (or2_intro2 … (decidable_ar16_aux13 T … H13))
660 ##| ##1: #H13; napply (or2_elim (? = ?) (? ≠ ?) ? (H x14 y14) …);
661 ##[ ##2: #H14; napply (or2_intro2 … (decidable_ar16_aux14 T … H14))
662 ##| ##1: #H14; napply (or2_elim (? = ?) (? ≠ ?) ? (H x15 y15) …);
663 ##[ ##2: #H15; napply (or2_intro2 … (decidable_ar16_aux15 T … H15))
664 ##| ##1: #H15; napply (or2_elim (? = ?) (? ≠ ?) ? (H x16 y16) …);
665 ##[ ##2: #H16; napply (or2_intro2 … (decidable_ar16_aux16 T … H16))
666 ##| ##1: #H16; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
667 nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
668 nrewrite > H9; nrewrite > H10; nrewrite > H11; nrewrite > H12;
669 nrewrite > H13; nrewrite > H14; nrewrite > H15; nrewrite > H16;
670 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
689 (* *************** *)
690 (* TIPO ARRAY DA 8 *)
691 (* *************** *)
693 nlemma ar8_destruct_1 :
694 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
695 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
697 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
698 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
699 with [ mk_Array8T a _ _ _ _ _ _ _ ⇒ x1 = a ]);
705 nlemma ar8_destruct_2 :
706 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
707 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
709 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
710 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
711 with [ mk_Array8T _ a _ _ _ _ _ _ ⇒ x2 = a ]);
717 nlemma ar8_destruct_3 :
718 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
719 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
721 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
722 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
723 with [ mk_Array8T _ _ a _ _ _ _ _ ⇒ x3 = a ]);
729 nlemma ar8_destruct_4 :
730 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
731 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
733 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
734 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
735 with [ mk_Array8T _ _ _ a _ _ _ _ ⇒ x4 = a ]);
741 nlemma ar8_destruct_5 :
742 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
743 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
745 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
746 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
747 with [ mk_Array8T _ _ _ _ a _ _ _ ⇒ x5 = a ]);
753 nlemma ar8_destruct_6 :
754 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
755 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
757 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
758 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
759 with [ mk_Array8T _ _ _ _ _ a _ _ ⇒ x6 = a ]);
765 nlemma ar8_destruct_7 :
766 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
767 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
769 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
770 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
771 with [ mk_Array8T _ _ _ _ _ _ a _ ⇒ x7 = a ]);
777 nlemma ar8_destruct_8 :
778 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
779 mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8 →
781 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
782 nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
783 with [ mk_Array8T _ _ _ _ _ _ _ a ⇒ x8 = a ]);
789 nlemma symmetric_eqar8 :
791 (symmetricT T bool f) →
792 (symmetricT (Array8T T) bool (eq_ar8 T f)).
795 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
797 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
799 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
800 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) =
801 ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
802 (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8)));
803 nrewrite > (H x1 y1);
804 nrewrite > (H x2 y2);
805 nrewrite > (H x3 y3);
806 nrewrite > (H x4 y4);
807 nrewrite > (H x5 y5);
808 nrewrite > (H x6 y6);
809 nrewrite > (H x7 y7);
810 nrewrite > (H x8 y8);
816 (∀x,y.(f x y = true) → (x = y)) →
817 (∀a1,a2:Array8T T.(eq_ar8 T f a1 a2 = true) → (a1 = a2)).
820 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
822 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
823 nchange in H1:(%) with (
824 ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
825 (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) = true);
826 nrewrite > (H … (andb_true_true_r … H1));
827 nletin H2 ≝ (andb_true_true_l … H1);
828 nrewrite > (H … (andb_true_true_r … H2));
829 nletin H3 ≝ (andb_true_true_l … H2);
830 nrewrite > (H … (andb_true_true_r … H3));
831 nletin H4 ≝ (andb_true_true_l … H3);
832 nrewrite > (H … (andb_true_true_r … H4));
833 nletin H5 ≝ (andb_true_true_l … H4);
834 nrewrite > (H … (andb_true_true_r … H5));
835 nletin H6 ≝ (andb_true_true_l … H5);
836 nrewrite > (H … (andb_true_true_r … H6));
837 nletin H7 ≝ (andb_true_true_l … H6);
838 nrewrite > (H … (andb_true_true_r … H7));
839 nrewrite > (H … (andb_true_true_l … H7));
845 (∀x,y.(x = y) → (f x y = true)) →
846 (∀a1,a2:Array8T T.(a1 = a2) → (eq_ar8 T f a1 a2 = true)).
849 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
851 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
852 nrewrite > (ar8_destruct_1 … H1);
853 nrewrite > (ar8_destruct_2 … H1);
854 nrewrite > (ar8_destruct_3 … H1);
855 nrewrite > (ar8_destruct_4 … H1);
856 nrewrite > (ar8_destruct_5 … H1);
857 nrewrite > (ar8_destruct_6 … H1);
858 nrewrite > (ar8_destruct_7 … H1);
859 nrewrite > (ar8_destruct_8 … H1);
861 ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
862 (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8)) = true);
863 nrewrite > (H … (refl_eq …));
864 nrewrite > (H … (refl_eq …));
865 nrewrite > (H … (refl_eq …));
866 nrewrite > (H … (refl_eq …));
867 nrewrite > (H … (refl_eq …));
868 nrewrite > (H … (refl_eq …));
869 nrewrite > (H … (refl_eq …));
870 nrewrite > (H … (refl_eq …));
874 nlemma decidable_ar8_aux1 :
875 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
877 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
878 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
880 napply (H (ar8_destruct_1 … H1)).
883 nlemma decidable_ar8_aux2 :
884 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
886 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
887 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
889 napply (H (ar8_destruct_2 … H1)).
892 nlemma decidable_ar8_aux3 :
893 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
895 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
896 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
898 napply (H (ar8_destruct_3 … H1)).
901 nlemma decidable_ar8_aux4 :
902 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
904 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
905 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
907 napply (H (ar8_destruct_4 … H1)).
910 nlemma decidable_ar8_aux5 :
911 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
913 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
914 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
916 napply (H (ar8_destruct_5 … H1)).
919 nlemma decidable_ar8_aux6 :
920 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
922 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
923 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
925 napply (H (ar8_destruct_6 … H1)).
928 nlemma decidable_ar8_aux7 :
929 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
931 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
932 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
934 napply (H (ar8_destruct_7 … H1)).
937 nlemma decidable_ar8_aux8 :
938 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
940 (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
941 #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
943 napply (H (ar8_destruct_8 … H1)).
946 nlemma decidable_ar8 :
947 ∀T.(∀x,y:T.decidable (x = y)) →
948 (∀a1,a2:Array8T T.decidable (a1 = a2)).
950 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
951 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
953 napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
954 ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar8_aux1 T … H1))
955 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
956 ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar8_aux2 T … H2))
957 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
958 ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar8_aux3 T … H3))
959 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
960 ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar8_aux4 T … H4))
961 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
962 ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar8_aux5 T … H5))
963 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
964 ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar8_aux6 T … H6))
965 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
966 ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar8_aux7 T … H7))
967 ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
968 ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar8_aux8 T … H8))
969 ##| ##1: #H8; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
970 nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
971 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))