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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/bool.ma".
24 include "freescale/quatern.ma".
25 include "freescale/oct.ma".
26 include "freescale/prod.ma".
32 ninductive exadecim : Type ≝
54 [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
55 | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
56 | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
57 | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
58 | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
59 | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
60 | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
61 | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
62 | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
63 | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
64 | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
65 | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
66 | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
67 | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
68 | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
69 | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
77 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
78 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
79 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
80 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
82 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
83 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
84 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
85 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
87 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
88 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
89 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
90 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
92 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
93 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
94 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
95 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
97 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
98 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
99 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
100 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
102 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
103 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
104 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
105 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
107 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
108 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
109 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
110 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
112 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
113 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
114 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
115 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
117 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
118 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
119 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
120 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
122 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
123 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
124 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
125 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
127 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
128 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
129 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
130 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
132 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
133 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
134 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
135 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
137 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
138 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
139 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
140 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
142 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
143 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
144 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
145 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
147 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
148 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
149 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
150 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
152 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
153 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
154 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
155 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
163 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
164 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
165 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
166 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
168 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
169 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
170 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
171 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
173 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
174 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
175 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
176 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
178 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
179 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
180 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
181 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
183 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
184 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
185 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
186 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
188 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
189 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
190 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
191 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
193 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
194 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
195 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
196 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
198 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
199 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
200 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
201 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
203 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
204 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
205 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
206 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
208 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
209 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
210 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
211 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
213 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
214 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
215 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
216 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
218 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
219 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
220 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
221 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
223 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
224 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
225 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
226 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
228 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
229 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
230 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
231 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
233 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
234 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
235 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
236 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
238 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
239 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
240 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
241 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
249 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
250 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
251 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
252 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
254 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
255 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
256 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
257 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
259 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
260 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
261 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
262 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
264 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
265 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
266 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
267 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
269 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
270 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
271 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
272 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
274 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
275 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
276 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
277 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
279 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
280 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
281 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
282 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
284 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
285 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
286 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
287 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
289 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
290 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
291 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
292 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
294 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
295 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
296 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
297 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
299 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
300 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
301 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
302 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
304 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
305 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
306 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
307 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
309 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
310 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
311 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
312 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
314 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
315 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
316 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
317 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
319 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
320 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
321 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
322 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
324 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
325 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
326 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
327 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
335 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
336 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
337 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
338 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
340 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
341 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
342 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
343 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
345 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
346 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
347 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
348 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
350 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
351 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
352 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
353 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
355 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
356 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
357 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
358 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
360 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
361 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
362 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
363 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
365 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
366 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
367 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
368 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
370 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
371 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
372 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
373 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
375 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
376 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
377 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
378 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
380 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
381 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
382 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
383 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
385 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
386 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
387 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
388 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
390 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
391 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
392 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
393 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
395 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
396 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
397 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
398 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
400 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
401 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
402 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
403 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
405 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
406 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
407 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
408 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
410 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
411 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
412 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
413 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
418 λe1,e2:exadecim.match e1 with
420 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
421 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
422 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
423 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
425 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
426 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
427 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
428 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
430 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
431 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
432 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
433 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
435 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
436 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
437 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
438 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
440 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
441 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
442 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
443 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
445 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
446 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
447 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
448 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
450 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
451 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
452 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
453 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
455 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
456 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
457 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
458 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
460 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
461 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
462 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
463 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
465 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
466 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
467 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
468 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
470 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
471 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
472 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
473 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
475 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
476 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
477 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
478 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
480 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
481 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
482 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
483 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
485 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
486 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
487 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
488 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
490 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
491 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
492 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
493 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
495 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
496 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
497 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
498 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
503 λe1,e2:exadecim.match e1 with
505 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
506 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
507 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
508 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
510 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
511 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
512 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
513 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
515 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
516 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
517 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
518 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
520 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
521 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
522 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
523 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
525 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
526 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
527 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
528 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
530 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
531 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
532 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
533 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
535 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
536 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
537 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
538 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
540 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
541 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
542 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
543 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
545 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
546 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
547 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
548 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
550 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
551 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
552 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
553 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
555 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
556 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
557 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
558 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
560 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
561 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
562 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
563 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
565 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
566 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
567 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
568 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
570 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
571 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
572 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
573 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
575 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
576 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
577 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
578 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
580 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
581 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
582 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
583 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
588 λe1,e2:exadecim.match e1 with
590 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
591 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
592 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
593 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
595 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
596 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
597 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
598 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
600 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
601 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
602 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
603 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
605 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
606 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
607 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
608 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
610 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
611 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
612 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
613 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
615 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
616 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
617 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
618 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
620 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
621 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
622 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
623 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
625 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
626 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
627 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
628 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
630 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
631 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
632 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
633 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
635 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
636 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
637 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
638 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
640 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
641 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
642 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
643 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
645 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
646 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
647 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
648 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
650 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
651 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
652 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
653 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
655 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
656 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
657 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
658 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
660 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
661 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
662 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
663 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
665 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
666 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
667 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
668 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
671 (* operatore rotazione destra con carry *)
673 λe:exadecim.λc:bool.match c with
674 [ true ⇒ match e with
675 [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
676 | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
677 | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
678 | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
679 | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
680 | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
681 | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
682 | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
683 | false ⇒ match e with
684 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
685 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
686 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
687 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
688 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
689 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
690 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
691 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
694 (* operatore shift destro *)
696 λe:exadecim.match e with
697 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
698 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
699 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
700 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
701 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
702 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
703 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
704 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
706 (* operatore rotazione destra *)
708 λe:exadecim.match e with
709 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
710 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
711 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
712 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
714 (* operatore rotazione destra n-volte *)
715 nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
718 | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ].
720 (* operatore rotazione sinistra con carry *)
722 λe:exadecim.λc:bool.match c with
723 [ true ⇒ match e with
724 [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
725 | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
726 | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
727 | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
728 | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
729 | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
730 | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
731 | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
732 | false ⇒ match e with
733 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
734 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
735 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
736 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
737 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
738 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
739 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
740 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
743 (* operatore shift sinistro *)
745 λe:exadecim.match e with
746 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
747 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
748 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
749 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
750 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
751 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
752 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
753 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
755 (* operatore rotazione sinistra *)
757 λe:exadecim.match e with
758 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
759 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
760 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
761 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
763 (* operatore rotazione sinistra n-volte *)
764 nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
767 | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ].
769 (* operatore not/complemento a 1 *)
771 λe:exadecim.match e with
772 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
773 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
774 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
775 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
777 (* operatore somma con data+carry → data+carry *)
778 ndefinition plus_ex_dc_dc ≝
779 λe1,e2:exadecim.λc:bool.
781 [ true ⇒ match e1 with
783 [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
784 | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
785 | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
786 | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
788 [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
789 | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
790 | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
791 | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
793 [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
794 | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
795 | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
796 | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
798 [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
799 | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
800 | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
801 | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
803 [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
804 | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
805 | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
806 | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
808 [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
809 | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
810 | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
811 | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
813 [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
814 | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
815 | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
816 | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
818 [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
819 | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
820 | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
821 | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
823 [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
824 | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
825 | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
826 | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
828 [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
829 | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
830 | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
831 | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
833 [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
834 | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
835 | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
836 | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
838 [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
839 | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
840 | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
841 | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
843 [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
844 | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
845 | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
846 | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
848 [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
849 | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
850 | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
851 | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
853 [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
854 | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
855 | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
856 | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
858 [ x0 ⇒ pair … x0 true | x1 ⇒ pair … x1 true | x2 ⇒ pair … x2 true | x3 ⇒ pair … x3 true
859 | x4 ⇒ pair … x4 true | x5 ⇒ pair … x5 true | x6 ⇒ pair … x6 true | x7 ⇒ pair … x7 true
860 | x8 ⇒ pair … x8 true | x9 ⇒ pair … x9 true | xA ⇒ pair … xA true | xB ⇒ pair … xB true
861 | xC ⇒ pair … xC true | xD ⇒ pair … xD true | xE ⇒ pair … xE true | xF ⇒ pair … xF true ]
863 | false ⇒ match e1 with
865 [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
866 | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
867 | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
868 | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
870 [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
871 | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
872 | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
873 | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
875 [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
876 | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
877 | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
878 | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
880 [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
881 | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
882 | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
883 | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
885 [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
886 | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
887 | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
888 | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
890 [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
891 | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
892 | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
893 | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
895 [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
896 | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
897 | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
898 | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
900 [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
901 | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
902 | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
903 | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
905 [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
906 | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
907 | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
908 | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
910 [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
911 | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
912 | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
913 | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
915 [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
916 | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
917 | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
918 | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
920 [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
921 | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
922 | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
923 | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
925 [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
926 | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
927 | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
928 | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
930 [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
931 | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
932 | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
933 | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
935 [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
936 | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
937 | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
938 | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
940 [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
941 | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
942 | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
943 | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
946 (* operatore somma con data → data+carry *)
947 ndefinition plus_ex_d_dc ≝
951 [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
952 | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
953 | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
954 | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
956 [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
957 | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
958 | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
959 | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
961 [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
962 | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
963 | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
964 | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
966 [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
967 | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
968 | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
969 | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
971 [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
972 | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
973 | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
974 | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
976 [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
977 | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
978 | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
979 | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
981 [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
982 | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
983 | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
984 | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
986 [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
987 | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
988 | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
989 | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
991 [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
992 | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
993 | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
994 | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
996 [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
997 | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
998 | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
999 | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
1000 | xA ⇒ match e2 with
1001 [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
1002 | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
1003 | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
1004 | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
1005 | xB ⇒ match e2 with
1006 [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
1007 | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
1008 | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
1009 | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
1010 | xC ⇒ match e2 with
1011 [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
1012 | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
1013 | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
1014 | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
1015 | xD ⇒ match e2 with
1016 [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
1017 | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
1018 | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
1019 | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
1020 | xE ⇒ match e2 with
1021 [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
1022 | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
1023 | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
1024 | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
1025 | xF ⇒ match e2 with
1026 [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
1027 | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
1028 | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
1029 | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
1032 (* operatore somma con data+carry → data *)
1033 ndefinition plus_ex_dc_d ≝
1034 λe1,e2:exadecim.λc:bool.
1036 [ true ⇒ match e1 with
1037 [ x0 ⇒ match e2 with
1038 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1039 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1040 | x1 ⇒ match e2 with
1041 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1042 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1043 | x2 ⇒ match e2 with
1044 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1045 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1046 | x3 ⇒ match e2 with
1047 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1048 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1049 | x4 ⇒ match e2 with
1050 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1051 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1052 | x5 ⇒ match e2 with
1053 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1054 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1055 | x6 ⇒ match e2 with
1056 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1057 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1058 | x7 ⇒ match e2 with
1059 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1060 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1061 | x8 ⇒ match e2 with
1062 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1063 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1064 | x9 ⇒ match e2 with
1065 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1066 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1067 | xA ⇒ match e2 with
1068 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1069 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1070 | xB ⇒ match e2 with
1071 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1072 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1073 | xC ⇒ match e2 with
1074 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1075 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1076 | xD ⇒ match e2 with
1077 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1078 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1079 | xE ⇒ match e2 with
1080 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1081 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1082 | xF ⇒ match e2 with
1083 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1084 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1086 | false ⇒ match e1 with
1087 [ x0 ⇒ match e2 with
1088 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1089 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1090 | x1 ⇒ match e2 with
1091 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1092 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1093 | x2 ⇒ match e2 with
1094 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1095 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1096 | x3 ⇒ match e2 with
1097 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1098 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1099 | x4 ⇒ match e2 with
1100 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1101 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1102 | x5 ⇒ match e2 with
1103 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1104 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1105 | x6 ⇒ match e2 with
1106 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1107 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1108 | x7 ⇒ match e2 with
1109 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1110 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1111 | x8 ⇒ match e2 with
1112 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1113 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1114 | x9 ⇒ match e2 with
1115 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1116 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1117 | xA ⇒ match e2 with
1118 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1119 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1120 | xB ⇒ match e2 with
1121 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1122 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1123 | xC ⇒ match e2 with
1124 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1125 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1126 | xD ⇒ match e2 with
1127 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1128 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1129 | xE ⇒ match e2 with
1130 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1131 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1132 | xF ⇒ match e2 with
1133 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1134 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1137 (* operatore somma con data → data *)
1138 ndefinition plus_ex_d_d ≝
1141 [ x0 ⇒ match e2 with
1142 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1143 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1144 | x1 ⇒ match e2 with
1145 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1146 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1147 | x2 ⇒ match e2 with
1148 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1149 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1150 | x3 ⇒ match e2 with
1151 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1152 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1153 | x4 ⇒ match e2 with
1154 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1155 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1156 | x5 ⇒ match e2 with
1157 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1158 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1159 | x6 ⇒ match e2 with
1160 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1161 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1162 | x7 ⇒ match e2 with
1163 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1164 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1165 | x8 ⇒ match e2 with
1166 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1167 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1168 | x9 ⇒ match e2 with
1169 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1170 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1171 | xA ⇒ match e2 with
1172 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1173 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1174 | xB ⇒ match e2 with
1175 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1176 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1177 | xC ⇒ match e2 with
1178 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1179 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1180 | xD ⇒ match e2 with
1181 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1182 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1183 | xE ⇒ match e2 with
1184 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1185 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1186 | xF ⇒ match e2 with
1187 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1188 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1191 (* operatore somma con data+carry → carry *)
1192 ndefinition plus_ex_dc_c ≝
1193 λe1,e2:exadecim.λc:bool.
1195 [ true ⇒ match e1 with
1196 [ x0 ⇒ match e2 with
1197 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1198 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1199 | x1 ⇒ match e2 with
1200 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1201 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1202 | x2 ⇒ match e2 with
1203 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1204 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1205 | x3 ⇒ match e2 with
1206 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1207 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1208 | x4 ⇒ match e2 with
1209 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1210 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1211 | x5 ⇒ match e2 with
1212 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1213 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1214 | x6 ⇒ match e2 with
1215 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1216 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1217 | x7 ⇒ match e2 with
1218 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1219 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1220 | x8 ⇒ match e2 with
1221 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1222 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1223 | x9 ⇒ match e2 with
1224 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1225 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1226 | xA ⇒ match e2 with
1227 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1228 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1229 | xB ⇒ match e2 with
1230 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1231 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1232 | xC ⇒ match e2 with
1233 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1234 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1235 | xD ⇒ match e2 with
1236 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1237 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1238 | xE ⇒ match e2 with
1239 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1240 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1241 | xF ⇒ match e2 with
1242 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1243 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1245 | false ⇒ match e1 with
1246 [ x0 ⇒ match e2 with
1247 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1248 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1249 | x1 ⇒ match e2 with
1250 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1251 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1252 | x2 ⇒ match e2 with
1253 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1254 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1255 | x3 ⇒ match e2 with
1256 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1257 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1258 | x4 ⇒ match e2 with
1259 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1260 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1261 | x5 ⇒ match e2 with
1262 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1263 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1264 | x6 ⇒ match e2 with
1265 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1266 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1267 | x7 ⇒ match e2 with
1268 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1269 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1270 | x8 ⇒ match e2 with
1271 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1272 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1273 | x9 ⇒ match e2 with
1274 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1275 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1276 | xA ⇒ match e2 with
1277 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1278 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1279 | xB ⇒ match e2 with
1280 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1281 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1282 | xC ⇒ match e2 with
1283 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1284 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1285 | xD ⇒ match e2 with
1286 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1287 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1288 | xE ⇒ match e2 with
1289 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1290 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1291 | xF ⇒ match e2 with
1292 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1293 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1296 (* operatore somma con data → carry *)
1297 ndefinition plus_ex_d_c ≝
1300 [ x0 ⇒ match e2 with
1301 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1302 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1303 | x1 ⇒ match e2 with
1304 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1305 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1306 | x2 ⇒ match e2 with
1307 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1308 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1309 | x3 ⇒ match e2 with
1310 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1311 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1312 | x4 ⇒ match e2 with
1313 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1314 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1315 | x5 ⇒ match e2 with
1316 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1317 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1318 | x6 ⇒ match e2 with
1319 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1320 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1321 | x7 ⇒ match e2 with
1322 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1323 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1324 | x8 ⇒ match e2 with
1325 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1326 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1327 | x9 ⇒ match e2 with
1328 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1329 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1330 | xA ⇒ match e2 with
1331 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1332 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1333 | xB ⇒ match e2 with
1334 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1335 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1336 | xC ⇒ match e2 with
1337 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1338 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1339 | xD ⇒ match e2 with
1340 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1341 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1342 | xE ⇒ match e2 with
1343 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1344 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1345 | xF ⇒ match e2 with
1346 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1347 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1350 (* operatore Most Significant Bit *)
1351 ndefinition MSB_ex ≝
1352 λe:exadecim.match e with
1353 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1354 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1355 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
1356 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
1358 (* operatore predecessore *)
1359 ndefinition pred_ex ≝
1362 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1363 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1365 (* operatore successore *)
1366 ndefinition succ_ex ≝
1369 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1370 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1372 (* operatore neg/complemento a 2 *)
1373 ndefinition compl_ex ≝
1374 λe:exadecim.match e with
1375 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1376 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1377 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1378 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1380 (* iteratore sugli esadecimali *)
1381 ndefinition forall_ex ≝ λP.
1382 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1383 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
1385 (* esadecimali ricorsivi *)
1386 ninductive rec_exadecim : exadecim → Type ≝
1387 ex_O : rec_exadecim x0
1388 | ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
1390 (* esadecimali → esadecimali ricorsivi *)
1391 ndefinition ex_to_recex ≝
1392 λn.match n return λx.rec_exadecim x with
1395 | x2 ⇒ ex_S ? (ex_S ? ex_O)
1396 | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
1397 | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
1398 | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
1399 | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
1400 | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
1401 | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
1402 | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
1403 | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
1404 | 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))))))))))
1405 | 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)))))))))))
1406 | 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))))))))))))
1407 | 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)))))))))))))
1408 | 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))))))))))))))
1411 (* quaternari → esadecimali *)
1412 ndefinition ex_of_qu ≝
1414 [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
1416 (* ottali → esadecimali *)
1417 ndefinition ex_of_oct ≝
1419 [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].