1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
24 include "num/quatern.ma".
26 include "common/prod.ma".
32 ninductive exadecim : Type ≝
50 (* iteratore sugli esadecimali *)
51 ndefinition forall_ex ≝ λP.
52 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
53 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
59 [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
60 | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
61 | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
62 | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
63 | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
64 | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
65 | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
66 | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
67 | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
68 | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
69 | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
70 | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
71 | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
72 | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
73 | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
74 | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
82 [ x0 ⇒ false | x1 ⇒ true | 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 ⇒ true | 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 ⇒ true
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 ⇒ true | 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 ⇒ true | 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 ⇒ true | 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 ⇒ true
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 ⇒ true | 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 ⇒ true | 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 ⇒ true | 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 ⇒ true
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 ⇒ true | 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 ⇒ true | 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 ⇒ true | 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 ⇒ true ]
157 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
158 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
159 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
160 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
168 [ x0 ⇒ true | 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 ⇒ true | 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 ⇒ true | 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 ⇒ true
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 ⇒ true | 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 ⇒ true | 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 ⇒ true | 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 ⇒ true
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 ⇒ true | 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 ⇒ true | 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 ⇒ true | 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 ⇒ true
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 ⇒ true | 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 ⇒ true | 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 ⇒ true | xF ⇒ true ]
243 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
244 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
245 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
246 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
254 [ x0 ⇒ false | 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 ⇒ false | 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 ⇒ false | 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 ⇒ false
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 ⇒ false | 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 ⇒ false | 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 ⇒ false | 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 ⇒ false
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 ⇒ false | 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 ⇒ false | 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 ⇒ false | 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 ⇒ false
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 ⇒ false | 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 ⇒ false | 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 ⇒ false | xF ⇒ false ]
329 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
330 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
331 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
332 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
340 [ x0 ⇒ true | x1 ⇒ false | 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 ⇒ false | 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 ⇒ false
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 ⇒ false | 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 ⇒ false | 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 ⇒ false | 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 ⇒ false
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 ⇒ false | 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 ⇒ false | 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 ⇒ false | 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 ⇒ false
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 ⇒ false | 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 ⇒ false | 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 ⇒ false | 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 ⇒ false ]
415 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
416 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
417 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
418 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
423 λe1,e2:exadecim.match e1 with
425 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
426 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
427 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
428 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
430 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
431 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
432 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
433 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
435 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
436 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
437 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
438 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
440 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
441 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
442 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
443 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
445 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
446 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
447 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
448 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
450 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
451 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
452 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
453 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
455 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
456 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
457 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
458 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
460 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
461 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
462 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
463 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
465 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
466 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
467 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
468 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
470 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
471 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
472 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
473 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
475 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
476 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
477 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
478 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
480 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
481 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
482 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
483 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
485 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
486 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
487 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
488 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
490 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
491 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
492 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
493 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
495 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
496 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
497 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
498 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
500 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
501 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
502 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
503 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
508 λe1,e2:exadecim.match e1 with
510 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
511 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
512 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
513 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
515 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
516 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
517 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
518 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
520 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
521 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
522 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
523 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
525 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
526 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
527 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
528 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
530 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
531 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
532 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
533 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
535 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
536 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
537 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
538 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
540 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
541 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
542 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
543 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
545 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
546 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
547 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
548 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
550 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
551 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
552 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
553 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
555 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
556 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
557 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
558 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
560 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
561 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
562 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
563 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
565 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
566 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
567 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
568 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
570 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
571 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
572 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
573 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
575 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
576 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
577 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
578 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
580 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
581 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
582 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
583 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
585 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
586 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
587 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
588 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
593 λe1,e2:exadecim.match e1 with
595 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
596 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
597 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
598 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
600 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
601 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
602 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
603 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
605 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
606 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
607 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
608 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
610 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
611 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
612 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
613 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
615 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
616 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
617 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
618 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
620 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
621 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
622 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
623 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
625 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
626 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
627 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
628 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
630 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
631 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
632 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
633 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
635 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
636 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
637 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
638 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
640 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
641 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
642 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
643 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
645 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
646 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
647 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
648 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
650 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
651 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
652 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
653 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
655 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
656 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
657 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
658 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
660 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
661 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
662 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
663 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
665 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
666 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
667 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
668 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
670 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
671 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
672 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
673 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
676 (* operatore Most Significant Bit *)
677 ndefinition getMSB_ex ≝
678 λe:exadecim.match e with
679 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
680 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
681 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
682 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
684 ndefinition setMSB_ex ≝
685 λe:exadecim.match e with
686 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
687 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
688 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
689 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ].
691 (* operatore Least Significant Bit *)
692 ndefinition getLSB_ex ≝
693 λe:exadecim.match e with
694 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true
695 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true
696 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true
697 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ].
699 ndefinition setLSB_ex ≝
700 λe:exadecim.match e with
701 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
702 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
703 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
704 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
706 (* operatore rotazione destra con carry *)
708 λc:bool.λe:exadecim.match c with
709 [ true ⇒ match e with
710 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … true x8
711 | x2 ⇒ pair … false x9 | x3 ⇒ pair … true x9
712 | x4 ⇒ pair … false xA | x5 ⇒ pair … true xA
713 | x6 ⇒ pair … false xB | x7 ⇒ pair … true xB
714 | x8 ⇒ pair … false xC | x9 ⇒ pair … true xC
715 | xA ⇒ pair … false xD | xB ⇒ pair … true xD
716 | xC ⇒ pair … false xE | xD ⇒ pair … true xE
717 | xE ⇒ pair … false xF | xF ⇒ pair … true xF ]
718 | false ⇒ match e with
719 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
720 | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
721 | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
722 | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
723 | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
724 | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
725 | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
726 | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ]
729 (* operatore shift destro *)
731 λe:exadecim.match e with
732 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
733 | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
734 | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
735 | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
736 | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
737 | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
738 | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
739 | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ].
741 (* operatore rotazione destra *)
743 λe:exadecim.match e with
744 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
745 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
746 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
747 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
749 (* operatore rotazione sinistra con carry *)
751 λc:bool.λe:exadecim.match c with
752 [ true ⇒ match e with
753 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x3
754 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x7
755 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xB
756 | x6 ⇒ pair … false xD | x7 ⇒ pair … false xF
757 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x3
758 | xA ⇒ pair … true x5 | xB ⇒ pair … true x7
759 | xC ⇒ pair … true x9 | xD ⇒ pair … true xB
760 | xE ⇒ pair … true xD | xF ⇒ pair … true xF ]
761 | false ⇒ match e with
762 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
763 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
764 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
765 | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
766 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2
767 | xA ⇒ pair … true x4 | xB ⇒ pair … true x6
768 | xC ⇒ pair … true x8 | xD ⇒ pair … true xA
769 | xE ⇒ pair … true xC | xF ⇒ pair … true xE ]
772 (* operatore shift sinistro *)
774 λe:exadecim.match e with
775 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
776 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
777 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
778 | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
779 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2
780 | xA ⇒ pair … true x4 | xB ⇒ pair … true x6
781 | xC ⇒ pair … true x8 | xD ⇒ pair … true xA
782 | xE ⇒ pair … true xC | xF ⇒ pair … true xE ].
784 (* operatore rotazione sinistra *)
786 λe:exadecim.match e with
787 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
788 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
789 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
790 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
792 (* operatore not/complemento a 1 *)
794 λe:exadecim.match e with
795 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
796 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
797 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
798 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
800 (* operatore somma con data+carry → data+carry *)
801 ndefinition plus_ex_dc_dc ≝
802 λc:bool.λe1,e2:exadecim.
804 [ true ⇒ match e1 with
806 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
807 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
808 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
809 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
811 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
812 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
813 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
814 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
816 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
817 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
818 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
819 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
821 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
822 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
823 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
824 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
826 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
827 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
828 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
829 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
831 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
832 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
833 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
834 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
836 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
837 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
838 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
839 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
841 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
842 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
843 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
844 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
846 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
847 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
848 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
849 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
851 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
852 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
853 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
854 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
856 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
857 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
858 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
859 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
861 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
862 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
863 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
864 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
866 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
867 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
868 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
869 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
871 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
872 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
873 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
874 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
876 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
877 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
878 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
879 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
881 [ x0 ⇒ pair … true x0 | x1 ⇒ pair … true x1 | x2 ⇒ pair … true x2 | x3 ⇒ pair … true x3
882 | x4 ⇒ pair … true x4 | x5 ⇒ pair … true x5 | x6 ⇒ pair … true x6 | x7 ⇒ pair … true x7
883 | x8 ⇒ pair … true x8 | x9 ⇒ pair … true x9 | xA ⇒ pair … true xA | xB ⇒ pair … true xB
884 | xC ⇒ pair … true xC | xD ⇒ pair … true xD | xE ⇒ pair … true xE | xF ⇒ pair … true xF ]
886 | false ⇒ match e1 with
888 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
889 | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
890 | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
891 | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]
893 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
894 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
895 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
896 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
898 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
899 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
900 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
901 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
903 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
904 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
905 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
906 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
908 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
909 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
910 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
911 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
913 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
914 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
915 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
916 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
918 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
919 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
920 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
921 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
923 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
924 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
925 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
926 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
928 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
929 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
930 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
931 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
933 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
934 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
935 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
936 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
938 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
939 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
940 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
941 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
943 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
944 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
945 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
946 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
948 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
949 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
950 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
951 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
953 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
954 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
955 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
956 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
958 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
959 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
960 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
961 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
963 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
964 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
965 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
966 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
969 (* operatore somma con data → data+carry *)
970 ndefinition plus_ex_d_dc ≝
974 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
975 | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
976 | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
977 | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]
979 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
980 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
981 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
982 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
984 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
985 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
986 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
987 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
989 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
990 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
991 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
992 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
994 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
995 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
996 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
997 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
999 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
1000 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
1001 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
1002 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
1003 | x6 ⇒ match e2 with
1004 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
1005 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
1006 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
1007 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
1008 | x7 ⇒ match e2 with
1009 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
1010 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
1011 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
1012 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
1013 | x8 ⇒ match e2 with
1014 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
1015 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
1016 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
1017 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
1018 | x9 ⇒ match e2 with
1019 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
1020 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
1021 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
1022 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
1023 | xA ⇒ match e2 with
1024 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
1025 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
1026 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
1027 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
1028 | xB ⇒ match e2 with
1029 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
1030 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
1031 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
1032 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
1033 | xC ⇒ match e2 with
1034 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
1035 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
1036 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
1037 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
1038 | xD ⇒ match e2 with
1039 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
1040 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
1041 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
1042 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
1043 | xE ⇒ match e2 with
1044 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
1045 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
1046 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
1047 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
1048 | xF ⇒ match e2 with
1049 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
1050 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
1051 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
1052 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
1055 (* operatore somma con data+carry → data *)
1056 ndefinition plus_ex_dc_d ≝
1057 λc:bool.λe1,e2:exadecim.
1059 [ true ⇒ match e1 with
1060 [ x0 ⇒ match e2 with
1061 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1062 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1063 | x1 ⇒ match e2 with
1064 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1065 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1066 | x2 ⇒ match e2 with
1067 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1068 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1069 | x3 ⇒ match e2 with
1070 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1071 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1072 | x4 ⇒ match e2 with
1073 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1074 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1075 | x5 ⇒ match e2 with
1076 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1077 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1078 | x6 ⇒ match e2 with
1079 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1080 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1081 | x7 ⇒ match e2 with
1082 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1083 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1084 | x8 ⇒ match e2 with
1085 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1086 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1087 | x9 ⇒ match e2 with
1088 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1089 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1090 | xA ⇒ match e2 with
1091 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1092 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1093 | xB ⇒ match e2 with
1094 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1095 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1096 | xC ⇒ match e2 with
1097 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1098 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1099 | xD ⇒ match e2 with
1100 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1101 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1102 | xE ⇒ match e2 with
1103 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1104 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1105 | xF ⇒ match e2 with
1106 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1107 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1109 | false ⇒ match e1 with
1110 [ x0 ⇒ match e2 with
1111 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1112 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1113 | x1 ⇒ match e2 with
1114 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1115 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1116 | x2 ⇒ match e2 with
1117 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1118 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1119 | x3 ⇒ match e2 with
1120 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1121 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1122 | x4 ⇒ match e2 with
1123 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1124 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1125 | x5 ⇒ match e2 with
1126 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1127 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1128 | x6 ⇒ match e2 with
1129 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1130 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1131 | x7 ⇒ match e2 with
1132 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1133 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1134 | x8 ⇒ match e2 with
1135 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1136 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1137 | x9 ⇒ match e2 with
1138 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1139 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1140 | xA ⇒ match e2 with
1141 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1142 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1143 | xB ⇒ match e2 with
1144 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1145 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1146 | xC ⇒ match e2 with
1147 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1148 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1149 | xD ⇒ match e2 with
1150 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1151 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1152 | xE ⇒ match e2 with
1153 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1154 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1155 | xF ⇒ match e2 with
1156 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1157 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1160 (* operatore somma con data → data *)
1161 ndefinition plus_ex_d_d ≝
1164 [ x0 ⇒ match e2 with
1165 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1166 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1167 | x1 ⇒ match e2 with
1168 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1169 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1170 | x2 ⇒ match e2 with
1171 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1172 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1173 | x3 ⇒ match e2 with
1174 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1175 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1176 | x4 ⇒ match e2 with
1177 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1178 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1179 | x5 ⇒ match e2 with
1180 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1181 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1182 | x6 ⇒ match e2 with
1183 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1184 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1185 | x7 ⇒ match e2 with
1186 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1187 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1188 | x8 ⇒ match e2 with
1189 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1190 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1191 | x9 ⇒ match e2 with
1192 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1193 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1194 | xA ⇒ match e2 with
1195 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1196 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1197 | xB ⇒ match e2 with
1198 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1199 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1200 | xC ⇒ match e2 with
1201 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1202 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1203 | xD ⇒ match e2 with
1204 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1205 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1206 | xE ⇒ match e2 with
1207 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1208 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1209 | xF ⇒ match e2 with
1210 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1211 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1214 (* operatore somma con data+carry → carry *)
1215 ndefinition plus_ex_dc_c ≝
1216 λc:bool.λe1,e2:exadecim.
1218 [ true ⇒ match e1 with
1219 [ x0 ⇒ match e2 with
1220 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1221 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1222 | x1 ⇒ match e2 with
1223 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1224 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1225 | x2 ⇒ match e2 with
1226 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1227 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1228 | x3 ⇒ match e2 with
1229 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1230 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1231 | x4 ⇒ match e2 with
1232 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1233 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1234 | x5 ⇒ match e2 with
1235 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1236 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1237 | x6 ⇒ match e2 with
1238 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1239 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1240 | x7 ⇒ match e2 with
1241 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1242 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1243 | x8 ⇒ match e2 with
1244 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1245 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1246 | x9 ⇒ match e2 with
1247 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1248 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1249 | xA ⇒ match e2 with
1250 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1251 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1252 | xB ⇒ match e2 with
1253 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1254 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1255 | xC ⇒ match e2 with
1256 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1257 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1258 | xD ⇒ match e2 with
1259 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1260 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1261 | xE ⇒ match e2 with
1262 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1263 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1264 | xF ⇒ match e2 with
1265 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1266 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1268 | false ⇒ match e1 with
1269 [ x0 ⇒ match e2 with
1270 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1271 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1272 | x1 ⇒ match e2 with
1273 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1274 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1275 | x2 ⇒ match e2 with
1276 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1277 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1278 | x3 ⇒ match e2 with
1279 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1280 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1281 | x4 ⇒ match e2 with
1282 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1283 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1284 | x5 ⇒ match e2 with
1285 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1286 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1287 | x6 ⇒ match e2 with
1288 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1289 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1290 | x7 ⇒ match e2 with
1291 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1292 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1293 | x8 ⇒ match e2 with
1294 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1295 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1296 | x9 ⇒ match e2 with
1297 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1298 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1299 | xA ⇒ match e2 with
1300 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1301 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1302 | xB ⇒ match e2 with
1303 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1304 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1305 | xC ⇒ match e2 with
1306 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1307 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1308 | xD ⇒ match e2 with
1309 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1310 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1311 | xE ⇒ match e2 with
1312 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1313 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1314 | xF ⇒ match e2 with
1315 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1316 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1319 (* operatore somma con data → carry *)
1320 ndefinition plus_ex_d_c ≝
1323 [ x0 ⇒ match e2 with
1324 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1325 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1326 | x1 ⇒ match e2 with
1327 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1328 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1329 | x2 ⇒ match e2 with
1330 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1331 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1332 | x3 ⇒ match e2 with
1333 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1334 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1335 | x4 ⇒ match e2 with
1336 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1337 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1338 | x5 ⇒ match e2 with
1339 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1340 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1341 | x6 ⇒ match e2 with
1342 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1343 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1344 | x7 ⇒ match e2 with
1345 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1346 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1347 | x8 ⇒ match e2 with
1348 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1349 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1350 | x9 ⇒ match e2 with
1351 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1352 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1353 | xA ⇒ match e2 with
1354 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1355 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1356 | xB ⇒ match e2 with
1357 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1358 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1359 | xC ⇒ match e2 with
1360 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1361 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1362 | xD ⇒ match e2 with
1363 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1364 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1365 | xE ⇒ match e2 with
1366 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1367 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1368 | xF ⇒ match e2 with
1369 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1370 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1373 (* operatore predecessore *)
1374 ndefinition pred_ex ≝
1377 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1378 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1380 (* operatore successore *)
1381 ndefinition succ_ex ≝
1384 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1385 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1387 (* operatore neg/complemento a 2 *)
1388 ndefinition compl_ex ≝
1389 λe:exadecim.match e with
1390 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1391 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1392 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1393 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1395 (* operatore x in [inf,sup] o in sup],[inf *)
1396 ndefinition inrange_ex ≝
1397 λx,inf,sup:exadecim.
1398 match le_ex inf sup with
1399 [ true ⇒ and_bool | false ⇒ or_bool ]
1400 (le_ex inf x) (le_ex x sup).
1402 (* esadecimali ricorsivi *)
1403 ninductive rec_exadecim : exadecim → Type ≝
1404 ex_O : rec_exadecim x0
1405 | ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
1407 (* esadecimali → esadecimali ricorsivi *)
1408 ndefinition ex_to_recex ≝
1409 λn.match n return λx.rec_exadecim x with
1412 | x2 ⇒ ex_S ? (ex_S ? ex_O)
1413 | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
1414 | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
1415 | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
1416 | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
1417 | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
1418 | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
1419 | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
1420 | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
1421 | 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))))))))))
1422 | 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)))))))))))
1423 | 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))))))))))))
1424 | 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)))))))))))))
1425 | 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))))))))))))))
1428 (* quaternari → esadecimali *)
1429 ndefinition ex_of_qu ≝
1431 [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
1433 (* ottali → esadecimali *)
1434 ndefinition ex_of_oct ≝
1436 [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
1438 (* esadecimali xNNNN → ottali *)
1439 ndefinition oct_of_exL ≝
1441 [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
1442 | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
1444 (* esadecimali NNNNx → ottali *)
1445 ndefinition oct_of_exH ≝
1447 [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3
1448 | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ].