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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/exadecim/".
29 (*include "/media/VIRTUOSO/freescale/extra.ma".*)
30 include "freescale/extra.ma".
32 (* ***************************** *)
33 (* DEFINIZIONE DEGLI ESADECIMALI *)
34 (* ***************************** *)
36 inductive exadecim : Type ≝
59 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
60 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
61 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
62 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
64 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
65 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
66 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
67 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
69 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
70 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
71 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
72 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
74 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
75 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
76 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
77 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
79 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
80 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
81 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
82 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
84 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
85 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
86 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
87 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
89 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
90 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
91 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
92 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
94 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
95 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
96 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
97 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
99 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
100 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
101 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
102 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
104 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
105 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
106 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
107 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
109 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
110 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
111 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
112 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
114 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
115 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
116 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
117 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
119 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
120 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
121 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
122 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
124 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
125 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
126 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
127 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
129 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
130 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
131 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
132 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
134 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
135 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
136 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
137 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
145 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
146 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
147 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
148 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
150 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
151 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
152 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
153 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
155 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
156 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
157 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
158 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
160 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
161 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
162 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
163 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
165 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
166 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
167 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
168 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
170 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
171 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
172 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
173 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
175 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
176 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
177 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
178 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
180 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
181 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
182 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
183 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
185 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
186 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
187 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
188 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
190 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
191 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
192 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
193 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
195 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
196 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
197 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
198 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
200 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
201 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
202 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
203 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
205 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
206 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
207 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
208 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
210 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
211 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
212 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
213 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
215 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
216 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
217 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
218 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
220 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
221 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
222 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
223 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
231 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
232 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
233 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
234 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
236 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
237 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
238 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
239 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
241 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
242 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
243 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
244 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
246 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
247 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
248 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
249 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
251 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
252 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
253 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
254 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
256 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
257 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
258 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
259 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
261 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
262 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
263 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
264 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
266 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
267 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
268 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
269 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
271 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
272 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
273 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
274 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
276 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
277 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
278 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
279 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
281 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
282 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
283 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
284 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
286 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
287 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
288 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
289 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
291 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
292 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
293 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
294 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
296 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
297 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
298 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
299 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
301 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
302 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
303 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
304 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
306 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
307 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
308 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
309 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
317 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
318 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
319 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
320 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
322 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
323 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
324 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
325 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
327 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
328 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
329 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
330 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
332 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
333 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
334 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
335 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
337 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
338 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
339 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
340 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
342 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
343 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
344 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
345 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
347 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
348 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
349 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
350 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
352 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
353 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
354 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
355 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
357 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
358 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
359 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
360 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
362 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
363 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
364 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
365 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
367 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
368 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
369 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
370 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
372 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
373 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
374 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
375 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
377 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
378 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
379 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
380 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
382 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
383 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
384 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
385 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
387 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
388 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
389 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
390 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
392 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
393 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
394 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
395 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
403 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
404 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
405 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
406 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
408 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
409 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
410 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
411 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
413 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
414 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
415 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
416 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
418 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
419 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
420 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
421 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
423 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
424 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
425 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
426 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
428 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
429 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
430 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
431 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
433 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
434 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
435 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
436 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
438 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
439 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
440 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
441 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
443 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
444 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
445 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
446 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
448 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
449 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
450 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
451 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
453 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
454 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
455 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
456 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
458 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
459 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
460 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
461 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
463 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
464 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
465 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
466 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
468 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
469 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
470 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
471 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
473 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
474 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
475 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
476 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
478 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
479 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
480 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
481 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
486 λe1,e2:exadecim.match e1 with
488 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
489 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
490 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
491 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
493 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
494 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
495 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
496 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
498 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
499 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
500 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
501 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
503 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
504 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
505 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
506 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
508 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
509 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
510 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
511 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
513 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
514 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
515 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
516 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
518 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
519 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
520 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
521 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
523 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
524 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
525 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
526 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
528 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
529 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
530 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
531 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
533 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
534 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
535 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
536 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
538 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
539 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
540 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
541 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
543 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
544 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
545 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
546 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
548 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
549 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
550 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
551 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
553 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
554 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
555 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
556 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
558 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
559 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
560 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
561 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
563 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
564 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
565 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
566 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
571 λe1,e2:exadecim.match e1 with
573 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
574 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
575 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
576 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
578 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
579 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
580 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
581 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
583 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
584 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
585 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
586 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
588 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
589 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
590 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
591 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
593 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
594 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
595 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
596 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
598 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
599 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
600 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
601 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
603 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
604 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
605 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
606 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
608 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
609 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
610 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
611 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
613 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
614 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
615 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
616 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
618 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
619 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
620 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
621 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
623 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
624 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
625 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
626 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
628 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
629 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
630 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
631 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
633 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
634 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
635 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
636 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
638 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
639 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
640 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
641 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
643 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
644 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
645 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
646 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
648 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
649 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
650 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
651 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
656 λe1,e2:exadecim.match e1 with
658 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
659 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
660 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
661 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
663 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
664 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
665 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
666 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
668 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
669 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
670 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
671 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
673 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
674 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
675 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
676 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
678 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
679 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
680 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
681 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
683 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
684 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
685 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
686 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
688 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
689 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
690 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
691 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
693 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
694 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
695 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
696 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
698 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
699 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
700 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
701 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
703 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
704 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
705 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
706 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
708 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
709 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
710 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
711 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
713 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
714 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
715 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
716 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
718 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
719 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
720 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
721 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
723 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
724 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
725 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
726 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
728 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
729 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
730 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
731 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
733 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
734 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
735 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
736 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
739 (* operatore rotazione destra con carry *)
741 λe:exadecim.λc:bool.match c with
742 [ true ⇒ match e with
743 [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
744 | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
745 | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
746 | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
747 | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
748 | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
749 | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
750 | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
751 | false ⇒ match e with
752 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
753 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
754 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
755 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
756 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
757 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
758 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
759 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
762 (* operatore shift destro *)
764 λe:exadecim.match e with
765 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
766 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
767 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
768 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
769 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
770 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
771 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
772 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
774 (* operatore rotazione destra *)
776 λe:exadecim.match e with
777 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
778 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
779 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
780 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
782 (* operatore rotazione destra n-volte *)
783 let rec ror_ex_n (e:exadecim) (n:nat) on n ≝
786 | S n' ⇒ ror_ex_n (ror_ex e) n' ].
788 (* operatore rotazione sinistra con carry *)
790 λe:exadecim.λc:bool.match c with
791 [ true ⇒ match e with
792 [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
793 | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
794 | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
795 | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
796 | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
797 | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
798 | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
799 | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
800 | false ⇒ match e with
801 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
802 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
803 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
804 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
805 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
806 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
807 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
808 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
811 (* operatore shift sinistro *)
813 λe:exadecim.match e with
814 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
815 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
816 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
817 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
818 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
819 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
820 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
821 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
823 (* operatore rotazione sinistra *)
825 λe:exadecim.match e with
826 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
827 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
828 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
829 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
831 (* operatore rotazione sinistra n-volte *)
832 let rec rol_ex_n (e:exadecim) (n:nat) on n ≝
835 | S n' ⇒ rol_ex_n (rol_ex e) n' ].
837 (* operatore not/complemento a 1 *)
839 λe:exadecim.match e with
840 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
841 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
842 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
843 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
845 (* operatore somma con carry *)
847 λe1,e2:exadecim.λc:bool.
853 [ x0 ⇒ pair exadecim bool x1 false
854 | x1 ⇒ pair exadecim bool x2 false
855 | x2 ⇒ pair exadecim bool x3 false
856 | x3 ⇒ pair exadecim bool x4 false
857 | x4 ⇒ pair exadecim bool x5 false
858 | x5 ⇒ pair exadecim bool x6 false
859 | x6 ⇒ pair exadecim bool x7 false
860 | x7 ⇒ pair exadecim bool x8 false
861 | x8 ⇒ pair exadecim bool x9 false
862 | x9 ⇒ pair exadecim bool xA false
863 | xA ⇒ pair exadecim bool xB false
864 | xB ⇒ pair exadecim bool xC false
865 | xC ⇒ pair exadecim bool xD false
866 | xD ⇒ pair exadecim bool xE false
867 | xE ⇒ pair exadecim bool xF false
868 | xF ⇒ pair exadecim bool x0 true ]
871 [ x0 ⇒ pair exadecim bool x2 false
872 | x1 ⇒ pair exadecim bool x3 false
873 | x2 ⇒ pair exadecim bool x4 false
874 | x3 ⇒ pair exadecim bool x5 false
875 | x4 ⇒ pair exadecim bool x6 false
876 | x5 ⇒ pair exadecim bool x7 false
877 | x6 ⇒ pair exadecim bool x8 false
878 | x7 ⇒ pair exadecim bool x9 false
879 | x8 ⇒ pair exadecim bool xA false
880 | x9 ⇒ pair exadecim bool xB false
881 | xA ⇒ pair exadecim bool xC false
882 | xB ⇒ pair exadecim bool xD false
883 | xC ⇒ pair exadecim bool xE false
884 | xD ⇒ pair exadecim bool xF false
885 | xE ⇒ pair exadecim bool x0 true
886 | xF ⇒ pair exadecim bool x1 true ]
889 [ x0 ⇒ pair exadecim bool x3 false
890 | x1 ⇒ pair exadecim bool x4 false
891 | x2 ⇒ pair exadecim bool x5 false
892 | x3 ⇒ pair exadecim bool x6 false
893 | x4 ⇒ pair exadecim bool x7 false
894 | x5 ⇒ pair exadecim bool x8 false
895 | x6 ⇒ pair exadecim bool x9 false
896 | x7 ⇒ pair exadecim bool xA false
897 | x8 ⇒ pair exadecim bool xB false
898 | x9 ⇒ pair exadecim bool xC false
899 | xA ⇒ pair exadecim bool xD false
900 | xB ⇒ pair exadecim bool xE false
901 | xC ⇒ pair exadecim bool xF false
902 | xD ⇒ pair exadecim bool x0 true
903 | xE ⇒ pair exadecim bool x1 true
904 | xF ⇒ pair exadecim bool x2 true ]
907 [ x0 ⇒ pair exadecim bool x4 false
908 | x1 ⇒ pair exadecim bool x5 false
909 | x2 ⇒ pair exadecim bool x6 false
910 | x3 ⇒ pair exadecim bool x7 false
911 | x4 ⇒ pair exadecim bool x8 false
912 | x5 ⇒ pair exadecim bool x9 false
913 | x6 ⇒ pair exadecim bool xA false
914 | x7 ⇒ pair exadecim bool xB false
915 | x8 ⇒ pair exadecim bool xC false
916 | x9 ⇒ pair exadecim bool xD false
917 | xA ⇒ pair exadecim bool xE false
918 | xB ⇒ pair exadecim bool xF false
919 | xC ⇒ pair exadecim bool x0 true
920 | xD ⇒ pair exadecim bool x1 true
921 | xE ⇒ pair exadecim bool x2 true
922 | xF ⇒ pair exadecim bool x3 true ]
925 [ x0 ⇒ pair exadecim bool x5 false
926 | x1 ⇒ pair exadecim bool x6 false
927 | x2 ⇒ pair exadecim bool x7 false
928 | x3 ⇒ pair exadecim bool x8 false
929 | x4 ⇒ pair exadecim bool x9 false
930 | x5 ⇒ pair exadecim bool xA false
931 | x6 ⇒ pair exadecim bool xB false
932 | x7 ⇒ pair exadecim bool xC false
933 | x8 ⇒ pair exadecim bool xD false
934 | x9 ⇒ pair exadecim bool xE false
935 | xA ⇒ pair exadecim bool xF false
936 | xB ⇒ pair exadecim bool x0 true
937 | xC ⇒ pair exadecim bool x1 true
938 | xD ⇒ pair exadecim bool x2 true
939 | xE ⇒ pair exadecim bool x3 true
940 | xF ⇒ pair exadecim bool x4 true ]
943 [ x0 ⇒ pair exadecim bool x6 false
944 | x1 ⇒ pair exadecim bool x7 false
945 | x2 ⇒ pair exadecim bool x8 false
946 | x3 ⇒ pair exadecim bool x9 false
947 | x4 ⇒ pair exadecim bool xA false
948 | x5 ⇒ pair exadecim bool xB false
949 | x6 ⇒ pair exadecim bool xC false
950 | x7 ⇒ pair exadecim bool xD false
951 | x8 ⇒ pair exadecim bool xE false
952 | x9 ⇒ pair exadecim bool xF false
953 | xA ⇒ pair exadecim bool x0 true
954 | xB ⇒ pair exadecim bool x1 true
955 | xC ⇒ pair exadecim bool x2 true
956 | xD ⇒ pair exadecim bool x3 true
957 | xE ⇒ pair exadecim bool x4 true
958 | xF ⇒ pair exadecim bool x5 true ]
961 [ x0 ⇒ pair exadecim bool x7 false
962 | x1 ⇒ pair exadecim bool x8 false
963 | x2 ⇒ pair exadecim bool x9 false
964 | x3 ⇒ pair exadecim bool xA false
965 | x4 ⇒ pair exadecim bool xB false
966 | x5 ⇒ pair exadecim bool xC false
967 | x6 ⇒ pair exadecim bool xD false
968 | x7 ⇒ pair exadecim bool xE false
969 | x8 ⇒ pair exadecim bool xF false
970 | x9 ⇒ pair exadecim bool x0 true
971 | xA ⇒ pair exadecim bool x1 true
972 | xB ⇒ pair exadecim bool x2 true
973 | xC ⇒ pair exadecim bool x3 true
974 | xD ⇒ pair exadecim bool x4 true
975 | xE ⇒ pair exadecim bool x5 true
976 | xF ⇒ pair exadecim bool x6 true ]
979 [ x0 ⇒ pair exadecim bool x8 false
980 | x1 ⇒ pair exadecim bool x9 false
981 | x2 ⇒ pair exadecim bool xA false
982 | x3 ⇒ pair exadecim bool xB false
983 | x4 ⇒ pair exadecim bool xC false
984 | x5 ⇒ pair exadecim bool xD false
985 | x6 ⇒ pair exadecim bool xE false
986 | x7 ⇒ pair exadecim bool xF false
987 | x8 ⇒ pair exadecim bool x0 true
988 | x9 ⇒ pair exadecim bool x1 true
989 | xA ⇒ pair exadecim bool x2 true
990 | xB ⇒ pair exadecim bool x3 true
991 | xC ⇒ pair exadecim bool x4 true
992 | xD ⇒ pair exadecim bool x5 true
993 | xE ⇒ pair exadecim bool x6 true
994 | xF ⇒ pair exadecim bool x7 true ]
997 [ x0 ⇒ pair exadecim bool x9 false
998 | x1 ⇒ pair exadecim bool xA false
999 | x2 ⇒ pair exadecim bool xB false
1000 | x3 ⇒ pair exadecim bool xC false
1001 | x4 ⇒ pair exadecim bool xD false
1002 | x5 ⇒ pair exadecim bool xE false
1003 | x6 ⇒ pair exadecim bool xF false
1004 | x7 ⇒ pair exadecim bool x0 true
1005 | x8 ⇒ pair exadecim bool x1 true
1006 | x9 ⇒ pair exadecim bool x2 true
1007 | xA ⇒ pair exadecim bool x3 true
1008 | xB ⇒ pair exadecim bool x4 true
1009 | xC ⇒ pair exadecim bool x5 true
1010 | xD ⇒ pair exadecim bool x6 true
1011 | xE ⇒ pair exadecim bool x7 true
1012 | xF ⇒ pair exadecim bool x8 true ]
1015 [ x0 ⇒ pair exadecim bool xA false
1016 | x1 ⇒ pair exadecim bool xB false
1017 | x2 ⇒ pair exadecim bool xC false
1018 | x3 ⇒ pair exadecim bool xD false
1019 | x4 ⇒ pair exadecim bool xE false
1020 | x5 ⇒ pair exadecim bool xF false
1021 | x6 ⇒ pair exadecim bool x0 true
1022 | x7 ⇒ pair exadecim bool x1 true
1023 | x8 ⇒ pair exadecim bool x2 true
1024 | x9 ⇒ pair exadecim bool x3 true
1025 | xA ⇒ pair exadecim bool x4 true
1026 | xB ⇒ pair exadecim bool x5 true
1027 | xC ⇒ pair exadecim bool x6 true
1028 | xD ⇒ pair exadecim bool x7 true
1029 | xE ⇒ pair exadecim bool x8 true
1030 | xF ⇒ pair exadecim bool x9 true ]
1033 [ x0 ⇒ pair exadecim bool xB false
1034 | x1 ⇒ pair exadecim bool xC false
1035 | x2 ⇒ pair exadecim bool xD false
1036 | x3 ⇒ pair exadecim bool xE false
1037 | x4 ⇒ pair exadecim bool xF false
1038 | x5 ⇒ pair exadecim bool x0 true
1039 | x6 ⇒ pair exadecim bool x1 true
1040 | x7 ⇒ pair exadecim bool x2 true
1041 | x8 ⇒ pair exadecim bool x3 true
1042 | x9 ⇒ pair exadecim bool x4 true
1043 | xA ⇒ pair exadecim bool x5 true
1044 | xB ⇒ pair exadecim bool x6 true
1045 | xC ⇒ pair exadecim bool x7 true
1046 | xD ⇒ pair exadecim bool x8 true
1047 | xE ⇒ pair exadecim bool x9 true
1048 | xF ⇒ pair exadecim bool xA true ]
1051 [ x0 ⇒ pair exadecim bool xC false
1052 | x1 ⇒ pair exadecim bool xD false
1053 | x2 ⇒ pair exadecim bool xE false
1054 | x3 ⇒ pair exadecim bool xF false
1055 | x4 ⇒ pair exadecim bool x0 true
1056 | x5 ⇒ pair exadecim bool x1 true
1057 | x6 ⇒ pair exadecim bool x2 true
1058 | x7 ⇒ pair exadecim bool x3 true
1059 | x8 ⇒ pair exadecim bool x4 true
1060 | x9 ⇒ pair exadecim bool x5 true
1061 | xA ⇒ pair exadecim bool x6 true
1062 | xB ⇒ pair exadecim bool x7 true
1063 | xC ⇒ pair exadecim bool x8 true
1064 | xD ⇒ pair exadecim bool x9 true
1065 | xE ⇒ pair exadecim bool xA true
1066 | xF ⇒ pair exadecim bool xB true ]
1069 [ x0 ⇒ pair exadecim bool xD false
1070 | x1 ⇒ pair exadecim bool xE false
1071 | x2 ⇒ pair exadecim bool xF false
1072 | x3 ⇒ pair exadecim bool x0 true
1073 | x4 ⇒ pair exadecim bool x1 true
1074 | x5 ⇒ pair exadecim bool x2 true
1075 | x6 ⇒ pair exadecim bool x3 true
1076 | x7 ⇒ pair exadecim bool x4 true
1077 | x8 ⇒ pair exadecim bool x5 true
1078 | x9 ⇒ pair exadecim bool x6 true
1079 | xA ⇒ pair exadecim bool x7 true
1080 | xB ⇒ pair exadecim bool x8 true
1081 | xC ⇒ pair exadecim bool x9 true
1082 | xD ⇒ pair exadecim bool xA true
1083 | xE ⇒ pair exadecim bool xB true
1084 | xF ⇒ pair exadecim bool xC true ]
1087 [ x0 ⇒ pair exadecim bool xE false
1088 | x1 ⇒ pair exadecim bool xF false
1089 | x2 ⇒ pair exadecim bool x0 true
1090 | x3 ⇒ pair exadecim bool x1 true
1091 | x4 ⇒ pair exadecim bool x2 true
1092 | x5 ⇒ pair exadecim bool x3 true
1093 | x6 ⇒ pair exadecim bool x4 true
1094 | x7 ⇒ pair exadecim bool x5 true
1095 | x8 ⇒ pair exadecim bool x6 true
1096 | x9 ⇒ pair exadecim bool x7 true
1097 | xA ⇒ pair exadecim bool x8 true
1098 | xB ⇒ pair exadecim bool x9 true
1099 | xC ⇒ pair exadecim bool xA true
1100 | xD ⇒ pair exadecim bool xB true
1101 | xE ⇒ pair exadecim bool xC true
1102 | xF ⇒ pair exadecim bool xD true ]
1105 [ x0 ⇒ pair exadecim bool xF false
1106 | x1 ⇒ pair exadecim bool x0 true
1107 | x2 ⇒ pair exadecim bool x1 true
1108 | x3 ⇒ pair exadecim bool x2 true
1109 | x4 ⇒ pair exadecim bool x3 true
1110 | x5 ⇒ pair exadecim bool x4 true
1111 | x6 ⇒ pair exadecim bool x5 true
1112 | x7 ⇒ pair exadecim bool x6 true
1113 | x8 ⇒ pair exadecim bool x7 true
1114 | x9 ⇒ pair exadecim bool x8 true
1115 | xA ⇒ pair exadecim bool x9 true
1116 | xB ⇒ pair exadecim bool xA true
1117 | xC ⇒ pair exadecim bool xB true
1118 | xD ⇒ pair exadecim bool xC true
1119 | xE ⇒ pair exadecim bool xD true
1120 | xF ⇒ pair exadecim bool xE true ]
1123 [ x0 ⇒ pair exadecim bool x0 true
1124 | x1 ⇒ pair exadecim bool x1 true
1125 | x2 ⇒ pair exadecim bool x2 true
1126 | x3 ⇒ pair exadecim bool x3 true
1127 | x4 ⇒ pair exadecim bool x4 true
1128 | x5 ⇒ pair exadecim bool x5 true
1129 | x6 ⇒ pair exadecim bool x6 true
1130 | x7 ⇒ pair exadecim bool x7 true
1131 | x8 ⇒ pair exadecim bool x8 true
1132 | x9 ⇒ pair exadecim bool x9 true
1133 | xA ⇒ pair exadecim bool xA true
1134 | xB ⇒ pair exadecim bool xB true
1135 | xC ⇒ pair exadecim bool xC true
1136 | xD ⇒ pair exadecim bool xD true
1137 | xE ⇒ pair exadecim bool xE true
1138 | xF ⇒ pair exadecim bool xF true ]
1144 [ x0 ⇒ pair exadecim bool x0 false
1145 | x1 ⇒ pair exadecim bool x1 false
1146 | x2 ⇒ pair exadecim bool x2 false
1147 | x3 ⇒ pair exadecim bool x3 false
1148 | x4 ⇒ pair exadecim bool x4 false
1149 | x5 ⇒ pair exadecim bool x5 false
1150 | x6 ⇒ pair exadecim bool x6 false
1151 | x7 ⇒ pair exadecim bool x7 false
1152 | x8 ⇒ pair exadecim bool x8 false
1153 | x9 ⇒ pair exadecim bool x9 false
1154 | xA ⇒ pair exadecim bool xA false
1155 | xB ⇒ pair exadecim bool xB false
1156 | xC ⇒ pair exadecim bool xC false
1157 | xD ⇒ pair exadecim bool xD false
1158 | xE ⇒ pair exadecim bool xE false
1159 | xF ⇒ pair exadecim bool xF false ]
1162 [ x0 ⇒ pair exadecim bool x1 false
1163 | x1 ⇒ pair exadecim bool x2 false
1164 | x2 ⇒ pair exadecim bool x3 false
1165 | x3 ⇒ pair exadecim bool x4 false
1166 | x4 ⇒ pair exadecim bool x5 false
1167 | x5 ⇒ pair exadecim bool x6 false
1168 | x6 ⇒ pair exadecim bool x7 false
1169 | x7 ⇒ pair exadecim bool x8 false
1170 | x8 ⇒ pair exadecim bool x9 false
1171 | x9 ⇒ pair exadecim bool xA false
1172 | xA ⇒ pair exadecim bool xB false
1173 | xB ⇒ pair exadecim bool xC false
1174 | xC ⇒ pair exadecim bool xD false
1175 | xD ⇒ pair exadecim bool xE false
1176 | xE ⇒ pair exadecim bool xF false
1177 | xF ⇒ pair exadecim bool x0 true ]
1180 [ x0 ⇒ pair exadecim bool x2 false
1181 | x1 ⇒ pair exadecim bool x3 false
1182 | x2 ⇒ pair exadecim bool x4 false
1183 | x3 ⇒ pair exadecim bool x5 false
1184 | x4 ⇒ pair exadecim bool x6 false
1185 | x5 ⇒ pair exadecim bool x7 false
1186 | x6 ⇒ pair exadecim bool x8 false
1187 | x7 ⇒ pair exadecim bool x9 false
1188 | x8 ⇒ pair exadecim bool xA false
1189 | x9 ⇒ pair exadecim bool xB false
1190 | xA ⇒ pair exadecim bool xC false
1191 | xB ⇒ pair exadecim bool xD false
1192 | xC ⇒ pair exadecim bool xE false
1193 | xD ⇒ pair exadecim bool xF false
1194 | xE ⇒ pair exadecim bool x0 true
1195 | xF ⇒ pair exadecim bool x1 true ]
1198 [ x0 ⇒ pair exadecim bool x3 false
1199 | x1 ⇒ pair exadecim bool x4 false
1200 | x2 ⇒ pair exadecim bool x5 false
1201 | x3 ⇒ pair exadecim bool x6 false
1202 | x4 ⇒ pair exadecim bool x7 false
1203 | x5 ⇒ pair exadecim bool x8 false
1204 | x6 ⇒ pair exadecim bool x9 false
1205 | x7 ⇒ pair exadecim bool xA false
1206 | x8 ⇒ pair exadecim bool xB false
1207 | x9 ⇒ pair exadecim bool xC false
1208 | xA ⇒ pair exadecim bool xD false
1209 | xB ⇒ pair exadecim bool xE false
1210 | xC ⇒ pair exadecim bool xF false
1211 | xD ⇒ pair exadecim bool x0 true
1212 | xE ⇒ pair exadecim bool x1 true
1213 | xF ⇒ pair exadecim bool x2 true ]
1216 [ x0 ⇒ pair exadecim bool x4 false
1217 | x1 ⇒ pair exadecim bool x5 false
1218 | x2 ⇒ pair exadecim bool x6 false
1219 | x3 ⇒ pair exadecim bool x7 false
1220 | x4 ⇒ pair exadecim bool x8 false
1221 | x5 ⇒ pair exadecim bool x9 false
1222 | x6 ⇒ pair exadecim bool xA false
1223 | x7 ⇒ pair exadecim bool xB false
1224 | x8 ⇒ pair exadecim bool xC false
1225 | x9 ⇒ pair exadecim bool xD false
1226 | xA ⇒ pair exadecim bool xE false
1227 | xB ⇒ pair exadecim bool xF false
1228 | xC ⇒ pair exadecim bool x0 true
1229 | xD ⇒ pair exadecim bool x1 true
1230 | xE ⇒ pair exadecim bool x2 true
1231 | xF ⇒ pair exadecim bool x3 true ]
1234 [ x0 ⇒ pair exadecim bool x5 false
1235 | x1 ⇒ pair exadecim bool x6 false
1236 | x2 ⇒ pair exadecim bool x7 false
1237 | x3 ⇒ pair exadecim bool x8 false
1238 | x4 ⇒ pair exadecim bool x9 false
1239 | x5 ⇒ pair exadecim bool xA false
1240 | x6 ⇒ pair exadecim bool xB false
1241 | x7 ⇒ pair exadecim bool xC false
1242 | x8 ⇒ pair exadecim bool xD false
1243 | x9 ⇒ pair exadecim bool xE false
1244 | xA ⇒ pair exadecim bool xF false
1245 | xB ⇒ pair exadecim bool x0 true
1246 | xC ⇒ pair exadecim bool x1 true
1247 | xD ⇒ pair exadecim bool x2 true
1248 | xE ⇒ pair exadecim bool x3 true
1249 | xF ⇒ pair exadecim bool x4 true ]
1252 [ x0 ⇒ pair exadecim bool x6 false
1253 | x1 ⇒ pair exadecim bool x7 false
1254 | x2 ⇒ pair exadecim bool x8 false
1255 | x3 ⇒ pair exadecim bool x9 false
1256 | x4 ⇒ pair exadecim bool xA false
1257 | x5 ⇒ pair exadecim bool xB false
1258 | x6 ⇒ pair exadecim bool xC false
1259 | x7 ⇒ pair exadecim bool xD false
1260 | x8 ⇒ pair exadecim bool xE false
1261 | x9 ⇒ pair exadecim bool xF false
1262 | xA ⇒ pair exadecim bool x0 true
1263 | xB ⇒ pair exadecim bool x1 true
1264 | xC ⇒ pair exadecim bool x2 true
1265 | xD ⇒ pair exadecim bool x3 true
1266 | xE ⇒ pair exadecim bool x4 true
1267 | xF ⇒ pair exadecim bool x5 true ]
1270 [ x0 ⇒ pair exadecim bool x7 false
1271 | x1 ⇒ pair exadecim bool x8 false
1272 | x2 ⇒ pair exadecim bool x9 false
1273 | x3 ⇒ pair exadecim bool xA false
1274 | x4 ⇒ pair exadecim bool xB false
1275 | x5 ⇒ pair exadecim bool xC false
1276 | x6 ⇒ pair exadecim bool xD false
1277 | x7 ⇒ pair exadecim bool xE false
1278 | x8 ⇒ pair exadecim bool xF false
1279 | x9 ⇒ pair exadecim bool x0 true
1280 | xA ⇒ pair exadecim bool x1 true
1281 | xB ⇒ pair exadecim bool x2 true
1282 | xC ⇒ pair exadecim bool x3 true
1283 | xD ⇒ pair exadecim bool x4 true
1284 | xE ⇒ pair exadecim bool x5 true
1285 | xF ⇒ pair exadecim bool x6 true ]
1288 [ x0 ⇒ pair exadecim bool x8 false
1289 | x1 ⇒ pair exadecim bool x9 false
1290 | x2 ⇒ pair exadecim bool xA false
1291 | x3 ⇒ pair exadecim bool xB false
1292 | x4 ⇒ pair exadecim bool xC false
1293 | x5 ⇒ pair exadecim bool xD false
1294 | x6 ⇒ pair exadecim bool xE false
1295 | x7 ⇒ pair exadecim bool xF false
1296 | x8 ⇒ pair exadecim bool x0 true
1297 | x9 ⇒ pair exadecim bool x1 true
1298 | xA ⇒ pair exadecim bool x2 true
1299 | xB ⇒ pair exadecim bool x3 true
1300 | xC ⇒ pair exadecim bool x4 true
1301 | xD ⇒ pair exadecim bool x5 true
1302 | xE ⇒ pair exadecim bool x6 true
1303 | xF ⇒ pair exadecim bool x7 true ]
1306 [ x0 ⇒ pair exadecim bool x9 false
1307 | x1 ⇒ pair exadecim bool xA false
1308 | x2 ⇒ pair exadecim bool xB false
1309 | x3 ⇒ pair exadecim bool xC false
1310 | x4 ⇒ pair exadecim bool xD false
1311 | x5 ⇒ pair exadecim bool xE false
1312 | x6 ⇒ pair exadecim bool xF false
1313 | x7 ⇒ pair exadecim bool x0 true
1314 | x8 ⇒ pair exadecim bool x1 true
1315 | x9 ⇒ pair exadecim bool x2 true
1316 | xA ⇒ pair exadecim bool x3 true
1317 | xB ⇒ pair exadecim bool x4 true
1318 | xC ⇒ pair exadecim bool x5 true
1319 | xD ⇒ pair exadecim bool x6 true
1320 | xE ⇒ pair exadecim bool x7 true
1321 | xF ⇒ pair exadecim bool x8 true ]
1324 [ x0 ⇒ pair exadecim bool xA false
1325 | x1 ⇒ pair exadecim bool xB false
1326 | x2 ⇒ pair exadecim bool xC false
1327 | x3 ⇒ pair exadecim bool xD false
1328 | x4 ⇒ pair exadecim bool xE false
1329 | x5 ⇒ pair exadecim bool xF false
1330 | x6 ⇒ pair exadecim bool x0 true
1331 | x7 ⇒ pair exadecim bool x1 true
1332 | x8 ⇒ pair exadecim bool x2 true
1333 | x9 ⇒ pair exadecim bool x3 true
1334 | xA ⇒ pair exadecim bool x4 true
1335 | xB ⇒ pair exadecim bool x5 true
1336 | xC ⇒ pair exadecim bool x6 true
1337 | xD ⇒ pair exadecim bool x7 true
1338 | xE ⇒ pair exadecim bool x8 true
1339 | xF ⇒ pair exadecim bool x9 true ]
1342 [ x0 ⇒ pair exadecim bool xB false
1343 | x1 ⇒ pair exadecim bool xC false
1344 | x2 ⇒ pair exadecim bool xD false
1345 | x3 ⇒ pair exadecim bool xE false
1346 | x4 ⇒ pair exadecim bool xF false
1347 | x5 ⇒ pair exadecim bool x0 true
1348 | x6 ⇒ pair exadecim bool x1 true
1349 | x7 ⇒ pair exadecim bool x2 true
1350 | x8 ⇒ pair exadecim bool x3 true
1351 | x9 ⇒ pair exadecim bool x4 true
1352 | xA ⇒ pair exadecim bool x5 true
1353 | xB ⇒ pair exadecim bool x6 true
1354 | xC ⇒ pair exadecim bool x7 true
1355 | xD ⇒ pair exadecim bool x8 true
1356 | xE ⇒ pair exadecim bool x9 true
1357 | xF ⇒ pair exadecim bool xA true ]
1360 [ x0 ⇒ pair exadecim bool xC false
1361 | x1 ⇒ pair exadecim bool xD false
1362 | x2 ⇒ pair exadecim bool xE false
1363 | x3 ⇒ pair exadecim bool xF false
1364 | x4 ⇒ pair exadecim bool x0 true
1365 | x5 ⇒ pair exadecim bool x1 true
1366 | x6 ⇒ pair exadecim bool x2 true
1367 | x7 ⇒ pair exadecim bool x3 true
1368 | x8 ⇒ pair exadecim bool x4 true
1369 | x9 ⇒ pair exadecim bool x5 true
1370 | xA ⇒ pair exadecim bool x6 true
1371 | xB ⇒ pair exadecim bool x7 true
1372 | xC ⇒ pair exadecim bool x8 true
1373 | xD ⇒ pair exadecim bool x9 true
1374 | xE ⇒ pair exadecim bool xA true
1375 | xF ⇒ pair exadecim bool xB true ]
1378 [ x0 ⇒ pair exadecim bool xD false
1379 | x1 ⇒ pair exadecim bool xE false
1380 | x2 ⇒ pair exadecim bool xF false
1381 | x3 ⇒ pair exadecim bool x0 true
1382 | x4 ⇒ pair exadecim bool x1 true
1383 | x5 ⇒ pair exadecim bool x2 true
1384 | x6 ⇒ pair exadecim bool x3 true
1385 | x7 ⇒ pair exadecim bool x4 true
1386 | x8 ⇒ pair exadecim bool x5 true
1387 | x9 ⇒ pair exadecim bool x6 true
1388 | xA ⇒ pair exadecim bool x7 true
1389 | xB ⇒ pair exadecim bool x8 true
1390 | xC ⇒ pair exadecim bool x9 true
1391 | xD ⇒ pair exadecim bool xA true
1392 | xE ⇒ pair exadecim bool xB true
1393 | xF ⇒ pair exadecim bool xC true ]
1396 [ x0 ⇒ pair exadecim bool xE false
1397 | x1 ⇒ pair exadecim bool xF false
1398 | x2 ⇒ pair exadecim bool x0 true
1399 | x3 ⇒ pair exadecim bool x1 true
1400 | x4 ⇒ pair exadecim bool x2 true
1401 | x5 ⇒ pair exadecim bool x3 true
1402 | x6 ⇒ pair exadecim bool x4 true
1403 | x7 ⇒ pair exadecim bool x5 true
1404 | x8 ⇒ pair exadecim bool x6 true
1405 | x9 ⇒ pair exadecim bool x7 true
1406 | xA ⇒ pair exadecim bool x8 true
1407 | xB ⇒ pair exadecim bool x9 true
1408 | xC ⇒ pair exadecim bool xA true
1409 | xD ⇒ pair exadecim bool xB true
1410 | xE ⇒ pair exadecim bool xC true
1411 | xF ⇒ pair exadecim bool xD true ]
1414 [ x0 ⇒ pair exadecim bool xF false
1415 | x1 ⇒ pair exadecim bool x0 true
1416 | x2 ⇒ pair exadecim bool x1 true
1417 | x3 ⇒ pair exadecim bool x2 true
1418 | x4 ⇒ pair exadecim bool x3 true
1419 | x5 ⇒ pair exadecim bool x4 true
1420 | x6 ⇒ pair exadecim bool x5 true
1421 | x7 ⇒ pair exadecim bool x6 true
1422 | x8 ⇒ pair exadecim bool x7 true
1423 | x9 ⇒ pair exadecim bool x8 true
1424 | xA ⇒ pair exadecim bool x9 true
1425 | xB ⇒ pair exadecim bool xA true
1426 | xC ⇒ pair exadecim bool xB true
1427 | xD ⇒ pair exadecim bool xC true
1428 | xE ⇒ pair exadecim bool xD true
1429 | xF ⇒ pair exadecim bool xE true ]
1433 (* operatore somma senza carry *)
1434 definition plus_exnc ≝
1435 λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
1437 (* operatore carry della somma *)
1438 definition plus_exc ≝
1439 λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
1441 (* operatore Most Significant Bit *)
1443 λe:exadecim.match e with
1444 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1445 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1446 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
1447 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
1449 (* esadecimali → naturali *)
1450 definition nat_of_exadecim ≝
1453 [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2 | x3 ⇒ 3 | x4 ⇒ 4 | x5 ⇒ 5 | x6 ⇒ 6 | x7 ⇒ 7
1454 | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
1456 coercion cic:/matita/freescale/exadecim/nat_of_exadecim.con.
1458 (* naturali → esadecimali *)
1459 let rec exadecim_of_nat n ≝
1460 match n with [ O ⇒ x0 | S n ⇒
1461 match n with [ O ⇒ x1 | S n ⇒
1462 match n with [ O ⇒ x2 | S n ⇒
1463 match n with [ O ⇒ x3 | S n ⇒
1464 match n with [ O ⇒ x4 | S n ⇒
1465 match n with [ O ⇒ x5 | S n ⇒
1466 match n with [ O ⇒ x6 | S n ⇒
1467 match n with [ O ⇒ x7 | S n ⇒
1468 match n with [ O ⇒ x8 | S n ⇒
1469 match n with [ O ⇒ x9 | S n ⇒
1470 match n with [ O ⇒ xA | S n ⇒
1471 match n with [ O ⇒ xB | S n ⇒
1472 match n with [ O ⇒ xC | S n ⇒
1473 match n with [ O ⇒ xD | S n ⇒
1474 match n with [ O ⇒ xE | S n ⇒
1475 match n with [ O ⇒ xF | S n ⇒ exadecim_of_nat n ]]]]]]]]]]]]]]]].
1477 (* operatore predecessore *)
1478 definition pred_ex ≝
1481 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1482 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1484 (* operatore successore *)
1485 definition succ_ex ≝
1488 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1489 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1491 (* operatore neg/complemento a 2 *)
1492 definition compl_ex ≝
1493 λe:exadecim.match e with
1494 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1495 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1496 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1497 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1499 (* iteratore sugli esadecimali *)
1500 definition forall_exadecim ≝ λP.
1501 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1502 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
1504 (* ********************** *)
1505 (* TEOREMI/LEMMMI/ASSIOMI *)
1506 (* ********************** *)
1508 (* ESPERIMENTO UTILIZZO DELL'ITERATORE *)
1511 lemma forall_exadecim_eqProp_left_aux :
1512 ∀P.(∀e:exadecim.P e = true) →
1513 ((P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1514 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF) = true).
1516 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1517 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1518 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1519 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1520 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1521 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1522 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1523 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1527 lemma forall_exadecim_eqProp_left :
1528 ∀P.(∀e:exadecim. P e = true) → (forall_exadecim (λe.P e) = true).
1531 [ simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
1532 simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
1536 lemma forall_exadecim_eqProp_right_aux :
1537 ∀P.((P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1538 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF) = true) →
1539 (∀e:exadecim.P e = true).
1543 lemma forall_exadecim_eqProp_right :
1544 ∀P.(forall_exadecim (λe.P e) = true) → (∀e:exadecim.P e = true).
1547 [ simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
1548 simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
1552 lemma lt_nat_of_exadecim_16_forall: ∀e.ltb (nat_of_exadecim e) 16 = true.
1553 apply forall_exadecim_eqProp_right;
1558 (* FINE DELL'ESPERIMENTO *)
1560 lemma lt_nat_of_exadecim_16: ∀e.nat_of_exadecim e < 16.
1567 lemma exadecim_of_nat_mod:
1568 ∀n.exadecim_of_nat n = exadecim_of_nat (n \mod 16).
1570 apply (nat_elim1 n); intro;
1571 cases m; [ intro; reflexivity | ];
1572 cases n1; [ intro; reflexivity | ];
1573 cases n2; [ intro; reflexivity | ];
1574 cases n3; [ intro; reflexivity | ];
1575 cases n4; [ intro; reflexivity | ];
1576 cases n5; [ intro; reflexivity | ];
1577 cases n6; [ intro; reflexivity | ];
1578 cases n7; [ intro; reflexivity | ];
1579 cases n8; [ intro; reflexivity | ];
1580 cases n9; [ intro; reflexivity | ];
1581 cases n10; [ intro; reflexivity | ];
1582 cases n11; [ intro; reflexivity | ];
1583 cases n12; [ intro; reflexivity | ];
1584 cases n13; [ intro; reflexivity | ];
1585 cases n14; [ intro; reflexivity | ];
1586 cases n15; [ intro; reflexivity | ];
1588 change in ⊢ (? ? % ?) with (exadecim_of_nat n16);
1589 change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
1591 change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
1600 lemma nat_of_exadecim_exadecim_of_nat:
1601 ∀n. nat_of_exadecim (exadecim_of_nat n) = n \mod 16.
1603 rewrite > exadecim_of_nat_mod;
1604 generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
1605 generalize in match (n \mod 16); intro;
1606 cases n1; [ intro; reflexivity | ];
1607 cases n2; [ intro; reflexivity | ];
1608 cases n3; [ intro; reflexivity | ];
1609 cases n4; [ intro; reflexivity | ];
1610 cases n5; [ intro; reflexivity | ];
1611 cases n6; [ intro; reflexivity | ];
1612 cases n7; [ intro; reflexivity | ];
1613 cases n8; [ intro; reflexivity | ];
1614 cases n9; [ intro; reflexivity | ];
1615 cases n10; [ intro; reflexivity | ];
1616 cases n11 [ intro; reflexivity | ];
1617 cases n12; [ intro; reflexivity | ];
1618 cases n13; [ intro; reflexivity | ];
1619 cases n14; [ intro; reflexivity | ];
1620 cases n15; [ intro; reflexivity | ];
1621 cases n16; [ intro; reflexivity | ];
1630 lemma exadecim_of_nat_nat_of_exadecim:
1631 ∀e.exadecim_of_nat (nat_of_exadecim e) = e.
1639 match plus_ex b1 b2 c with
1640 [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
1642 elim b1; (elim b2; (elim c; normalize; reflexivity)).
1645 lemma eq_eqex_S_x0_false:
1646 ∀n. n < 15 → eq_ex x0 (exadecim_of_nat (S n)) = false.
1648 cases n 0; [ intro; simplify; reflexivity | clear n];
1649 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1650 cases n 0; [ intro; simplify; reflexivity | clear n];
1651 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1652 cases n 0; [ intro; simplify; reflexivity | clear n];
1653 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1654 cases n 0; [ intro; simplify; reflexivity | clear n];
1655 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1656 cases n 0; [ intro; simplify; reflexivity | clear n];
1657 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1658 cases n 0; [ intro; simplify; reflexivity | clear n];
1659 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1660 cases n 0; [ intro; simplify; reflexivity | clear n];
1661 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1662 cases n 0; [ intro; simplify; reflexivity | clear n];
1666 [ elim (not_le_Sn_O ? Hcut)
1667 | do 15 (apply le_S_S_to_le);
1672 lemma eqex_true_to_eq: ∀b,b'. eq_ex b b' = true → b=b'.
1678 first [ reflexivity | destruct H ].
1681 lemma eqex_false_to_not_eq: ∀b,b'. eq_ex b b' = false → b ≠ b'.
1694 lemma ok_lt_ex : ∀e1,e2:exadecim.
1695 lt_ex e1 e2 = ltb e1 e2.
1703 lemma ok_le_ex : ∀e1,e2:exadecim.
1704 le_ex e1 e2 = leb e1 e2.
1712 lemma ok_gt_ex : ∀e1,e2:exadecim.
1713 gt_ex e1 e2 = notb (leb e1 e2).
1721 lemma ok_ge_ex : ∀e1,e2:exadecim.
1722 ge_ex e1 e2 = notb (ltb e1 e2).
1730 lemma ok_pred_ex : ∀e:exadecim.
1731 pred_ex e = plus_exnc e xF.
1738 lemma ok_succ_ex : ∀e:exadecim.
1739 succ_ex e = plus_exnc e x1.
1746 lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
1749 (exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
1754 simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
1755 simplify in ⊢ (? ? ? (? ? ? ? %));
1756 simplify in ⊢ (? ? ? (? ? ? % ?));
1757 simplify in ⊢ (? ? % ?);
1761 lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
1764 (exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
1769 simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
1770 simplify in ⊢ (? ? ? (? ? ? % ?));
1771 simplify in ⊢ (? ? ? (? ? ? ? (? %)));
1772 simplify in ⊢ (? ? ? (? ? ? ? %));
1773 simplify in ⊢ (? ? % ?);
1777 lemma ok_shr_ex : ∀e:exadecim.
1780 (exadecim_of_nat (e/2))
1784 simplify in ⊢ (? ? ? (? ? ? % ?));
1785 simplify in ⊢ (? ? ? (? ? ? ? %));
1786 simplify in ⊢ (? ? % ?);
1790 lemma ok_shl_ex : ∀e:exadecim.
1793 (exadecim_of_nat (mod (e*2) 16))
1797 simplify in ⊢ (? ? ? (? ? ? % ?));
1798 simplify in ⊢ (? ? ? (? ? ? ? (? %)));
1799 simplify in ⊢ (? ? ? (? ? ? ? %));
1800 simplify in ⊢ (? ? % ?);
1804 lemma ok_not_ex : ∀e:exadecim.
1805 e + (not_ex e) = 15.
1812 lemma ok_compl_ex : ∀e:exadecim.
1813 e + (compl_ex e) = match gt_ex e x0 with [ true ⇒ 16 | false ⇒ 0 ].
1820 lemma ok_MSB_ex : ∀e:exadecim.
1821 MSB_ex e = notb (ltb e 8).