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 ndefinition clrMSB_ex ≝
692 λe:exadecim.match e with
693 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
694 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
695 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
696 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ].
698 (* operatore Least Significant Bit *)
699 ndefinition getLSB_ex ≝
700 λe:exadecim.match e with
701 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true
702 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true
703 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true
704 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ].
706 ndefinition setLSB_ex ≝
707 λe:exadecim.match e with
708 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
709 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
710 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
711 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
713 ndefinition clrLSB_ex ≝
714 λe:exadecim.match e with
715 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
716 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
717 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
718 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ].
720 (* operatore rotazione destra con carry *)
722 λc:bool.λe:exadecim.match c with
723 [ true ⇒ match e with
724 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … true x8
725 | x2 ⇒ pair … false x9 | x3 ⇒ pair … true x9
726 | x4 ⇒ pair … false xA | x5 ⇒ pair … true xA
727 | x6 ⇒ pair … false xB | x7 ⇒ pair … true xB
728 | x8 ⇒ pair … false xC | x9 ⇒ pair … true xC
729 | xA ⇒ pair … false xD | xB ⇒ pair … true xD
730 | xC ⇒ pair … false xE | xD ⇒ pair … true xE
731 | xE ⇒ pair … false xF | xF ⇒ pair … true xF ]
732 | false ⇒ match e with
733 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
734 | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
735 | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
736 | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
737 | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
738 | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
739 | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
740 | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ]
743 (* operatore shift destro *)
745 λe:exadecim.match e with
746 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
747 | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
748 | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
749 | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
750 | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
751 | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
752 | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
753 | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ].
755 (* operatore rotazione destra *)
757 λe:exadecim.match e with
758 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
759 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
760 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
761 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
763 (* operatore rotazione sinistra con carry *)
765 λc:bool.λe:exadecim.match c with
766 [ true ⇒ match e with
767 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x3
768 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x7
769 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xB
770 | x6 ⇒ pair … false xD | x7 ⇒ pair … false xF
771 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x3
772 | xA ⇒ pair … true x5 | xB ⇒ pair … true x7
773 | xC ⇒ pair … true x9 | xD ⇒ pair … true xB
774 | xE ⇒ pair … true xD | xF ⇒ pair … true xF ]
775 | false ⇒ match e with
776 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
777 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
778 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
779 | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
780 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2
781 | xA ⇒ pair … true x4 | xB ⇒ pair … true x6
782 | xC ⇒ pair … true x8 | xD ⇒ pair … true xA
783 | xE ⇒ pair … true xC | xF ⇒ pair … true xE ]
786 (* operatore shift sinistro *)
788 λe:exadecim.match e with
789 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
790 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
791 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
792 | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
793 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2
794 | xA ⇒ pair … true x4 | xB ⇒ pair … true x6
795 | xC ⇒ pair … true x8 | xD ⇒ pair … true xA
796 | xE ⇒ pair … true xC | xF ⇒ pair … true xE ].
798 (* operatore rotazione sinistra *)
800 λe:exadecim.match e with
801 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
802 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
803 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
804 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
806 (* operatore not/complemento a 1 *)
808 λe:exadecim.match e with
809 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
810 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
811 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
812 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
814 (* operatore somma con data+carry → data+carry *)
815 ndefinition plus_ex_dc_dc ≝
816 λc:bool.λe1,e2:exadecim.
818 [ true ⇒ match e1 with
820 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
821 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
822 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
823 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
825 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
826 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
827 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
828 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
830 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
831 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
832 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
833 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
835 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
836 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
837 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
838 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
840 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
841 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
842 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
843 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
845 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
846 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
847 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
848 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
850 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
851 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
852 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
853 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
855 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
856 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
857 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
858 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
860 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
861 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
862 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
863 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
865 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
866 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
867 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
868 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
870 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
871 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
872 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
873 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
875 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
876 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
877 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
878 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
880 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
881 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
882 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
883 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
885 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
886 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
887 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
888 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
890 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
891 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
892 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
893 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
895 [ x0 ⇒ pair … true x0 | x1 ⇒ pair … true x1 | x2 ⇒ pair … true x2 | x3 ⇒ pair … true x3
896 | x4 ⇒ pair … true x4 | x5 ⇒ pair … true x5 | x6 ⇒ pair … true x6 | x7 ⇒ pair … true x7
897 | x8 ⇒ pair … true x8 | x9 ⇒ pair … true x9 | xA ⇒ pair … true xA | xB ⇒ pair … true xB
898 | xC ⇒ pair … true xC | xD ⇒ pair … true xD | xE ⇒ pair … true xE | xF ⇒ pair … true xF ]
900 | false ⇒ match e1 with
902 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
903 | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
904 | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
905 | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]
907 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
908 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
909 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
910 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
912 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
913 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
914 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
915 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
917 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
918 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
919 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
920 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
922 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
923 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
924 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
925 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
927 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
928 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
929 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
930 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
932 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
933 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
934 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
935 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
937 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
938 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
939 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
940 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
942 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
943 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
944 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
945 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
947 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
948 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
949 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
950 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
952 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
953 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
954 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
955 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
957 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
958 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
959 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
960 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
962 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
963 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
964 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
965 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
967 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
968 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
969 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
970 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
972 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
973 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
974 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
975 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
977 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
978 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
979 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
980 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
983 (* operatore somma con data → data+carry *)
984 ndefinition plus_ex_d_dc ≝
988 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
989 | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
990 | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
991 | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]
993 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
994 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
995 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
996 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
998 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
999 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
1000 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
1001 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
1002 | x3 ⇒ match e2 with
1003 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
1004 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
1005 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
1006 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
1007 | x4 ⇒ match e2 with
1008 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
1009 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
1010 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
1011 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
1012 | x5 ⇒ match e2 with
1013 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
1014 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
1015 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
1016 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
1017 | x6 ⇒ match e2 with
1018 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
1019 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
1020 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
1021 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
1022 | x7 ⇒ match e2 with
1023 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
1024 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
1025 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
1026 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
1027 | x8 ⇒ match e2 with
1028 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
1029 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
1030 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
1031 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
1032 | x9 ⇒ match e2 with
1033 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
1034 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
1035 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
1036 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
1037 | xA ⇒ match e2 with
1038 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
1039 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
1040 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
1041 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
1042 | xB ⇒ match e2 with
1043 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
1044 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
1045 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
1046 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
1047 | xC ⇒ match e2 with
1048 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
1049 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
1050 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
1051 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
1052 | xD ⇒ match e2 with
1053 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
1054 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
1055 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
1056 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
1057 | xE ⇒ match e2 with
1058 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
1059 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
1060 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
1061 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
1062 | xF ⇒ match e2 with
1063 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
1064 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
1065 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
1066 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
1069 (* operatore somma con data+carry → data *)
1070 ndefinition plus_ex_dc_d ≝
1071 λc:bool.λe1,e2:exadecim.
1073 [ true ⇒ match e1 with
1074 [ x0 ⇒ match e2 with
1075 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1076 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1077 | x1 ⇒ match e2 with
1078 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1079 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1080 | x2 ⇒ match e2 with
1081 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1082 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1083 | x3 ⇒ match e2 with
1084 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1085 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1086 | x4 ⇒ match e2 with
1087 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1088 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1089 | x5 ⇒ match e2 with
1090 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1091 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1092 | x6 ⇒ match e2 with
1093 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1094 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1095 | x7 ⇒ match e2 with
1096 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1097 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1098 | x8 ⇒ match e2 with
1099 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1100 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1101 | x9 ⇒ match e2 with
1102 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1103 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1104 | xA ⇒ match e2 with
1105 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1106 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1107 | xB ⇒ match e2 with
1108 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1109 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1110 | xC ⇒ match e2 with
1111 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1112 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1113 | xD ⇒ match e2 with
1114 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1115 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1116 | xE ⇒ match e2 with
1117 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1118 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1119 | xF ⇒ match e2 with
1120 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1121 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1123 | false ⇒ match e1 with
1124 [ x0 ⇒ match e2 with
1125 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1126 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1127 | x1 ⇒ match e2 with
1128 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1129 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1130 | x2 ⇒ match e2 with
1131 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1132 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1133 | x3 ⇒ match e2 with
1134 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1135 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1136 | x4 ⇒ match e2 with
1137 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1138 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1139 | x5 ⇒ match e2 with
1140 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1141 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1142 | x6 ⇒ match e2 with
1143 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1144 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1145 | x7 ⇒ match e2 with
1146 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1147 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1148 | x8 ⇒ match e2 with
1149 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1150 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1151 | x9 ⇒ match e2 with
1152 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1153 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1154 | xA ⇒ match e2 with
1155 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1156 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1157 | xB ⇒ match e2 with
1158 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1159 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1160 | xC ⇒ match e2 with
1161 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1162 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1163 | xD ⇒ match e2 with
1164 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1165 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1166 | xE ⇒ match e2 with
1167 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1168 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1169 | xF ⇒ match e2 with
1170 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1171 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1174 (* operatore somma con data → data *)
1175 ndefinition plus_ex_d_d ≝
1178 [ x0 ⇒ match e2 with
1179 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1180 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1181 | x1 ⇒ match e2 with
1182 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1183 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1184 | x2 ⇒ match e2 with
1185 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1186 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1187 | x3 ⇒ match e2 with
1188 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1189 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1190 | x4 ⇒ match e2 with
1191 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1192 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1193 | x5 ⇒ match e2 with
1194 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1195 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1196 | x6 ⇒ match e2 with
1197 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1198 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1199 | x7 ⇒ match e2 with
1200 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1201 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1202 | x8 ⇒ match e2 with
1203 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1204 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1205 | x9 ⇒ match e2 with
1206 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1207 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1208 | xA ⇒ match e2 with
1209 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1210 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1211 | xB ⇒ match e2 with
1212 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1213 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1214 | xC ⇒ match e2 with
1215 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1216 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1217 | xD ⇒ match e2 with
1218 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1219 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1220 | xE ⇒ match e2 with
1221 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1222 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1223 | xF ⇒ match e2 with
1224 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1225 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1228 (* operatore somma con data+carry → carry *)
1229 ndefinition plus_ex_dc_c ≝
1230 λc:bool.λe1,e2:exadecim.
1232 [ true ⇒ match e1 with
1233 [ x0 ⇒ match e2 with
1234 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1235 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1236 | x1 ⇒ match e2 with
1237 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1238 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1239 | x2 ⇒ match e2 with
1240 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1241 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1242 | x3 ⇒ match e2 with
1243 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1244 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1245 | x4 ⇒ match e2 with
1246 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1247 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1248 | x5 ⇒ match e2 with
1249 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1250 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1251 | x6 ⇒ match e2 with
1252 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1253 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1254 | x7 ⇒ match e2 with
1255 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1256 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1257 | x8 ⇒ match e2 with
1258 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1259 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1260 | x9 ⇒ match e2 with
1261 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1262 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1263 | xA ⇒ match e2 with
1264 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1265 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1266 | xB ⇒ match e2 with
1267 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1268 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1269 | xC ⇒ match e2 with
1270 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1271 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1272 | xD ⇒ match e2 with
1273 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1274 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1275 | xE ⇒ match e2 with
1276 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1277 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1278 | xF ⇒ match e2 with
1279 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1280 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1282 | false ⇒ match e1 with
1283 [ x0 ⇒ match e2 with
1284 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1285 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1286 | x1 ⇒ match e2 with
1287 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1288 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1289 | x2 ⇒ match e2 with
1290 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1291 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1292 | x3 ⇒ match e2 with
1293 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1294 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1295 | x4 ⇒ match e2 with
1296 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1297 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1298 | x5 ⇒ match e2 with
1299 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1300 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1301 | x6 ⇒ match e2 with
1302 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1303 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1304 | x7 ⇒ match e2 with
1305 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1306 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1307 | x8 ⇒ match e2 with
1308 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1309 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1310 | x9 ⇒ match e2 with
1311 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1312 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1313 | xA ⇒ match e2 with
1314 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1315 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1316 | xB ⇒ match e2 with
1317 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1318 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1319 | xC ⇒ match e2 with
1320 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1321 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1322 | xD ⇒ match e2 with
1323 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1324 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1325 | xE ⇒ match e2 with
1326 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1327 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1328 | xF ⇒ match e2 with
1329 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1330 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1333 (* operatore somma con data → carry *)
1334 ndefinition plus_ex_d_c ≝
1337 [ x0 ⇒ match e2 with
1338 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1339 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1340 | x1 ⇒ match e2 with
1341 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1342 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1343 | x2 ⇒ match e2 with
1344 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1345 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1346 | x3 ⇒ match e2 with
1347 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1348 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1349 | x4 ⇒ match e2 with
1350 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1351 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1352 | x5 ⇒ match e2 with
1353 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1354 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1355 | x6 ⇒ match e2 with
1356 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1357 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1358 | x7 ⇒ match e2 with
1359 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1360 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1361 | x8 ⇒ match e2 with
1362 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1363 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1364 | x9 ⇒ match e2 with
1365 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1366 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1367 | xA ⇒ match e2 with
1368 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1369 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1370 | xB ⇒ match e2 with
1371 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1372 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1373 | xC ⇒ match e2 with
1374 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1375 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1376 | xD ⇒ match e2 with
1377 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1378 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1379 | xE ⇒ match e2 with
1380 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1381 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1382 | xF ⇒ match e2 with
1383 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1384 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1387 (* operatore predecessore *)
1388 ndefinition pred_ex ≝
1391 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1392 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1394 (* operatore successore *)
1395 ndefinition succ_ex ≝
1398 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1399 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1401 (* operatore neg/complemento a 2 *)
1402 ndefinition compl_ex ≝
1403 λe:exadecim.match e with
1404 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1405 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1406 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1407 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1410 ndefinition abs_ex ≝
1411 λe:exadecim.match getMSB_ex e with
1412 [ true ⇒ compl_ex e | false ⇒ e ].
1414 (* operatore x in [inf,sup] o in sup],[inf *)
1415 ndefinition inrange_ex ≝
1416 λx,inf,sup:exadecim.
1417 match le_ex inf sup with
1418 [ true ⇒ and_bool | false ⇒ or_bool ]
1419 (le_ex inf x) (le_ex x sup).
1421 (* esadecimali ricorsivi *)
1422 ninductive rec_exadecim : exadecim → Type ≝
1423 ex_O : rec_exadecim x0
1424 | ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
1426 (* esadecimali → esadecimali ricorsivi *)
1427 ndefinition ex_to_recex ≝
1428 λn.match n return λx.rec_exadecim x with
1431 | x2 ⇒ ex_S ? (ex_S ? ex_O)
1432 | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
1433 | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
1434 | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
1435 | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
1436 | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
1437 | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
1438 | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
1439 | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
1440 | 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))))))))))
1441 | 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)))))))))))
1442 | 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))))))))))))
1443 | 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)))))))))))))
1444 | 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))))))))))))))
1447 (* quaternari → esadecimali *)
1448 ndefinition ex_of_qu ≝
1450 [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
1452 (* ottali → esadecimali *)
1453 ndefinition ex_of_oct ≝
1455 [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
1457 (* esadecimali xNNNN → ottali *)
1458 ndefinition oct_of_exL ≝
1460 [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
1461 | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
1463 (* esadecimali NNNNx → ottali *)
1464 ndefinition oct_of_exH ≝
1466 [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3
1467 | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ].