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/comp_ext.ma".
24 include "num/bool_lemmas.ma".
31 ninductive exadecim : Type ≝
49 (* iteratore sugli esadecimali *)
50 ndefinition forall_ex ≝ λP.
51 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
52 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
58 [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
59 | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
60 | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
61 | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
62 | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
63 | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
64 | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
65 | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
66 | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
67 | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
68 | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
69 | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
70 | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
71 | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
72 | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
73 | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
81 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
82 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
83 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
84 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
86 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
87 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
88 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
89 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
91 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
92 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
93 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
94 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
96 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
97 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
98 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
99 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
101 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
102 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
103 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
104 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
106 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
107 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
108 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
109 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
111 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
112 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
113 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
114 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
116 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
117 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
118 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
119 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
121 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
122 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
123 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
124 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
126 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
127 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
128 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
129 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
131 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
132 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
133 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
134 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
136 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
137 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
138 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
139 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
141 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
142 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
143 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
144 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
146 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
147 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
148 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
149 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
151 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
152 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
153 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
154 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
156 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
157 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
158 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
159 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
167 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
168 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
169 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
170 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
172 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
173 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
174 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
175 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
177 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
178 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
179 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
180 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
182 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
183 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
184 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
185 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
187 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
188 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
189 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
190 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
192 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
193 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
194 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
195 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
197 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
198 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
199 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
200 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
202 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
203 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
204 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
205 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
207 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
208 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
209 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
210 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
212 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
213 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
214 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
215 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
217 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
218 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
219 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
220 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
222 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
223 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
224 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
225 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
227 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
228 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
229 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
230 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
232 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
233 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
234 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
235 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
237 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
238 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
239 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
240 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
242 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
243 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
244 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
245 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
253 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
254 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
255 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
256 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
258 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
259 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
260 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
261 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
263 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
264 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
265 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
266 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
268 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
269 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
270 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
271 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
273 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
274 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
275 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
276 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
278 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
279 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
280 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
281 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
283 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
284 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
285 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
286 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
288 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
289 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
290 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
291 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
293 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
294 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
295 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
296 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
298 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
299 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
300 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
301 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
303 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
304 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
305 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
306 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
308 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
309 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
310 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
311 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
313 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
314 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
315 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
316 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
318 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
319 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
320 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
321 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
323 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
324 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
325 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
326 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
328 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
329 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
330 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
331 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
339 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
340 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
341 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
342 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
344 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
345 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
346 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
347 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
349 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
350 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
351 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
352 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
354 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
355 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
356 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
357 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
359 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
360 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
361 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
362 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
364 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
365 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
366 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
367 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
369 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
370 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
371 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
372 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
374 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
375 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
376 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
377 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
379 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
380 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
381 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
382 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
384 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
385 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
386 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
387 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
389 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
390 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
391 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
392 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
394 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
395 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
396 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
397 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
399 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
400 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
401 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
402 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
404 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
405 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
406 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
407 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
409 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
410 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
411 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
412 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
414 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
415 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
416 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
417 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
422 λe1,e2:exadecim.match e1 with
424 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
425 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
426 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
427 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
429 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
430 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
431 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
432 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
434 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
435 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
436 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
437 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
439 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
440 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
441 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
442 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
444 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
445 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
446 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
447 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
449 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
450 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
451 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
452 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
454 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
455 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
456 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
457 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
459 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
460 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
461 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
462 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
464 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
465 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
466 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
467 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
469 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
470 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
471 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
472 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
474 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
475 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
476 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
477 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
479 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
480 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
481 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
482 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
484 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
485 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
486 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
487 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
489 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
490 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
491 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
492 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
494 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
495 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
496 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
497 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
499 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
500 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
501 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
502 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
507 λe1,e2:exadecim.match e1 with
509 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
510 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
511 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
512 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
514 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
515 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
516 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
517 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
519 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
520 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
521 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
522 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
524 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
525 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
526 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
527 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
529 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
530 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
531 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
532 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
534 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
535 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
536 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
537 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
539 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
540 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
541 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
542 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
544 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
545 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
546 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
547 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
549 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
550 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
551 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
552 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
554 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
555 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
556 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
557 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
559 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
560 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
561 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
562 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
564 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
565 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
566 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
567 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
569 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
570 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
571 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
572 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
574 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
575 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
576 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
577 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
579 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
580 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
581 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
582 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
584 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
585 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
586 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
587 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
592 λe1,e2:exadecim.match e1 with
594 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
595 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
596 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
597 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
599 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
600 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
601 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
602 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
604 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
605 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
606 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
607 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
609 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
610 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
611 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
612 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
614 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
615 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
616 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
617 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
619 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
620 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
621 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
622 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
624 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
625 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
626 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
627 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
629 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
630 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
631 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
632 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
634 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
635 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
636 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
637 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
639 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
640 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
641 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
642 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
644 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
645 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
646 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
647 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
649 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
650 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
651 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
652 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
654 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
655 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
656 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
657 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
659 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
660 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
661 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
662 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
664 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
665 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
666 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
667 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
669 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
670 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
671 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
672 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
675 (* operatore Most Significant Bit *)
676 ndefinition getMSB_ex ≝
677 λe:exadecim.match e with
678 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
679 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
680 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
681 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
683 ndefinition setMSB_ex ≝
684 λe:exadecim.match e with
685 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
686 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
687 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
688 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ].
690 ndefinition clrMSB_ex ≝
691 λe:exadecim.match e with
692 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
693 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
694 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
695 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ].
697 (* operatore Least Significant Bit *)
698 ndefinition getLSB_ex ≝
699 λe:exadecim.match e with
700 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true
701 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true
702 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true
703 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ].
705 ndefinition setLSB_ex ≝
706 λe:exadecim.match e with
707 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
708 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
709 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
710 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
712 ndefinition clrLSB_ex ≝
713 λe:exadecim.match e with
714 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
715 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
716 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
717 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ].
719 (* operatore rotazione destra con carry *)
721 λc:bool.λe:exadecim.match c with
722 [ true ⇒ match e with
723 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … true x8
724 | x2 ⇒ pair … false x9 | x3 ⇒ pair … true x9
725 | x4 ⇒ pair … false xA | x5 ⇒ pair … true xA
726 | x6 ⇒ pair … false xB | x7 ⇒ pair … true xB
727 | x8 ⇒ pair … false xC | x9 ⇒ pair … true xC
728 | xA ⇒ pair … false xD | xB ⇒ pair … true xD
729 | xC ⇒ pair … false xE | xD ⇒ pair … true xE
730 | xE ⇒ pair … false xF | xF ⇒ pair … true xF ]
731 | false ⇒ 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 ]
742 (* operatore shift destro *)
744 λe:exadecim.match e with
745 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
746 | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
747 | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
748 | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
749 | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
750 | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
751 | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
752 | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ].
754 (* operatore rotazione destra *)
756 λe:exadecim.match e with
757 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
758 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
759 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
760 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
762 (* operatore rotazione sinistra con carry *)
764 λc:bool.λe:exadecim.match c with
765 [ true ⇒ match e with
766 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x3
767 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x7
768 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xB
769 | x6 ⇒ pair … false xD | x7 ⇒ pair … false xF
770 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x3
771 | xA ⇒ pair … true x5 | xB ⇒ pair … true x7
772 | xC ⇒ pair … true x9 | xD ⇒ pair … true xB
773 | xE ⇒ pair … true xD | xF ⇒ pair … true xF ]
774 | false ⇒ 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 ]
785 (* operatore shift sinistro *)
787 λe:exadecim.match e with
788 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
789 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
790 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
791 | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
792 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2
793 | xA ⇒ pair … true x4 | xB ⇒ pair … true x6
794 | xC ⇒ pair … true x8 | xD ⇒ pair … true xA
795 | xE ⇒ pair … true xC | xF ⇒ pair … true xE ].
797 (* operatore rotazione sinistra *)
799 λe:exadecim.match e with
800 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
801 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
802 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
803 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
805 (* operatore not/complemento a 1 *)
807 λe:exadecim.match e with
808 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
809 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
810 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
811 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
813 (* operatore somma con data+carry → data+carry *)
814 ndefinition plus_ex_dc_dc ≝
815 λc:bool.λe1,e2:exadecim.
817 [ true ⇒ match e1 with
819 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
820 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
821 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
822 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
824 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
825 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
826 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
827 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
829 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
830 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
831 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
832 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
834 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
835 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
836 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
837 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
839 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
840 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
841 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
842 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
844 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
845 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
846 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
847 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
849 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
850 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
851 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
852 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
854 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
855 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
856 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
857 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
859 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
860 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
861 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
862 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
864 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
865 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
866 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
867 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
869 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
870 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
871 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
872 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
874 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
875 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
876 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
877 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
879 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
880 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
881 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
882 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
884 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
885 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
886 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
887 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
889 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
890 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
891 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
892 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
894 [ x0 ⇒ pair … true x0 | x1 ⇒ pair … true x1 | x2 ⇒ pair … true x2 | x3 ⇒ pair … true x3
895 | x4 ⇒ pair … true x4 | x5 ⇒ pair … true x5 | x6 ⇒ pair … true x6 | x7 ⇒ pair … true x7
896 | x8 ⇒ pair … true x8 | x9 ⇒ pair … true x9 | xA ⇒ pair … true xA | xB ⇒ pair … true xB
897 | xC ⇒ pair … true xC | xD ⇒ pair … true xD | xE ⇒ pair … true xE | xF ⇒ pair … true xF ]
899 | false ⇒ match e1 with
901 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
902 | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
903 | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
904 | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]
906 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
907 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
908 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
909 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
911 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
912 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
913 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
914 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
916 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
917 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
918 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
919 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
921 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
922 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
923 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
924 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
926 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
927 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
928 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
929 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
931 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
932 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
933 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
934 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
936 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
937 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
938 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
939 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
941 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
942 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
943 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
944 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
946 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
947 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
948 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
949 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
951 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
952 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
953 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
954 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
956 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
957 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
958 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
959 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
961 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
962 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
963 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
964 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
966 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
967 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
968 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
969 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
971 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
972 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
973 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
974 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
976 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
977 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
978 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
979 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
982 (* operatore somma con data → data+carry *)
983 ndefinition plus_ex_d_dc ≝
987 [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
988 | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
989 | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
990 | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]
992 [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
993 | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
994 | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
995 | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ]
997 [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
998 | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
999 | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
1000 | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ]
1001 | x3 ⇒ match e2 with
1002 [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
1003 | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
1004 | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
1005 | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ]
1006 | x4 ⇒ match e2 with
1007 [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
1008 | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
1009 | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
1010 | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ]
1011 | x5 ⇒ match e2 with
1012 [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
1013 | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
1014 | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
1015 | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ]
1016 | x6 ⇒ match e2 with
1017 [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
1018 | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
1019 | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1
1020 | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ]
1021 | x7 ⇒ match e2 with
1022 [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
1023 | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
1024 | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2
1025 | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ]
1026 | x8 ⇒ match e2 with
1027 [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
1028 | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
1029 | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3
1030 | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ]
1031 | x9 ⇒ match e2 with
1032 [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
1033 | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
1034 | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4
1035 | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ]
1036 | xA ⇒ match e2 with
1037 [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
1038 | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1
1039 | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5
1040 | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ]
1041 | xB ⇒ match e2 with
1042 [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
1043 | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2
1044 | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6
1045 | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ]
1046 | xC ⇒ match e2 with
1047 [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
1048 | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3
1049 | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7
1050 | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ]
1051 | xD ⇒ match e2 with
1052 [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
1053 | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4
1054 | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8
1055 | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ]
1056 | xE ⇒ match e2 with
1057 [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1
1058 | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5
1059 | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9
1060 | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ]
1061 | xF ⇒ match e2 with
1062 [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2
1063 | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6
1064 | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA
1065 | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ]
1068 (* operatore somma con data+carry → data *)
1069 ndefinition plus_ex_dc_d ≝
1070 λc:bool.λe1,e2:exadecim.
1072 [ true ⇒ match e1 with
1073 [ x0 ⇒ match e2 with
1074 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1075 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1076 | x1 ⇒ match e2 with
1077 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1078 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1079 | x2 ⇒ match e2 with
1080 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1081 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1082 | x3 ⇒ match e2 with
1083 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1084 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1085 | x4 ⇒ match e2 with
1086 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1087 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1088 | x5 ⇒ match e2 with
1089 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1090 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1091 | x6 ⇒ match e2 with
1092 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1093 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1094 | x7 ⇒ match e2 with
1095 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1096 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1097 | x8 ⇒ match e2 with
1098 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1099 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1100 | x9 ⇒ match e2 with
1101 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1102 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1103 | xA ⇒ match e2 with
1104 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1105 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1106 | xB ⇒ match e2 with
1107 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1108 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1109 | xC ⇒ match e2 with
1110 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1111 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1112 | xD ⇒ match e2 with
1113 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1114 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1115 | xE ⇒ match e2 with
1116 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1117 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1118 | xF ⇒ match e2 with
1119 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1120 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1122 | false ⇒ match e1 with
1123 [ x0 ⇒ match e2 with
1124 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1125 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1126 | x1 ⇒ match e2 with
1127 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1128 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1129 | x2 ⇒ match e2 with
1130 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1131 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1132 | x3 ⇒ match e2 with
1133 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1134 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1135 | x4 ⇒ match e2 with
1136 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1137 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1138 | x5 ⇒ match e2 with
1139 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1140 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1141 | x6 ⇒ match e2 with
1142 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1143 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1144 | x7 ⇒ match e2 with
1145 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1146 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1147 | x8 ⇒ match e2 with
1148 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1149 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1150 | x9 ⇒ match e2 with
1151 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1152 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1153 | xA ⇒ match e2 with
1154 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1155 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1156 | xB ⇒ match e2 with
1157 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1158 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1159 | xC ⇒ match e2 with
1160 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1161 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1162 | xD ⇒ match e2 with
1163 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1164 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1165 | xE ⇒ match e2 with
1166 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1167 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1168 | xF ⇒ match e2 with
1169 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1170 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1173 (* operatore somma con data → data *)
1174 ndefinition plus_ex_d_d ≝
1177 [ x0 ⇒ match e2 with
1178 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1179 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1180 | x1 ⇒ match e2 with
1181 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1182 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1183 | x2 ⇒ match e2 with
1184 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1185 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1186 | x3 ⇒ match e2 with
1187 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1188 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1189 | x4 ⇒ match e2 with
1190 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1191 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1192 | x5 ⇒ match e2 with
1193 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1194 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1195 | x6 ⇒ match e2 with
1196 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1197 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1198 | x7 ⇒ match e2 with
1199 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1200 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1201 | x8 ⇒ match e2 with
1202 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1203 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1204 | x9 ⇒ match e2 with
1205 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1206 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1207 | xA ⇒ match e2 with
1208 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1209 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1210 | xB ⇒ match e2 with
1211 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1212 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1213 | xC ⇒ match e2 with
1214 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1215 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1216 | xD ⇒ match e2 with
1217 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1218 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1219 | xE ⇒ match e2 with
1220 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1221 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1222 | xF ⇒ match e2 with
1223 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1224 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1227 (* operatore somma con data+carry → carry *)
1228 ndefinition plus_ex_dc_c ≝
1229 λc:bool.λe1,e2:exadecim.
1231 [ true ⇒ match e1 with
1232 [ x0 ⇒ match e2 with
1233 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1234 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1235 | x1 ⇒ match e2 with
1236 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1237 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1238 | x2 ⇒ match e2 with
1239 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1240 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1241 | x3 ⇒ match e2 with
1242 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1243 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1244 | x4 ⇒ match e2 with
1245 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1246 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1247 | x5 ⇒ match e2 with
1248 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1249 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1250 | x6 ⇒ match e2 with
1251 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1252 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1253 | x7 ⇒ match e2 with
1254 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1255 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1256 | x8 ⇒ match e2 with
1257 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1258 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1259 | x9 ⇒ match e2 with
1260 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1261 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1262 | xA ⇒ match e2 with
1263 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1264 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1265 | xB ⇒ match e2 with
1266 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1267 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1268 | xC ⇒ match e2 with
1269 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1270 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1271 | xD ⇒ match e2 with
1272 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1273 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1274 | xE ⇒ match e2 with
1275 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1276 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1277 | xF ⇒ match e2 with
1278 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1279 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1281 | false ⇒ match e1 with
1282 [ x0 ⇒ match e2 with
1283 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1284 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1285 | x1 ⇒ match e2 with
1286 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1287 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1288 | x2 ⇒ match e2 with
1289 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1290 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1291 | x3 ⇒ match e2 with
1292 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1293 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1294 | x4 ⇒ match e2 with
1295 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1296 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1297 | x5 ⇒ match e2 with
1298 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1299 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1300 | x6 ⇒ match e2 with
1301 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1302 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1303 | x7 ⇒ match e2 with
1304 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1305 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1306 | x8 ⇒ match e2 with
1307 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1308 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1309 | x9 ⇒ match e2 with
1310 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1311 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1312 | xA ⇒ match e2 with
1313 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1314 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1315 | xB ⇒ match e2 with
1316 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1317 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1318 | xC ⇒ match e2 with
1319 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1320 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1321 | xD ⇒ match e2 with
1322 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1323 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1324 | xE ⇒ match e2 with
1325 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1326 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1327 | xF ⇒ match e2 with
1328 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1329 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1332 (* operatore somma con data → carry *)
1333 ndefinition plus_ex_d_c ≝
1336 [ x0 ⇒ match e2 with
1337 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1338 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1339 | x1 ⇒ match e2 with
1340 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1341 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1342 | x2 ⇒ match e2 with
1343 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1344 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1345 | x3 ⇒ match e2 with
1346 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1347 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1348 | x4 ⇒ match e2 with
1349 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1350 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1351 | x5 ⇒ match e2 with
1352 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1353 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1354 | x6 ⇒ match e2 with
1355 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1356 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1357 | x7 ⇒ match e2 with
1358 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1359 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1360 | x8 ⇒ match e2 with
1361 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1362 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1363 | x9 ⇒ match e2 with
1364 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1365 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1366 | xA ⇒ match e2 with
1367 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1368 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1369 | xB ⇒ match e2 with
1370 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1371 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1372 | xC ⇒ match e2 with
1373 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1374 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1375 | xD ⇒ match e2 with
1376 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1377 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1378 | xE ⇒ match e2 with
1379 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1380 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1381 | xF ⇒ match e2 with
1382 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1383 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1386 (* operatore predecessore *)
1387 ndefinition pred_ex ≝
1390 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2
1391 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1392 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA
1393 | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1395 (* operatore successore *)
1396 ndefinition succ_ex ≝
1399 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4
1400 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1401 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC
1402 | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1404 (* operatore neg/complemento a 2 *)
1405 ndefinition compl_ex ≝
1406 λe:exadecim.match e with
1407 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1408 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1409 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1410 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1413 ndefinition abs_ex ≝
1414 λe:exadecim.match getMSB_ex e with
1415 [ true ⇒ compl_ex e | false ⇒ e ].
1417 (* operatore x in [inf,sup] o in sup],[inf *)
1418 ndefinition inrange_ex ≝
1419 λx,inf,sup:exadecim.
1420 match le_ex inf sup with
1421 [ true ⇒ and_bool | false ⇒ or_bool ]
1422 (le_ex inf x) (le_ex x sup).
1424 (* esadecimali ricorsivi *)
1425 ninductive rec_exadecim : exadecim → Type ≝
1426 ex_O : rec_exadecim x0
1427 | ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
1429 (* esadecimali → esadecimali ricorsivi *)
1430 ndefinition ex_to_recex ≝
1431 λn.match n return λx.rec_exadecim x with
1434 | x2 ⇒ ex_S ? (ex_S ? ex_O)
1435 | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
1436 | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
1437 | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
1438 | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
1439 | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
1440 | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
1441 | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
1442 | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
1443 | 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))))))))))
1444 | 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)))))))))))
1445 | 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))))))))))))
1446 | 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)))))))))))))
1447 | 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))))))))))))))
1450 (* ottali → esadecimali *)
1451 ndefinition ex_of_oct ≝
1453 [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
1455 (* esadecimali xNNNN → ottali *)
1456 ndefinition oct_of_exL ≝
1458 [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
1459 | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
1461 (* esadecimali NNNNx → ottali *)
1462 ndefinition oct_of_exH ≝
1464 [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3
1465 | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ].
1467 ndefinition exadecim_destruct_aux ≝
1468 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
1469 match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
1471 ndefinition exadecim_destruct : exadecim_destruct_aux.
1479 nlemma eq_to_eqex : ∀n1,n2.n1 = n2 → eq_ex n1 n2 = true.
1487 nlemma neqex_to_neq : ∀n1,n2.eq_ex n1 n2 = false → n1 ≠ n2.
1489 napply (not_to_not (n1 = n2) (eq_ex n1 n2 = true) …);
1490 ##[ ##1: napply (eq_to_eqex n1 n2)
1491 ##| ##2: napply (eqfalse_to_neqtrue … H)
1495 nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2.
1500 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
1501 ##| ##*: #H; (*ndestruct lentissima...*) napply (bool_destruct … H)
1505 nlemma neq_to_neqex : ∀n1,n2.n1 ≠ n2 → eq_ex n1 n2 = false.
1507 napply (neqtrue_to_eqfalse (eq_ex n1 n2));
1508 napply (not_to_not (eq_ex n1 n2 = true) (n1 = n2) ? H);
1509 napply (eqex_to_eq n1 n2).
1512 nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
1514 napply (or2_elim (eq_ex x y = true) (eq_ex x y = false) ? (decidable_bexpr ?));
1515 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqex_to_eq … H))
1516 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqex_to_neq … H))
1520 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
1522 napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_ex n1 n2));
1523 ##[ ##1: #H; nrewrite > H; napply refl_eq
1524 ##| ##2: #H; nrewrite > (neq_to_neqex n1 n2 H);
1525 napply (symmetric_eq ? (eq_ex n2 n1) false);
1526 napply (neq_to_neqex n2 n1 (symmetric_neq ? n1 n2 H))
1530 nlemma exadecim_is_comparable : comparable.
1533 ##| napply forall_ex
1535 ##| napply eqex_to_eq
1536 ##| napply eq_to_eqex
1537 ##| napply neqex_to_neq
1538 ##| napply neq_to_neqex
1539 ##| napply decidable_ex
1540 ##| napply symmetric_eqex
1544 unification hint 0 ≔ ⊢ carr exadecim_is_comparable ≡ exadecim.
1546 nlemma exadecim_is_comparable_ext : comparable_ext.
1547 napply mk_comparable_ext;
1548 ##[ napply exadecim_is_comparable
1556 ##| napply getMSB_ex
1557 ##| napply setMSB_ex
1558 ##| napply clrMSB_ex
1559 ##| napply getLSB_ex
1560 ##| napply setLSB_ex
1561 ##| napply clrLSB_ex
1569 ##| napply plus_ex_dc_dc
1570 ##| napply plus_ex_d_dc
1571 ##| napply plus_ex_dc_d
1572 ##| napply plus_ex_d_d
1573 ##| napply plus_ex_dc_c
1574 ##| napply plus_ex_d_c
1579 ##| napply inrange_ex
1583 unification hint 0 ≔ ⊢ carr (comp_base exadecim_is_comparable_ext) ≡ exadecim.