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 include "freescale/extra.ma".
29 (* ***************************** *)
30 (* DEFINIZIONE DEGLI ESADECIMALI *)
31 (* ***************************** *)
33 inductive exadecim : Type ≝
56 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
57 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
58 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
59 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
61 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
62 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
63 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
64 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
66 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
67 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
68 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
69 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
71 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
72 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
73 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
74 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
76 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
77 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
78 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
79 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
81 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
82 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
83 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
84 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
86 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
87 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
88 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
89 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
91 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
92 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
93 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
94 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
96 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
97 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
98 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
99 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
101 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
102 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
103 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
104 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
106 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
107 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
108 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
109 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
111 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
112 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
113 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
114 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
116 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
117 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
118 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
119 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
121 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
122 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
123 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
124 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
126 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
127 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
128 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
129 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
131 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
132 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
133 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
134 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
142 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
143 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
144 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
145 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
147 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
148 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
149 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
150 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
152 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
153 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
154 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
155 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
157 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
158 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
159 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
160 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
162 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
163 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
164 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
165 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
167 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
168 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
169 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
170 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
172 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
173 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
174 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
175 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
177 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
178 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
179 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
180 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
182 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
183 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
184 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
185 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
187 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
188 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
189 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
190 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
192 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
193 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
194 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
195 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
197 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
198 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
199 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
200 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
202 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
203 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
204 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
205 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
207 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
208 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
209 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
210 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
212 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
213 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
214 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
215 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
217 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
218 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
219 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
220 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
228 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
229 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
230 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
231 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
233 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
234 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
235 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
236 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
238 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
239 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
240 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
241 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
243 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
244 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
245 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
246 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
248 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
249 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
250 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
251 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
253 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
254 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
255 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
256 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
258 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
259 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
260 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
261 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
263 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
264 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
265 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
266 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
268 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
269 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
270 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
271 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
273 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
274 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
275 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
276 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
278 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
279 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
280 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
281 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
283 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
284 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
285 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
286 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
288 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
289 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
290 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
291 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
293 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
294 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
295 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
296 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
298 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
299 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
300 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
301 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
303 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
304 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
305 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
306 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
314 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
315 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
316 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
317 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
319 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
320 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
321 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
322 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
324 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
325 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
326 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
327 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
329 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
330 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
331 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
332 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
334 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
335 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
336 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
337 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
339 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
340 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
341 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
342 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
344 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
345 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
346 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
347 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
349 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
350 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
351 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
352 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
354 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
355 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
356 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
357 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
359 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
360 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
361 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
362 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
364 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
365 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
366 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
367 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
369 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
370 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
371 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
372 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
374 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
375 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
376 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
377 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
379 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
380 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
381 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
382 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
384 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
385 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
386 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
387 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
389 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
390 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
391 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
392 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
400 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
401 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
402 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
403 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
405 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
406 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
407 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
408 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
410 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
411 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
412 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
413 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
415 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
416 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
417 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
418 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
420 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
421 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
422 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
423 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
425 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
426 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
427 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
428 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
430 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
431 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
432 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
433 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
435 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
436 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
437 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
438 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
440 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
441 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
442 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
443 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
445 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
446 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
447 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
448 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
450 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
451 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
452 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
453 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
455 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
456 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
457 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
458 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
460 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
461 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
462 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
463 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
465 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
466 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
467 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
468 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
470 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
471 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
472 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
473 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
475 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
476 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
477 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
478 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
483 λe1,e2:exadecim.match e1 with
485 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
486 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
487 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
488 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
490 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
491 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
492 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
493 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
495 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
496 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
497 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
498 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
500 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
501 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
502 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
503 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
505 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
506 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
507 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
508 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
510 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
511 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
512 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
513 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
515 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
516 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
517 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
518 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
520 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
521 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
522 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
523 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
525 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
526 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
527 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
528 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
530 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
531 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
532 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
533 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
535 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
536 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
537 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
538 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
540 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
541 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
542 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
543 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
545 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
546 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
547 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
548 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
550 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
551 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
552 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
553 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
555 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
556 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
557 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
558 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
560 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
561 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
562 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
563 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
568 λe1,e2:exadecim.match e1 with
570 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
571 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
572 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
573 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
575 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
576 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
577 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
578 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
580 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
581 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
582 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
583 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
585 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
586 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
587 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
588 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
590 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
591 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
592 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
593 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
595 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
596 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
597 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
598 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
600 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
601 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
602 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
603 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
605 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
606 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
607 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
608 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
610 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
611 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
612 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
613 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
615 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
616 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
617 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
618 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
620 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
621 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
622 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
623 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
625 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
626 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
627 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
628 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
630 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
631 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
632 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
633 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
635 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
636 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
637 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
638 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
640 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
641 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
642 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
643 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
645 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
646 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
647 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
648 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
653 λe1,e2:exadecim.match e1 with
655 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
656 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
657 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
658 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
660 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
661 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
662 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
663 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
665 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
666 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
667 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
668 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
670 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
671 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
672 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
673 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
675 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
676 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
677 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
678 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
680 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
681 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
682 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
683 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
685 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
686 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
687 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
688 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
690 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
691 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
692 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
693 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
695 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
696 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
697 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
698 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
700 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
701 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
702 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
703 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
705 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
706 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
707 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
708 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
710 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
711 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
712 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
713 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
715 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
716 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
717 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
718 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
720 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
721 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
722 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
723 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
725 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
726 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
727 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
728 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
730 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
731 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
732 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
733 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
736 (* operatore rotazione destra con carry *)
738 λe:exadecim.λc:bool.match c with
739 [ true ⇒ match e with
740 [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
741 | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
742 | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
743 | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
744 | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
745 | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
746 | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
747 | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
748 | false ⇒ match e with
749 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
750 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
751 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
752 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
753 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
754 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
755 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
756 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
759 (* operatore shift destro *)
761 λe:exadecim.match e with
762 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
763 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
764 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
765 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
766 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
767 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
768 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
769 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
771 (* operatore rotazione destra *)
773 λe:exadecim.match e with
774 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
775 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
776 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
777 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
779 (* operatore rotazione destra n-volte *)
780 let rec ror_ex_n (e:exadecim) (n:nat) on n ≝
783 | S n' ⇒ ror_ex_n (ror_ex e) n' ].
785 (* operatore rotazione sinistra con carry *)
787 λe:exadecim.λc:bool.match c with
788 [ true ⇒ match e with
789 [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
790 | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
791 | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
792 | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
793 | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
794 | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
795 | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
796 | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
797 | false ⇒ match e with
798 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
799 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
800 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
801 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
802 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
803 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
804 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
805 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
808 (* operatore shift sinistro *)
810 λe:exadecim.match e with
811 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
812 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
813 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
814 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
815 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
816 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
817 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
818 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
820 (* operatore rotazione sinistra *)
822 λe:exadecim.match e with
823 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
824 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
825 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
826 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
828 (* operatore rotazione sinistra n-volte *)
829 let rec rol_ex_n (e:exadecim) (n:nat) on n ≝
832 | S n' ⇒ rol_ex_n (rol_ex e) n' ].
834 (* operatore not/complemento a 1 *)
836 λe:exadecim.match e with
837 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
838 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
839 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
840 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
842 (* operatore somma con carry *)
844 λe1,e2:exadecim.λc:bool.
850 [ x0 ⇒ pair exadecim bool x1 false
851 | x1 ⇒ pair exadecim bool x2 false
852 | x2 ⇒ pair exadecim bool x3 false
853 | x3 ⇒ pair exadecim bool x4 false
854 | x4 ⇒ pair exadecim bool x5 false
855 | x5 ⇒ pair exadecim bool x6 false
856 | x6 ⇒ pair exadecim bool x7 false
857 | x7 ⇒ pair exadecim bool x8 false
858 | x8 ⇒ pair exadecim bool x9 false
859 | x9 ⇒ pair exadecim bool xA false
860 | xA ⇒ pair exadecim bool xB false
861 | xB ⇒ pair exadecim bool xC false
862 | xC ⇒ pair exadecim bool xD false
863 | xD ⇒ pair exadecim bool xE false
864 | xE ⇒ pair exadecim bool xF false
865 | xF ⇒ pair exadecim bool x0 true ]
868 [ x0 ⇒ pair exadecim bool x2 false
869 | x1 ⇒ pair exadecim bool x3 false
870 | x2 ⇒ pair exadecim bool x4 false
871 | x3 ⇒ pair exadecim bool x5 false
872 | x4 ⇒ pair exadecim bool x6 false
873 | x5 ⇒ pair exadecim bool x7 false
874 | x6 ⇒ pair exadecim bool x8 false
875 | x7 ⇒ pair exadecim bool x9 false
876 | x8 ⇒ pair exadecim bool xA false
877 | x9 ⇒ pair exadecim bool xB false
878 | xA ⇒ pair exadecim bool xC false
879 | xB ⇒ pair exadecim bool xD false
880 | xC ⇒ pair exadecim bool xE false
881 | xD ⇒ pair exadecim bool xF false
882 | xE ⇒ pair exadecim bool x0 true
883 | xF ⇒ pair exadecim bool x1 true ]
886 [ x0 ⇒ pair exadecim bool x3 false
887 | x1 ⇒ pair exadecim bool x4 false
888 | x2 ⇒ pair exadecim bool x5 false
889 | x3 ⇒ pair exadecim bool x6 false
890 | x4 ⇒ pair exadecim bool x7 false
891 | x5 ⇒ pair exadecim bool x8 false
892 | x6 ⇒ pair exadecim bool x9 false
893 | x7 ⇒ pair exadecim bool xA false
894 | x8 ⇒ pair exadecim bool xB false
895 | x9 ⇒ pair exadecim bool xC false
896 | xA ⇒ pair exadecim bool xD false
897 | xB ⇒ pair exadecim bool xE false
898 | xC ⇒ pair exadecim bool xF false
899 | xD ⇒ pair exadecim bool x0 true
900 | xE ⇒ pair exadecim bool x1 true
901 | xF ⇒ pair exadecim bool x2 true ]
904 [ x0 ⇒ pair exadecim bool x4 false
905 | x1 ⇒ pair exadecim bool x5 false
906 | x2 ⇒ pair exadecim bool x6 false
907 | x3 ⇒ pair exadecim bool x7 false
908 | x4 ⇒ pair exadecim bool x8 false
909 | x5 ⇒ pair exadecim bool x9 false
910 | x6 ⇒ pair exadecim bool xA false
911 | x7 ⇒ pair exadecim bool xB false
912 | x8 ⇒ pair exadecim bool xC false
913 | x9 ⇒ pair exadecim bool xD false
914 | xA ⇒ pair exadecim bool xE false
915 | xB ⇒ pair exadecim bool xF false
916 | xC ⇒ pair exadecim bool x0 true
917 | xD ⇒ pair exadecim bool x1 true
918 | xE ⇒ pair exadecim bool x2 true
919 | xF ⇒ pair exadecim bool x3 true ]
922 [ x0 ⇒ pair exadecim bool x5 false
923 | x1 ⇒ pair exadecim bool x6 false
924 | x2 ⇒ pair exadecim bool x7 false
925 | x3 ⇒ pair exadecim bool x8 false
926 | x4 ⇒ pair exadecim bool x9 false
927 | x5 ⇒ pair exadecim bool xA false
928 | x6 ⇒ pair exadecim bool xB false
929 | x7 ⇒ pair exadecim bool xC false
930 | x8 ⇒ pair exadecim bool xD false
931 | x9 ⇒ pair exadecim bool xE false
932 | xA ⇒ pair exadecim bool xF false
933 | xB ⇒ pair exadecim bool x0 true
934 | xC ⇒ pair exadecim bool x1 true
935 | xD ⇒ pair exadecim bool x2 true
936 | xE ⇒ pair exadecim bool x3 true
937 | xF ⇒ pair exadecim bool x4 true ]
940 [ x0 ⇒ pair exadecim bool x6 false
941 | x1 ⇒ pair exadecim bool x7 false
942 | x2 ⇒ pair exadecim bool x8 false
943 | x3 ⇒ pair exadecim bool x9 false
944 | x4 ⇒ pair exadecim bool xA false
945 | x5 ⇒ pair exadecim bool xB false
946 | x6 ⇒ pair exadecim bool xC false
947 | x7 ⇒ pair exadecim bool xD false
948 | x8 ⇒ pair exadecim bool xE false
949 | x9 ⇒ pair exadecim bool xF false
950 | xA ⇒ pair exadecim bool x0 true
951 | xB ⇒ pair exadecim bool x1 true
952 | xC ⇒ pair exadecim bool x2 true
953 | xD ⇒ pair exadecim bool x3 true
954 | xE ⇒ pair exadecim bool x4 true
955 | xF ⇒ pair exadecim bool x5 true ]
958 [ x0 ⇒ pair exadecim bool x7 false
959 | x1 ⇒ pair exadecim bool x8 false
960 | x2 ⇒ pair exadecim bool x9 false
961 | x3 ⇒ pair exadecim bool xA false
962 | x4 ⇒ pair exadecim bool xB false
963 | x5 ⇒ pair exadecim bool xC false
964 | x6 ⇒ pair exadecim bool xD false
965 | x7 ⇒ pair exadecim bool xE false
966 | x8 ⇒ pair exadecim bool xF false
967 | x9 ⇒ pair exadecim bool x0 true
968 | xA ⇒ pair exadecim bool x1 true
969 | xB ⇒ pair exadecim bool x2 true
970 | xC ⇒ pair exadecim bool x3 true
971 | xD ⇒ pair exadecim bool x4 true
972 | xE ⇒ pair exadecim bool x5 true
973 | xF ⇒ pair exadecim bool x6 true ]
976 [ x0 ⇒ pair exadecim bool x8 false
977 | x1 ⇒ pair exadecim bool x9 false
978 | x2 ⇒ pair exadecim bool xA false
979 | x3 ⇒ pair exadecim bool xB false
980 | x4 ⇒ pair exadecim bool xC false
981 | x5 ⇒ pair exadecim bool xD false
982 | x6 ⇒ pair exadecim bool xE false
983 | x7 ⇒ pair exadecim bool xF false
984 | x8 ⇒ pair exadecim bool x0 true
985 | x9 ⇒ pair exadecim bool x1 true
986 | xA ⇒ pair exadecim bool x2 true
987 | xB ⇒ pair exadecim bool x3 true
988 | xC ⇒ pair exadecim bool x4 true
989 | xD ⇒ pair exadecim bool x5 true
990 | xE ⇒ pair exadecim bool x6 true
991 | xF ⇒ pair exadecim bool x7 true ]
994 [ x0 ⇒ pair exadecim bool x9 false
995 | x1 ⇒ pair exadecim bool xA false
996 | x2 ⇒ pair exadecim bool xB false
997 | x3 ⇒ pair exadecim bool xC false
998 | x4 ⇒ pair exadecim bool xD false
999 | x5 ⇒ pair exadecim bool xE false
1000 | x6 ⇒ pair exadecim bool xF false
1001 | x7 ⇒ pair exadecim bool x0 true
1002 | x8 ⇒ pair exadecim bool x1 true
1003 | x9 ⇒ pair exadecim bool x2 true
1004 | xA ⇒ pair exadecim bool x3 true
1005 | xB ⇒ pair exadecim bool x4 true
1006 | xC ⇒ pair exadecim bool x5 true
1007 | xD ⇒ pair exadecim bool x6 true
1008 | xE ⇒ pair exadecim bool x7 true
1009 | xF ⇒ pair exadecim bool x8 true ]
1012 [ x0 ⇒ pair exadecim bool xA false
1013 | x1 ⇒ pair exadecim bool xB false
1014 | x2 ⇒ pair exadecim bool xC false
1015 | x3 ⇒ pair exadecim bool xD false
1016 | x4 ⇒ pair exadecim bool xE false
1017 | x5 ⇒ pair exadecim bool xF false
1018 | x6 ⇒ pair exadecim bool x0 true
1019 | x7 ⇒ pair exadecim bool x1 true
1020 | x8 ⇒ pair exadecim bool x2 true
1021 | x9 ⇒ pair exadecim bool x3 true
1022 | xA ⇒ pair exadecim bool x4 true
1023 | xB ⇒ pair exadecim bool x5 true
1024 | xC ⇒ pair exadecim bool x6 true
1025 | xD ⇒ pair exadecim bool x7 true
1026 | xE ⇒ pair exadecim bool x8 true
1027 | xF ⇒ pair exadecim bool x9 true ]
1030 [ x0 ⇒ pair exadecim bool xB false
1031 | x1 ⇒ pair exadecim bool xC false
1032 | x2 ⇒ pair exadecim bool xD false
1033 | x3 ⇒ pair exadecim bool xE false
1034 | x4 ⇒ pair exadecim bool xF false
1035 | x5 ⇒ pair exadecim bool x0 true
1036 | x6 ⇒ pair exadecim bool x1 true
1037 | x7 ⇒ pair exadecim bool x2 true
1038 | x8 ⇒ pair exadecim bool x3 true
1039 | x9 ⇒ pair exadecim bool x4 true
1040 | xA ⇒ pair exadecim bool x5 true
1041 | xB ⇒ pair exadecim bool x6 true
1042 | xC ⇒ pair exadecim bool x7 true
1043 | xD ⇒ pair exadecim bool x8 true
1044 | xE ⇒ pair exadecim bool x9 true
1045 | xF ⇒ pair exadecim bool xA true ]
1048 [ x0 ⇒ pair exadecim bool xC false
1049 | x1 ⇒ pair exadecim bool xD false
1050 | x2 ⇒ pair exadecim bool xE false
1051 | x3 ⇒ pair exadecim bool xF false
1052 | x4 ⇒ pair exadecim bool x0 true
1053 | x5 ⇒ pair exadecim bool x1 true
1054 | x6 ⇒ pair exadecim bool x2 true
1055 | x7 ⇒ pair exadecim bool x3 true
1056 | x8 ⇒ pair exadecim bool x4 true
1057 | x9 ⇒ pair exadecim bool x5 true
1058 | xA ⇒ pair exadecim bool x6 true
1059 | xB ⇒ pair exadecim bool x7 true
1060 | xC ⇒ pair exadecim bool x8 true
1061 | xD ⇒ pair exadecim bool x9 true
1062 | xE ⇒ pair exadecim bool xA true
1063 | xF ⇒ pair exadecim bool xB true ]
1066 [ x0 ⇒ pair exadecim bool xD false
1067 | x1 ⇒ pair exadecim bool xE false
1068 | x2 ⇒ pair exadecim bool xF false
1069 | x3 ⇒ pair exadecim bool x0 true
1070 | x4 ⇒ pair exadecim bool x1 true
1071 | x5 ⇒ pair exadecim bool x2 true
1072 | x6 ⇒ pair exadecim bool x3 true
1073 | x7 ⇒ pair exadecim bool x4 true
1074 | x8 ⇒ pair exadecim bool x5 true
1075 | x9 ⇒ pair exadecim bool x6 true
1076 | xA ⇒ pair exadecim bool x7 true
1077 | xB ⇒ pair exadecim bool x8 true
1078 | xC ⇒ pair exadecim bool x9 true
1079 | xD ⇒ pair exadecim bool xA true
1080 | xE ⇒ pair exadecim bool xB true
1081 | xF ⇒ pair exadecim bool xC true ]
1084 [ x0 ⇒ pair exadecim bool xE false
1085 | x1 ⇒ pair exadecim bool xF false
1086 | x2 ⇒ pair exadecim bool x0 true
1087 | x3 ⇒ pair exadecim bool x1 true
1088 | x4 ⇒ pair exadecim bool x2 true
1089 | x5 ⇒ pair exadecim bool x3 true
1090 | x6 ⇒ pair exadecim bool x4 true
1091 | x7 ⇒ pair exadecim bool x5 true
1092 | x8 ⇒ pair exadecim bool x6 true
1093 | x9 ⇒ pair exadecim bool x7 true
1094 | xA ⇒ pair exadecim bool x8 true
1095 | xB ⇒ pair exadecim bool x9 true
1096 | xC ⇒ pair exadecim bool xA true
1097 | xD ⇒ pair exadecim bool xB true
1098 | xE ⇒ pair exadecim bool xC true
1099 | xF ⇒ pair exadecim bool xD true ]
1102 [ x0 ⇒ pair exadecim bool xF false
1103 | x1 ⇒ pair exadecim bool x0 true
1104 | x2 ⇒ pair exadecim bool x1 true
1105 | x3 ⇒ pair exadecim bool x2 true
1106 | x4 ⇒ pair exadecim bool x3 true
1107 | x5 ⇒ pair exadecim bool x4 true
1108 | x6 ⇒ pair exadecim bool x5 true
1109 | x7 ⇒ pair exadecim bool x6 true
1110 | x8 ⇒ pair exadecim bool x7 true
1111 | x9 ⇒ pair exadecim bool x8 true
1112 | xA ⇒ pair exadecim bool x9 true
1113 | xB ⇒ pair exadecim bool xA true
1114 | xC ⇒ pair exadecim bool xB true
1115 | xD ⇒ pair exadecim bool xC true
1116 | xE ⇒ pair exadecim bool xD true
1117 | xF ⇒ pair exadecim bool xE true ]
1120 [ x0 ⇒ pair exadecim bool x0 true
1121 | x1 ⇒ pair exadecim bool x1 true
1122 | x2 ⇒ pair exadecim bool x2 true
1123 | x3 ⇒ pair exadecim bool x3 true
1124 | x4 ⇒ pair exadecim bool x4 true
1125 | x5 ⇒ pair exadecim bool x5 true
1126 | x6 ⇒ pair exadecim bool x6 true
1127 | x7 ⇒ pair exadecim bool x7 true
1128 | x8 ⇒ pair exadecim bool x8 true
1129 | x9 ⇒ pair exadecim bool x9 true
1130 | xA ⇒ pair exadecim bool xA true
1131 | xB ⇒ pair exadecim bool xB true
1132 | xC ⇒ pair exadecim bool xC true
1133 | xD ⇒ pair exadecim bool xD true
1134 | xE ⇒ pair exadecim bool xE true
1135 | xF ⇒ pair exadecim bool xF true ]
1141 [ x0 ⇒ pair exadecim bool x0 false
1142 | x1 ⇒ pair exadecim bool x1 false
1143 | x2 ⇒ pair exadecim bool x2 false
1144 | x3 ⇒ pair exadecim bool x3 false
1145 | x4 ⇒ pair exadecim bool x4 false
1146 | x5 ⇒ pair exadecim bool x5 false
1147 | x6 ⇒ pair exadecim bool x6 false
1148 | x7 ⇒ pair exadecim bool x7 false
1149 | x8 ⇒ pair exadecim bool x8 false
1150 | x9 ⇒ pair exadecim bool x9 false
1151 | xA ⇒ pair exadecim bool xA false
1152 | xB ⇒ pair exadecim bool xB false
1153 | xC ⇒ pair exadecim bool xC false
1154 | xD ⇒ pair exadecim bool xD false
1155 | xE ⇒ pair exadecim bool xE false
1156 | xF ⇒ pair exadecim bool xF false ]
1159 [ x0 ⇒ pair exadecim bool x1 false
1160 | x1 ⇒ pair exadecim bool x2 false
1161 | x2 ⇒ pair exadecim bool x3 false
1162 | x3 ⇒ pair exadecim bool x4 false
1163 | x4 ⇒ pair exadecim bool x5 false
1164 | x5 ⇒ pair exadecim bool x6 false
1165 | x6 ⇒ pair exadecim bool x7 false
1166 | x7 ⇒ pair exadecim bool x8 false
1167 | x8 ⇒ pair exadecim bool x9 false
1168 | x9 ⇒ pair exadecim bool xA false
1169 | xA ⇒ pair exadecim bool xB false
1170 | xB ⇒ pair exadecim bool xC false
1171 | xC ⇒ pair exadecim bool xD false
1172 | xD ⇒ pair exadecim bool xE false
1173 | xE ⇒ pair exadecim bool xF false
1174 | xF ⇒ pair exadecim bool x0 true ]
1177 [ x0 ⇒ pair exadecim bool x2 false
1178 | x1 ⇒ pair exadecim bool x3 false
1179 | x2 ⇒ pair exadecim bool x4 false
1180 | x3 ⇒ pair exadecim bool x5 false
1181 | x4 ⇒ pair exadecim bool x6 false
1182 | x5 ⇒ pair exadecim bool x7 false
1183 | x6 ⇒ pair exadecim bool x8 false
1184 | x7 ⇒ pair exadecim bool x9 false
1185 | x8 ⇒ pair exadecim bool xA false
1186 | x9 ⇒ pair exadecim bool xB false
1187 | xA ⇒ pair exadecim bool xC false
1188 | xB ⇒ pair exadecim bool xD false
1189 | xC ⇒ pair exadecim bool xE false
1190 | xD ⇒ pair exadecim bool xF false
1191 | xE ⇒ pair exadecim bool x0 true
1192 | xF ⇒ pair exadecim bool x1 true ]
1195 [ x0 ⇒ pair exadecim bool x3 false
1196 | x1 ⇒ pair exadecim bool x4 false
1197 | x2 ⇒ pair exadecim bool x5 false
1198 | x3 ⇒ pair exadecim bool x6 false
1199 | x4 ⇒ pair exadecim bool x7 false
1200 | x5 ⇒ pair exadecim bool x8 false
1201 | x6 ⇒ pair exadecim bool x9 false
1202 | x7 ⇒ pair exadecim bool xA false
1203 | x8 ⇒ pair exadecim bool xB false
1204 | x9 ⇒ pair exadecim bool xC false
1205 | xA ⇒ pair exadecim bool xD false
1206 | xB ⇒ pair exadecim bool xE false
1207 | xC ⇒ pair exadecim bool xF false
1208 | xD ⇒ pair exadecim bool x0 true
1209 | xE ⇒ pair exadecim bool x1 true
1210 | xF ⇒ pair exadecim bool x2 true ]
1213 [ x0 ⇒ pair exadecim bool x4 false
1214 | x1 ⇒ pair exadecim bool x5 false
1215 | x2 ⇒ pair exadecim bool x6 false
1216 | x3 ⇒ pair exadecim bool x7 false
1217 | x4 ⇒ pair exadecim bool x8 false
1218 | x5 ⇒ pair exadecim bool x9 false
1219 | x6 ⇒ pair exadecim bool xA false
1220 | x7 ⇒ pair exadecim bool xB false
1221 | x8 ⇒ pair exadecim bool xC false
1222 | x9 ⇒ pair exadecim bool xD false
1223 | xA ⇒ pair exadecim bool xE false
1224 | xB ⇒ pair exadecim bool xF false
1225 | xC ⇒ pair exadecim bool x0 true
1226 | xD ⇒ pair exadecim bool x1 true
1227 | xE ⇒ pair exadecim bool x2 true
1228 | xF ⇒ pair exadecim bool x3 true ]
1231 [ x0 ⇒ pair exadecim bool x5 false
1232 | x1 ⇒ pair exadecim bool x6 false
1233 | x2 ⇒ pair exadecim bool x7 false
1234 | x3 ⇒ pair exadecim bool x8 false
1235 | x4 ⇒ pair exadecim bool x9 false
1236 | x5 ⇒ pair exadecim bool xA false
1237 | x6 ⇒ pair exadecim bool xB false
1238 | x7 ⇒ pair exadecim bool xC false
1239 | x8 ⇒ pair exadecim bool xD false
1240 | x9 ⇒ pair exadecim bool xE false
1241 | xA ⇒ pair exadecim bool xF false
1242 | xB ⇒ pair exadecim bool x0 true
1243 | xC ⇒ pair exadecim bool x1 true
1244 | xD ⇒ pair exadecim bool x2 true
1245 | xE ⇒ pair exadecim bool x3 true
1246 | xF ⇒ pair exadecim bool x4 true ]
1249 [ x0 ⇒ pair exadecim bool x6 false
1250 | x1 ⇒ pair exadecim bool x7 false
1251 | x2 ⇒ pair exadecim bool x8 false
1252 | x3 ⇒ pair exadecim bool x9 false
1253 | x4 ⇒ pair exadecim bool xA false
1254 | x5 ⇒ pair exadecim bool xB false
1255 | x6 ⇒ pair exadecim bool xC false
1256 | x7 ⇒ pair exadecim bool xD false
1257 | x8 ⇒ pair exadecim bool xE false
1258 | x9 ⇒ pair exadecim bool xF false
1259 | xA ⇒ pair exadecim bool x0 true
1260 | xB ⇒ pair exadecim bool x1 true
1261 | xC ⇒ pair exadecim bool x2 true
1262 | xD ⇒ pair exadecim bool x3 true
1263 | xE ⇒ pair exadecim bool x4 true
1264 | xF ⇒ pair exadecim bool x5 true ]
1267 [ x0 ⇒ pair exadecim bool x7 false
1268 | x1 ⇒ pair exadecim bool x8 false
1269 | x2 ⇒ pair exadecim bool x9 false
1270 | x3 ⇒ pair exadecim bool xA false
1271 | x4 ⇒ pair exadecim bool xB false
1272 | x5 ⇒ pair exadecim bool xC false
1273 | x6 ⇒ pair exadecim bool xD false
1274 | x7 ⇒ pair exadecim bool xE false
1275 | x8 ⇒ pair exadecim bool xF false
1276 | x9 ⇒ pair exadecim bool x0 true
1277 | xA ⇒ pair exadecim bool x1 true
1278 | xB ⇒ pair exadecim bool x2 true
1279 | xC ⇒ pair exadecim bool x3 true
1280 | xD ⇒ pair exadecim bool x4 true
1281 | xE ⇒ pair exadecim bool x5 true
1282 | xF ⇒ pair exadecim bool x6 true ]
1285 [ x0 ⇒ pair exadecim bool x8 false
1286 | x1 ⇒ pair exadecim bool x9 false
1287 | x2 ⇒ pair exadecim bool xA false
1288 | x3 ⇒ pair exadecim bool xB false
1289 | x4 ⇒ pair exadecim bool xC false
1290 | x5 ⇒ pair exadecim bool xD false
1291 | x6 ⇒ pair exadecim bool xE false
1292 | x7 ⇒ pair exadecim bool xF false
1293 | x8 ⇒ pair exadecim bool x0 true
1294 | x9 ⇒ pair exadecim bool x1 true
1295 | xA ⇒ pair exadecim bool x2 true
1296 | xB ⇒ pair exadecim bool x3 true
1297 | xC ⇒ pair exadecim bool x4 true
1298 | xD ⇒ pair exadecim bool x5 true
1299 | xE ⇒ pair exadecim bool x6 true
1300 | xF ⇒ pair exadecim bool x7 true ]
1303 [ x0 ⇒ pair exadecim bool x9 false
1304 | x1 ⇒ pair exadecim bool xA false
1305 | x2 ⇒ pair exadecim bool xB false
1306 | x3 ⇒ pair exadecim bool xC false
1307 | x4 ⇒ pair exadecim bool xD false
1308 | x5 ⇒ pair exadecim bool xE false
1309 | x6 ⇒ pair exadecim bool xF false
1310 | x7 ⇒ pair exadecim bool x0 true
1311 | x8 ⇒ pair exadecim bool x1 true
1312 | x9 ⇒ pair exadecim bool x2 true
1313 | xA ⇒ pair exadecim bool x3 true
1314 | xB ⇒ pair exadecim bool x4 true
1315 | xC ⇒ pair exadecim bool x5 true
1316 | xD ⇒ pair exadecim bool x6 true
1317 | xE ⇒ pair exadecim bool x7 true
1318 | xF ⇒ pair exadecim bool x8 true ]
1321 [ x0 ⇒ pair exadecim bool xA false
1322 | x1 ⇒ pair exadecim bool xB false
1323 | x2 ⇒ pair exadecim bool xC false
1324 | x3 ⇒ pair exadecim bool xD false
1325 | x4 ⇒ pair exadecim bool xE false
1326 | x5 ⇒ pair exadecim bool xF false
1327 | x6 ⇒ pair exadecim bool x0 true
1328 | x7 ⇒ pair exadecim bool x1 true
1329 | x8 ⇒ pair exadecim bool x2 true
1330 | x9 ⇒ pair exadecim bool x3 true
1331 | xA ⇒ pair exadecim bool x4 true
1332 | xB ⇒ pair exadecim bool x5 true
1333 | xC ⇒ pair exadecim bool x6 true
1334 | xD ⇒ pair exadecim bool x7 true
1335 | xE ⇒ pair exadecim bool x8 true
1336 | xF ⇒ pair exadecim bool x9 true ]
1339 [ x0 ⇒ pair exadecim bool xB false
1340 | x1 ⇒ pair exadecim bool xC false
1341 | x2 ⇒ pair exadecim bool xD false
1342 | x3 ⇒ pair exadecim bool xE false
1343 | x4 ⇒ pair exadecim bool xF false
1344 | x5 ⇒ pair exadecim bool x0 true
1345 | x6 ⇒ pair exadecim bool x1 true
1346 | x7 ⇒ pair exadecim bool x2 true
1347 | x8 ⇒ pair exadecim bool x3 true
1348 | x9 ⇒ pair exadecim bool x4 true
1349 | xA ⇒ pair exadecim bool x5 true
1350 | xB ⇒ pair exadecim bool x6 true
1351 | xC ⇒ pair exadecim bool x7 true
1352 | xD ⇒ pair exadecim bool x8 true
1353 | xE ⇒ pair exadecim bool x9 true
1354 | xF ⇒ pair exadecim bool xA true ]
1357 [ x0 ⇒ pair exadecim bool xC false
1358 | x1 ⇒ pair exadecim bool xD false
1359 | x2 ⇒ pair exadecim bool xE false
1360 | x3 ⇒ pair exadecim bool xF false
1361 | x4 ⇒ pair exadecim bool x0 true
1362 | x5 ⇒ pair exadecim bool x1 true
1363 | x6 ⇒ pair exadecim bool x2 true
1364 | x7 ⇒ pair exadecim bool x3 true
1365 | x8 ⇒ pair exadecim bool x4 true
1366 | x9 ⇒ pair exadecim bool x5 true
1367 | xA ⇒ pair exadecim bool x6 true
1368 | xB ⇒ pair exadecim bool x7 true
1369 | xC ⇒ pair exadecim bool x8 true
1370 | xD ⇒ pair exadecim bool x9 true
1371 | xE ⇒ pair exadecim bool xA true
1372 | xF ⇒ pair exadecim bool xB true ]
1375 [ x0 ⇒ pair exadecim bool xD false
1376 | x1 ⇒ pair exadecim bool xE false
1377 | x2 ⇒ pair exadecim bool xF false
1378 | x3 ⇒ pair exadecim bool x0 true
1379 | x4 ⇒ pair exadecim bool x1 true
1380 | x5 ⇒ pair exadecim bool x2 true
1381 | x6 ⇒ pair exadecim bool x3 true
1382 | x7 ⇒ pair exadecim bool x4 true
1383 | x8 ⇒ pair exadecim bool x5 true
1384 | x9 ⇒ pair exadecim bool x6 true
1385 | xA ⇒ pair exadecim bool x7 true
1386 | xB ⇒ pair exadecim bool x8 true
1387 | xC ⇒ pair exadecim bool x9 true
1388 | xD ⇒ pair exadecim bool xA true
1389 | xE ⇒ pair exadecim bool xB true
1390 | xF ⇒ pair exadecim bool xC true ]
1393 [ x0 ⇒ pair exadecim bool xE false
1394 | x1 ⇒ pair exadecim bool xF false
1395 | x2 ⇒ pair exadecim bool x0 true
1396 | x3 ⇒ pair exadecim bool x1 true
1397 | x4 ⇒ pair exadecim bool x2 true
1398 | x5 ⇒ pair exadecim bool x3 true
1399 | x6 ⇒ pair exadecim bool x4 true
1400 | x7 ⇒ pair exadecim bool x5 true
1401 | x8 ⇒ pair exadecim bool x6 true
1402 | x9 ⇒ pair exadecim bool x7 true
1403 | xA ⇒ pair exadecim bool x8 true
1404 | xB ⇒ pair exadecim bool x9 true
1405 | xC ⇒ pair exadecim bool xA true
1406 | xD ⇒ pair exadecim bool xB true
1407 | xE ⇒ pair exadecim bool xC true
1408 | xF ⇒ pair exadecim bool xD true ]
1411 [ x0 ⇒ pair exadecim bool xF false
1412 | x1 ⇒ pair exadecim bool x0 true
1413 | x2 ⇒ pair exadecim bool x1 true
1414 | x3 ⇒ pair exadecim bool x2 true
1415 | x4 ⇒ pair exadecim bool x3 true
1416 | x5 ⇒ pair exadecim bool x4 true
1417 | x6 ⇒ pair exadecim bool x5 true
1418 | x7 ⇒ pair exadecim bool x6 true
1419 | x8 ⇒ pair exadecim bool x7 true
1420 | x9 ⇒ pair exadecim bool x8 true
1421 | xA ⇒ pair exadecim bool x9 true
1422 | xB ⇒ pair exadecim bool xA true
1423 | xC ⇒ pair exadecim bool xB true
1424 | xD ⇒ pair exadecim bool xC true
1425 | xE ⇒ pair exadecim bool xD true
1426 | xF ⇒ pair exadecim bool xE true ]
1430 (* operatore somma senza carry *)
1431 definition plus_exnc ≝
1432 λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
1434 (* operatore carry della somma *)
1435 definition plus_exc ≝
1436 λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
1438 (* operatore Most Significant Bit *)
1440 λe:exadecim.match e with
1441 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1442 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1443 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
1444 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
1446 (* esadecimali → naturali *)
1447 definition nat_of_exadecim ≝
1450 [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2 | x3 ⇒ 3 | x4 ⇒ 4 | x5 ⇒ 5 | x6 ⇒ 6 | x7 ⇒ 7
1451 | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
1453 coercion nat_of_exadecim.
1455 (* naturali → esadecimali *)
1456 let rec exadecim_of_nat n ≝
1457 match n with [ O ⇒ x0 | S n ⇒
1458 match n with [ O ⇒ x1 | S n ⇒
1459 match n with [ O ⇒ x2 | S n ⇒
1460 match n with [ O ⇒ x3 | S n ⇒
1461 match n with [ O ⇒ x4 | S n ⇒
1462 match n with [ O ⇒ x5 | S n ⇒
1463 match n with [ O ⇒ x6 | S n ⇒
1464 match n with [ O ⇒ x7 | S n ⇒
1465 match n with [ O ⇒ x8 | S n ⇒
1466 match n with [ O ⇒ x9 | S n ⇒
1467 match n with [ O ⇒ xA | S n ⇒
1468 match n with [ O ⇒ xB | S n ⇒
1469 match n with [ O ⇒ xC | S n ⇒
1470 match n with [ O ⇒ xD | S n ⇒
1471 match n with [ O ⇒ xE | S n ⇒
1472 match n with [ O ⇒ xF | S n ⇒ exadecim_of_nat n ]]]]]]]]]]]]]]]].
1474 (* operatore predecessore *)
1475 definition pred_ex ≝
1478 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1479 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1481 (* operatore successore *)
1482 definition succ_ex ≝
1485 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1486 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1488 (* operatore neg/complemento a 2 *)
1489 definition compl_ex ≝
1490 λe:exadecim.match e with
1491 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1492 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1493 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1494 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1496 (* iteratore sugli esadecimali *)
1497 definition forall_exadecim ≝ λP.
1498 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1499 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
1501 (* ********************** *)
1502 (* TEOREMI/LEMMMI/ASSIOMI *)
1503 (* ********************** *)
1505 (* ESPERIMENTO UTILIZZO DELL'ITERATORE *)
1508 lemma forall_exadecim_eqProp_left_aux :
1509 ∀P.(∀e:exadecim.P e = true) →
1510 ((P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1511 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF) = true).
1513 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1514 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
1515 elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
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; ]
1524 lemma forall_exadecim_eqProp_left :
1525 ∀P.(∀e:exadecim. P e = true) → (forall_exadecim (λe.P e) = true).
1528 [ simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
1529 simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
1533 lemma forall_exadecim_eqProp_right_aux :
1534 ∀P.((P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1535 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF) = true) →
1536 (∀e:exadecim.P e = true).
1540 lemma forall_exadecim_eqProp_right :
1541 ∀P.(forall_exadecim (λe.P e) = true) → (∀e:exadecim.P e = true).
1544 [ simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
1545 simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
1549 lemma lt_nat_of_exadecim_16_forall: ∀e.ltb (nat_of_exadecim e) 16 = true.
1550 apply forall_exadecim_eqProp_right;
1555 (* FINE DELL'ESPERIMENTO *)
1557 lemma lt_nat_of_exadecim_16: ∀e.nat_of_exadecim e < 16.
1564 lemma exadecim_of_nat_mod:
1565 ∀n.exadecim_of_nat n = exadecim_of_nat (n \mod 16).
1567 apply (nat_elim1 n); intro;
1568 cases m; [ intro; reflexivity | ];
1569 cases n1; [ intro; reflexivity | ];
1570 cases n2; [ intro; reflexivity | ];
1571 cases n3; [ intro; reflexivity | ];
1572 cases n4; [ intro; reflexivity | ];
1573 cases n5; [ intro; reflexivity | ];
1574 cases n6; [ intro; reflexivity | ];
1575 cases n7; [ intro; reflexivity | ];
1576 cases n8; [ intro; reflexivity | ];
1577 cases n9; [ intro; reflexivity | ];
1578 cases n10; [ intro; reflexivity | ];
1579 cases n11; [ intro; reflexivity | ];
1580 cases n12; [ intro; reflexivity | ];
1581 cases n13; [ intro; reflexivity | ];
1582 cases n14; [ intro; reflexivity | ];
1583 cases n15; [ intro; reflexivity | ];
1585 change in ⊢ (? ? % ?) with (exadecim_of_nat n16);
1586 change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
1588 change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
1597 lemma nat_of_exadecim_exadecim_of_nat:
1598 ∀n. nat_of_exadecim (exadecim_of_nat n) = n \mod 16.
1600 rewrite > exadecim_of_nat_mod;
1601 generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
1602 generalize in match (n \mod 16); intro;
1603 cases n1; [ intro; reflexivity | ];
1604 cases n2; [ intro; reflexivity | ];
1605 cases n3; [ intro; reflexivity | ];
1606 cases n4; [ intro; reflexivity | ];
1607 cases n5; [ intro; reflexivity | ];
1608 cases n6; [ intro; reflexivity | ];
1609 cases n7; [ intro; reflexivity | ];
1610 cases n8; [ intro; reflexivity | ];
1611 cases n9; [ intro; reflexivity | ];
1612 cases n10; [ intro; reflexivity | ];
1613 cases n11 [ intro; reflexivity | ];
1614 cases n12; [ intro; reflexivity | ];
1615 cases n13; [ intro; reflexivity | ];
1616 cases n14; [ intro; reflexivity | ];
1617 cases n15; [ intro; reflexivity | ];
1618 cases n16; [ intro; reflexivity | ];
1627 lemma exadecim_of_nat_nat_of_exadecim:
1628 ∀e.exadecim_of_nat (nat_of_exadecim e) = e.
1636 match plus_ex b1 b2 c with
1637 [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
1639 elim b1; (elim b2; (elim c; normalize; reflexivity)).
1642 lemma eq_eqex_S_x0_false:
1643 ∀n. n < 15 → eq_ex x0 (exadecim_of_nat (S n)) = false.
1645 cases n 0; [ intro; simplify; reflexivity | clear n];
1646 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1647 cases n 0; [ intro; simplify; reflexivity | clear n];
1648 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1649 cases n 0; [ intro; simplify; reflexivity | clear n];
1650 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1651 cases n 0; [ intro; simplify; reflexivity | clear n];
1652 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1653 cases n 0; [ intro; simplify; reflexivity | clear n];
1654 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1655 cases n 0; [ intro; simplify; reflexivity | clear n];
1656 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1657 cases n 0; [ intro; simplify; reflexivity | clear n];
1658 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1659 cases n 0; [ intro; simplify; reflexivity | clear n];
1663 [ elim (not_le_Sn_O ? Hcut)
1664 | do 15 (apply le_S_S_to_le);
1669 lemma eqex_true_to_eq: ∀b,b'. eq_ex b b' = true → b=b'.
1675 first [ reflexivity | destruct H ].
1678 lemma eqex_false_to_not_eq: ∀b,b'. eq_ex b b' = false → b ≠ b'.
1691 lemma ok_lt_ex : ∀e1,e2:exadecim.
1692 lt_ex e1 e2 = ltb e1 e2.
1700 lemma ok_le_ex : ∀e1,e2:exadecim.
1701 le_ex e1 e2 = leb e1 e2.
1709 lemma ok_gt_ex : ∀e1,e2:exadecim.
1710 gt_ex e1 e2 = notb (leb e1 e2).
1718 lemma ok_ge_ex : ∀e1,e2:exadecim.
1719 ge_ex e1 e2 = notb (ltb e1 e2).
1727 lemma ok_pred_ex : ∀e:exadecim.
1728 pred_ex e = plus_exnc e xF.
1735 lemma ok_succ_ex : ∀e:exadecim.
1736 succ_ex e = plus_exnc e x1.
1743 lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
1746 (exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
1751 simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
1752 simplify in ⊢ (? ? ? (? ? ? ? %));
1753 simplify in ⊢ (? ? ? (? ? ? % ?));
1754 simplify in ⊢ (? ? % ?);
1758 lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
1761 (exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
1766 simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
1767 simplify in ⊢ (? ? ? (? ? ? % ?));
1768 simplify in ⊢ (? ? ? (? ? ? ? (? %)));
1769 simplify in ⊢ (? ? ? (? ? ? ? %));
1770 simplify in ⊢ (? ? % ?);
1774 lemma ok_shr_ex : ∀e:exadecim.
1777 (exadecim_of_nat (e/2))
1781 simplify in ⊢ (? ? ? (? ? ? % ?));
1782 simplify in ⊢ (? ? ? (? ? ? ? %));
1783 simplify in ⊢ (? ? % ?);
1787 lemma ok_shl_ex : ∀e:exadecim.
1790 (exadecim_of_nat (mod (e*2) 16))
1794 simplify in ⊢ (? ? ? (? ? ? % ?));
1795 simplify in ⊢ (? ? ? (? ? ? ? (? %)));
1796 simplify in ⊢ (? ? ? (? ? ? ? %));
1797 simplify in ⊢ (? ? % ?);
1801 lemma ok_not_ex : ∀e:exadecim.
1802 e + (not_ex e) = 15.
1809 lemma ok_compl_ex : ∀e:exadecim.
1810 e + (compl_ex e) = match gt_ex e x0 with [ true ⇒ 16 | false ⇒ 0 ].
1817 lemma ok_MSB_ex : ∀e:exadecim.
1818 MSB_ex e = notb (ltb e 8).