1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
24 include "num/quatern.ma".
26 include "common/prod.ma".
27 include "common/nat.ma".
33 ninductive exadecim : Type ≝
55 [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
56 | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
57 | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
58 | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
59 | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
60 | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
61 | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
62 | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
63 | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
64 | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
65 | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
66 | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
67 | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
68 | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
69 | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
70 | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
78 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
79 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
80 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
81 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
83 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
84 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
85 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
86 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
88 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
89 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
90 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
91 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
93 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
94 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
95 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
96 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
98 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
99 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
100 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
101 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
103 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
104 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
105 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
106 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
108 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
109 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
110 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
111 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
113 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
114 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
115 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
116 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
118 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
119 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
120 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
121 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
123 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
124 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
125 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
126 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
128 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
129 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
130 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
131 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
133 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
134 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
135 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
136 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
138 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
139 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
140 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
141 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
143 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
144 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
145 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
146 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
148 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
149 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
150 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
151 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
153 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
154 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
155 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
156 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
164 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
165 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
166 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
167 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
169 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
170 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
171 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
172 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
174 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
175 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
176 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
177 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
179 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
180 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
181 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
182 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
184 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
185 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
186 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
187 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
189 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
190 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
191 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
192 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
194 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
195 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
196 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
197 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
199 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
200 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
201 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
202 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
204 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
205 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
206 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
207 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
209 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
210 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
211 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
212 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
214 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
215 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
216 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
217 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
219 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
220 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
221 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
222 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
224 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
225 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
226 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
227 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
229 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
230 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
231 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
232 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
234 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
235 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
236 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
237 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
239 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
240 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
241 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
242 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
250 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
251 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
252 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
253 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
255 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
256 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
257 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
258 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
260 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
261 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
262 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
263 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
265 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
266 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
267 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
268 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
270 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
271 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
272 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
273 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
275 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
276 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
277 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
278 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
280 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
281 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
282 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
283 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
285 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
286 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
287 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
288 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
290 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
291 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
292 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
293 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
295 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
296 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
297 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
298 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
300 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
301 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
302 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
303 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
305 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
306 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
307 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
308 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
310 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
311 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
312 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
313 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
315 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
316 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
317 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
318 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
320 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
321 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
322 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
323 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
325 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
326 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
327 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
328 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
336 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
337 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
338 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
339 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
341 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
342 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
343 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
344 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
346 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
347 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
348 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
349 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
351 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
352 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
353 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
354 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
356 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
357 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
358 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
359 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
361 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
362 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
363 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
364 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
366 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
367 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
368 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
369 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
371 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
372 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
373 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
374 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
376 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
377 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
378 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
379 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
381 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
382 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
383 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
384 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
386 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
387 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
388 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
389 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
391 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
392 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
393 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
394 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
396 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
397 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
398 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
399 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
401 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
402 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
403 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
404 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
406 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
407 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
408 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
409 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
411 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
412 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
413 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
414 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
419 λe1,e2:exadecim.match e1 with
421 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
422 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
423 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
424 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
426 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
427 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
428 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
429 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
431 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
432 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
433 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
434 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
436 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
437 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
438 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
439 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
441 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
442 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
443 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
444 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
446 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
447 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
448 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
449 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
451 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
452 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
453 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
454 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
456 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
457 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
458 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
459 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
461 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
462 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
463 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
464 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
466 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
467 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
468 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
469 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
471 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
472 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
473 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
474 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
476 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
477 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
478 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
479 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
481 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
482 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
483 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
484 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
486 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
487 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
488 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
489 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
491 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
492 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
493 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
494 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
496 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
497 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
498 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
499 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
504 λe1,e2:exadecim.match e1 with
506 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
507 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
508 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
509 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
511 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
512 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
513 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
514 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
516 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
517 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
518 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
519 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
521 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
522 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
523 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
524 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
526 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
527 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
528 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
529 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
531 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
532 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
533 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
534 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
536 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
537 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
538 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
539 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
541 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
542 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
543 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
544 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
546 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
547 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
548 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
549 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
551 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
552 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
553 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
554 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
556 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
557 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
558 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
559 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
561 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
562 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
563 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
564 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
566 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
567 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
568 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
569 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
571 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
572 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
573 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
574 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
576 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
577 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
578 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
579 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
581 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
582 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
583 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
584 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
589 λe1,e2:exadecim.match e1 with
591 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
592 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
593 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
594 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
596 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
597 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
598 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
599 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
601 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
602 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
603 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
604 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
606 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
607 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
608 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
609 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
611 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
612 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
613 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
614 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
616 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
617 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
618 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
619 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
621 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
622 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
623 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
624 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
626 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
627 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
628 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
629 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
631 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
632 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
633 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
634 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
636 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
637 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
638 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
639 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
641 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
642 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
643 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
644 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
646 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
647 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
648 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
649 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
651 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
652 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
653 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
654 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
656 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
657 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
658 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
659 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
661 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
662 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
663 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
664 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
666 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
667 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
668 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
669 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
672 (* operatore rotazione destra con carry *)
674 λe:exadecim.λc:bool.match c with
675 [ true ⇒ match e with
676 [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
677 | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
678 | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
679 | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
680 | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
681 | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
682 | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
683 | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
684 | false ⇒ match e with
685 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
686 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
687 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
688 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
689 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
690 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
691 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
692 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
695 (* operatore shift destro *)
697 λe:exadecim.match e with
698 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
699 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
700 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
701 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
702 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
703 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
704 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
705 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
707 (* operatore rotazione destra *)
709 λe:exadecim.match e with
710 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
711 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
712 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
713 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
715 (* operatore rotazione destra n-volte *)
716 nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
719 | S n' ⇒ ror_ex_n (ror_ex e) n' ].
721 (* operatore rotazione sinistra con carry *)
723 λe:exadecim.λc:bool.match c with
724 [ true ⇒ match e with
725 [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
726 | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
727 | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
728 | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
729 | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
730 | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
731 | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
732 | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
733 | false ⇒ match e with
734 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
735 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
736 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
737 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
738 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
739 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
740 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
741 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
744 (* operatore shift sinistro *)
746 λe:exadecim.match e with
747 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
748 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
749 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
750 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
751 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
752 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
753 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
754 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
756 (* operatore rotazione sinistra *)
758 λe:exadecim.match e with
759 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
760 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
761 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
762 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
764 (* operatore rotazione sinistra n-volte *)
765 nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
768 | S n' ⇒ rol_ex_n (rol_ex e) n' ].
770 (* operatore not/complemento a 1 *)
772 λe:exadecim.match e with
773 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
774 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
775 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
776 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
778 (* operatore somma con data+carry → data+carry *)
779 ndefinition plus_ex_dc_dc ≝
780 λe1,e2:exadecim.λc:bool.
782 [ true ⇒ match e1 with
784 [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
785 | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
786 | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
787 | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
789 [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
790 | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
791 | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
792 | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
794 [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
795 | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
796 | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
797 | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
799 [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
800 | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
801 | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
802 | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
804 [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
805 | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
806 | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
807 | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
809 [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
810 | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
811 | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
812 | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
814 [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
815 | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
816 | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
817 | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
819 [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
820 | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
821 | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
822 | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
824 [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
825 | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
826 | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
827 | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
829 [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
830 | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
831 | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
832 | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
834 [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
835 | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
836 | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
837 | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
839 [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
840 | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
841 | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
842 | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
844 [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
845 | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
846 | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
847 | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
849 [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
850 | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
851 | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
852 | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
854 [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
855 | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
856 | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
857 | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
859 [ x0 ⇒ pair … x0 true | x1 ⇒ pair … x1 true | x2 ⇒ pair … x2 true | x3 ⇒ pair … x3 true
860 | x4 ⇒ pair … x4 true | x5 ⇒ pair … x5 true | x6 ⇒ pair … x6 true | x7 ⇒ pair … x7 true
861 | x8 ⇒ pair … x8 true | x9 ⇒ pair … x9 true | xA ⇒ pair … xA true | xB ⇒ pair … xB true
862 | xC ⇒ pair … xC true | xD ⇒ pair … xD true | xE ⇒ pair … xE true | xF ⇒ pair … xF true ]
864 | false ⇒ match e1 with
866 [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
867 | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
868 | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
869 | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
871 [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
872 | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
873 | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
874 | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
876 [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
877 | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
878 | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
879 | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
881 [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
882 | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
883 | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
884 | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
886 [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
887 | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
888 | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
889 | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
891 [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
892 | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
893 | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
894 | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
896 [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
897 | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
898 | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
899 | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
901 [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
902 | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
903 | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
904 | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
906 [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
907 | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
908 | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
909 | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
911 [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
912 | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
913 | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
914 | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
916 [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
917 | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
918 | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
919 | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
921 [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
922 | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
923 | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
924 | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
926 [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
927 | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
928 | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
929 | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
931 [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
932 | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
933 | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
934 | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
936 [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
937 | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
938 | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
939 | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
941 [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
942 | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
943 | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
944 | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
947 (* operatore somma con data → data+carry *)
948 ndefinition plus_ex_d_dc ≝
952 [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
953 | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
954 | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
955 | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
957 [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
958 | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
959 | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
960 | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
962 [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
963 | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
964 | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
965 | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
967 [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
968 | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
969 | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
970 | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
972 [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
973 | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
974 | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
975 | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
977 [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
978 | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
979 | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
980 | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
982 [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
983 | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
984 | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
985 | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
987 [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
988 | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
989 | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
990 | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
992 [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
993 | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
994 | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
995 | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
997 [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
998 | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
999 | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
1000 | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
1001 | xA ⇒ match e2 with
1002 [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
1003 | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
1004 | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
1005 | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
1006 | xB ⇒ match e2 with
1007 [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
1008 | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
1009 | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
1010 | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
1011 | xC ⇒ match e2 with
1012 [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
1013 | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
1014 | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
1015 | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
1016 | xD ⇒ match e2 with
1017 [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
1018 | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
1019 | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
1020 | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
1021 | xE ⇒ match e2 with
1022 [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
1023 | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
1024 | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
1025 | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
1026 | xF ⇒ match e2 with
1027 [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
1028 | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
1029 | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
1030 | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
1033 (* operatore somma con data+carry → data *)
1034 ndefinition plus_ex_dc_d ≝
1035 λe1,e2:exadecim.λc:bool.
1037 [ true ⇒ match e1 with
1038 [ x0 ⇒ match e2 with
1039 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1040 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1041 | x1 ⇒ match e2 with
1042 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1043 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1044 | x2 ⇒ match e2 with
1045 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1046 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1047 | x3 ⇒ match e2 with
1048 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1049 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1050 | x4 ⇒ match e2 with
1051 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1052 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1053 | x5 ⇒ match e2 with
1054 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1055 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1056 | x6 ⇒ match e2 with
1057 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1058 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1059 | x7 ⇒ match e2 with
1060 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1061 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1062 | x8 ⇒ match e2 with
1063 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1064 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1065 | x9 ⇒ match e2 with
1066 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1067 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1068 | xA ⇒ match e2 with
1069 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1070 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1071 | xB ⇒ match e2 with
1072 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1073 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1074 | xC ⇒ match e2 with
1075 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1076 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1077 | xD ⇒ match e2 with
1078 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1079 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1080 | xE ⇒ match e2 with
1081 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1082 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1083 | xF ⇒ match e2 with
1084 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1085 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1087 | false ⇒ match e1 with
1088 [ x0 ⇒ match e2 with
1089 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1090 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1091 | x1 ⇒ match e2 with
1092 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1093 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1094 | x2 ⇒ match e2 with
1095 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1096 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1097 | x3 ⇒ match e2 with
1098 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1099 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1100 | x4 ⇒ match e2 with
1101 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1102 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1103 | x5 ⇒ match e2 with
1104 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1105 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1106 | x6 ⇒ match e2 with
1107 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1108 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1109 | x7 ⇒ match e2 with
1110 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1111 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1112 | x8 ⇒ match e2 with
1113 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1114 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1115 | x9 ⇒ match e2 with
1116 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1117 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1118 | xA ⇒ match e2 with
1119 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1120 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1121 | xB ⇒ match e2 with
1122 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1123 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1124 | xC ⇒ match e2 with
1125 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1126 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1127 | xD ⇒ match e2 with
1128 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1129 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1130 | xE ⇒ match e2 with
1131 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1132 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1133 | xF ⇒ match e2 with
1134 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1135 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1138 (* operatore somma con data → data *)
1139 ndefinition plus_ex_d_d ≝
1142 [ x0 ⇒ match e2 with
1143 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1144 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1145 | x1 ⇒ match e2 with
1146 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1147 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1148 | x2 ⇒ match e2 with
1149 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1150 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1151 | x3 ⇒ match e2 with
1152 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1153 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1154 | x4 ⇒ match e2 with
1155 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1156 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1157 | x5 ⇒ match e2 with
1158 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1159 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1160 | x6 ⇒ match e2 with
1161 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1162 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1163 | x7 ⇒ match e2 with
1164 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1165 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1166 | x8 ⇒ match e2 with
1167 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1168 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1169 | x9 ⇒ match e2 with
1170 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1171 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1172 | xA ⇒ match e2 with
1173 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1174 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1175 | xB ⇒ match e2 with
1176 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1177 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1178 | xC ⇒ match e2 with
1179 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1180 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1181 | xD ⇒ match e2 with
1182 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1183 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1184 | xE ⇒ match e2 with
1185 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1186 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1187 | xF ⇒ match e2 with
1188 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1189 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1192 (* operatore somma con data+carry → carry *)
1193 ndefinition plus_ex_dc_c ≝
1194 λe1,e2:exadecim.λc:bool.
1196 [ true ⇒ match e1 with
1197 [ x0 ⇒ match e2 with
1198 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1199 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1200 | x1 ⇒ match e2 with
1201 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1202 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1203 | x2 ⇒ match e2 with
1204 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1205 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1206 | x3 ⇒ match e2 with
1207 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1208 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1209 | x4 ⇒ match e2 with
1210 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1211 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1212 | x5 ⇒ match e2 with
1213 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1214 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1215 | x6 ⇒ match e2 with
1216 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1217 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1218 | x7 ⇒ match e2 with
1219 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1220 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1221 | x8 ⇒ match e2 with
1222 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1223 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1224 | x9 ⇒ match e2 with
1225 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1226 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1227 | xA ⇒ match e2 with
1228 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1229 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1230 | xB ⇒ match e2 with
1231 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1232 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1233 | xC ⇒ match e2 with
1234 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1235 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1236 | xD ⇒ match e2 with
1237 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1238 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1239 | xE ⇒ match e2 with
1240 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1241 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1242 | xF ⇒ match e2 with
1243 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1244 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1246 | false ⇒ match e1 with
1247 [ x0 ⇒ match e2 with
1248 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1249 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1250 | x1 ⇒ match e2 with
1251 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1252 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1253 | x2 ⇒ match e2 with
1254 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1255 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1256 | x3 ⇒ match e2 with
1257 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1258 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1259 | x4 ⇒ match e2 with
1260 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1261 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1262 | x5 ⇒ match e2 with
1263 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1264 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1265 | x6 ⇒ match e2 with
1266 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1267 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1268 | x7 ⇒ match e2 with
1269 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1270 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1271 | x8 ⇒ match e2 with
1272 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1273 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1274 | x9 ⇒ match e2 with
1275 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1276 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1277 | xA ⇒ match e2 with
1278 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1279 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1280 | xB ⇒ match e2 with
1281 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1282 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1283 | xC ⇒ match e2 with
1284 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1285 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1286 | xD ⇒ match e2 with
1287 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1288 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1289 | xE ⇒ match e2 with
1290 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1291 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1292 | xF ⇒ match e2 with
1293 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1294 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1297 (* operatore somma con data → carry *)
1298 ndefinition plus_ex_d_c ≝
1301 [ x0 ⇒ match e2 with
1302 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1303 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1304 | x1 ⇒ match e2 with
1305 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1306 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1307 | x2 ⇒ match e2 with
1308 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1309 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1310 | x3 ⇒ match e2 with
1311 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1312 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1313 | x4 ⇒ match e2 with
1314 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1315 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1316 | x5 ⇒ match e2 with
1317 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1318 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1319 | x6 ⇒ match e2 with
1320 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1321 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1322 | x7 ⇒ match e2 with
1323 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1324 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1325 | x8 ⇒ match e2 with
1326 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1327 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1328 | x9 ⇒ match e2 with
1329 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1330 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1331 | xA ⇒ match e2 with
1332 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1333 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1334 | xB ⇒ match e2 with
1335 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1336 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1337 | xC ⇒ match e2 with
1338 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1339 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1340 | xD ⇒ match e2 with
1341 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1342 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1343 | xE ⇒ match e2 with
1344 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1345 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1346 | xF ⇒ match e2 with
1347 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1348 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1351 (* operatore Most Significant Bit *)
1352 ndefinition MSB_ex ≝
1353 λe:exadecim.match e with
1354 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1355 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1356 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
1357 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
1359 (* operatore predecessore *)
1360 ndefinition pred_ex ≝
1363 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1364 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1366 (* operatore successore *)
1367 ndefinition succ_ex ≝
1370 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1371 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1373 (* operatore neg/complemento a 2 *)
1374 ndefinition compl_ex ≝
1375 λe:exadecim.match e with
1376 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1377 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1378 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1379 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1381 (* operatore x in [inf,sup] *)
1382 ndefinition inrange_ex ≝
1383 λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup).
1385 (* iteratore sugli esadecimali *)
1386 ndefinition forall_ex ≝ λP.
1387 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1388 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
1390 (* esadecimali ricorsivi *)
1391 ninductive rec_exadecim : exadecim → Type ≝
1392 ex_O : rec_exadecim x0
1393 | ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
1395 (* esadecimali → esadecimali ricorsivi *)
1396 ndefinition ex_to_recex ≝
1397 λn.match n return λx.rec_exadecim x with
1400 | x2 ⇒ ex_S ? (ex_S ? ex_O)
1401 | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
1402 | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
1403 | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
1404 | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
1405 | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
1406 | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
1407 | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
1408 | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
1409 | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))
1410 | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))
1411 | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))
1412 | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))
1413 | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))))
1416 (* quaternari → esadecimali *)
1417 ndefinition ex_of_qu ≝
1419 [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
1421 (* ottali → esadecimali *)
1422 ndefinition ex_of_oct ≝
1424 [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].