1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/bool.ma".
24 include "freescale/prod.ma".
25 include "freescale/nat.ma".
31 ninductive exadecim : Type ≝
49 ndefinition exadecim_ind :
50 ΠP:exadecim → Prop.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
51 P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
53 λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
54 λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
56 [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
57 | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].
59 ndefinition exadecim_rec :
60 ΠP:exadecim → Set.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
61 P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
63 λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
64 λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
66 [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
67 | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].
69 ndefinition exadecim_rect :
70 ΠP:exadecim → Type.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
71 P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
73 λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
74 λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
76 [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
77 | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].
84 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
85 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
86 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
87 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
89 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
90 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
91 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
92 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
94 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
95 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
96 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
97 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
99 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
100 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
101 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
102 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
104 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
105 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
106 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
107 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
109 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
110 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
111 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
112 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
114 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
115 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
116 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
117 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
119 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
120 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
121 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
122 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
124 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
125 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
126 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
127 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
129 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
130 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
131 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
132 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
134 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
135 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
136 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
137 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
139 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
140 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
141 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
142 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
144 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
145 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
146 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
147 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
149 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
150 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
151 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
152 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
154 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
155 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
156 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
157 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
159 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
160 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
161 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
162 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
170 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
171 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
172 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
173 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
175 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
176 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
177 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
178 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
180 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
181 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
182 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
183 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
185 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
186 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
187 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
188 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
190 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
191 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
192 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
193 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
195 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
196 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
197 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
198 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
200 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
201 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
202 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
203 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
205 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
206 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
207 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
208 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
210 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
211 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
212 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
213 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
215 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
216 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
217 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
218 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
220 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
221 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
222 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
223 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
225 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
226 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
227 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
228 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
230 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
231 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
232 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
233 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
235 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
236 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
237 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
238 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
240 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
241 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
242 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
243 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
245 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
246 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
247 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
248 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
256 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
257 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
258 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
259 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
261 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
262 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
263 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
264 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
266 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
267 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
268 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
269 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
271 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
272 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
273 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
274 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
276 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
277 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
278 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
279 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
281 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
282 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
283 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
284 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
286 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
287 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
288 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
289 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
291 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
292 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
293 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
294 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
296 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
297 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
298 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
299 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
301 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
302 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
303 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
304 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
306 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
307 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
308 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
309 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
311 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
312 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
313 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
314 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
316 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
317 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
318 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
319 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
321 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
322 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
323 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
324 | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
326 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
327 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
328 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
329 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
331 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
332 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
333 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
334 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
342 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
343 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
344 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
345 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
347 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
348 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
349 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
350 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
352 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
353 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
354 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
355 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
357 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
358 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
359 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
360 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
362 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
363 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
364 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
365 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
367 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
368 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
369 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
370 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
372 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
373 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
374 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
375 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
377 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
378 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
379 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
380 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
382 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
383 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
384 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
385 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
387 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
388 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
389 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
390 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
392 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
393 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
394 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
395 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
397 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
398 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
399 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
400 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
402 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
403 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
404 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
405 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
407 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
408 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
409 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
410 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
412 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
413 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
414 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
415 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
417 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
418 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
419 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
420 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
428 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
429 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
430 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
431 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
433 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
434 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
435 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
436 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
438 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
439 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
440 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
441 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
443 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
444 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
445 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
446 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
448 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
449 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
450 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
451 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
453 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
454 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
455 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
456 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
458 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
459 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
460 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
461 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
463 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
464 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
465 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
466 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
468 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
469 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
470 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
471 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
473 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
474 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
475 | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
476 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
478 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
479 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
480 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
481 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
483 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
484 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
485 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
486 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
488 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
489 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
490 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
491 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
493 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
494 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
495 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
496 | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
498 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
499 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
500 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
501 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
503 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
504 | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
505 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
506 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
511 λe1,e2:exadecim.match e1 with
513 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
514 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
515 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
516 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
518 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
519 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
520 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
521 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
523 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
524 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
525 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
526 | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
528 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
529 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
530 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
531 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
533 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
534 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
535 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
536 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
538 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
539 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
540 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
541 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
543 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
544 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
545 | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
546 | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
548 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
549 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
550 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
551 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
553 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
554 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
555 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
556 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
558 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
559 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
560 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
561 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
563 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
564 | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
565 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
566 | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
568 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
569 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
570 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
571 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
573 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
574 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
575 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
576 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
578 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
579 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
580 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
581 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
583 [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
584 | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
585 | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
586 | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
588 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
589 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
590 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
591 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
596 λe1,e2:exadecim.match e1 with
598 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
599 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
600 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
601 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
603 [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
604 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
605 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
606 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
608 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
609 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
610 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
611 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
613 [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
614 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
615 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
616 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
618 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
619 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
620 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
621 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
623 [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
624 | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
625 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
626 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
628 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
629 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
630 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
631 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
633 [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
634 | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
635 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
636 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
638 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
639 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
640 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
641 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
643 [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
644 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
645 | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
646 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
648 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
649 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
650 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
651 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
653 [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
654 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
655 | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
656 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
658 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
659 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
660 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
661 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
663 [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
664 | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
665 | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
666 | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
668 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
669 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
670 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
671 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
673 [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
674 | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
675 | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
676 | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
681 λe1,e2:exadecim.match e1 with
683 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
684 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
685 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
686 | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
688 [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
689 | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
690 | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
691 | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
693 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
694 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
695 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
696 | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
698 [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
699 | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
700 | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
701 | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
703 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
704 | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
705 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
706 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
708 [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
709 | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
710 | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
711 | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
713 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
714 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
715 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
716 | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
718 [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
719 | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
720 | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
721 | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
723 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
724 | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
725 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
726 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
728 [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
729 | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
730 | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
731 | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
733 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
734 | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
735 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
736 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
738 [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
739 | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
740 | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
741 | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
743 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
744 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
745 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
746 | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
748 [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
749 | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
750 | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
751 | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
753 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
754 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
755 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
756 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
758 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
759 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
760 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
761 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
764 (* operatore rotazione destra con carry *)
766 λe:exadecim.λc:bool.match c with
767 [ true ⇒ match e with
768 [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
769 | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
770 | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
771 | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
772 | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
773 | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
774 | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
775 | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
776 | false ⇒ match e with
777 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
778 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
779 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
780 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
781 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
782 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
783 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
784 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
787 (* operatore shift destro *)
789 λe:exadecim.match e with
790 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
791 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
792 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
793 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
794 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
795 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
796 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
797 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
799 (* operatore rotazione destra *)
801 λe:exadecim.match e with
802 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
803 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
804 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
805 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
807 (* operatore rotazione destra n-volte *)
808 nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
811 | S n' ⇒ ror_ex_n (ror_ex e) n' ].
813 (* operatore rotazione sinistra con carry *)
815 λe:exadecim.λc:bool.match c with
816 [ true ⇒ match e with
817 [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
818 | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
819 | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
820 | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
821 | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
822 | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
823 | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
824 | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
825 | false ⇒ match e with
826 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
827 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
828 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
829 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
830 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
831 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
832 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
833 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
836 (* operatore shift sinistro *)
838 λe:exadecim.match e with
839 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
840 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
841 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
842 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
843 | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
844 | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
845 | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
846 | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
848 (* operatore rotazione sinistra *)
850 λe:exadecim.match e with
851 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
852 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
853 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
854 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
856 (* operatore rotazione sinistra n-volte *)
857 nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
860 | S n' ⇒ rol_ex_n (rol_ex e) n' ].
862 (* operatore not/complemento a 1 *)
864 λe:exadecim.match e with
865 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
866 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
867 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
868 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
870 (* operatore somma con data+carry → data+carry *)
871 ndefinition plus_ex_dc_dc ≝
872 λe1,e2:exadecim.λc:bool.
874 [ true ⇒ match e1 with
876 [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
877 | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
878 | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
879 | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ]
881 [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
882 | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
883 | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
884 | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true | xF ⇒ pair ?? x1 true ]
886 [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
887 | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
888 | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
889 | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true | xE ⇒ pair ?? x1 true | xF ⇒ pair ?? x2 true ]
891 [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
892 | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
893 | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
894 | xC ⇒ pair ?? x0 true | xD ⇒ pair ?? x1 true | xE ⇒ pair ?? x2 true | xF ⇒ pair ?? x3 true ]
896 [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
897 | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
898 | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
899 | xC ⇒ pair ?? x1 true | xD ⇒ pair ?? x2 true | xE ⇒ pair ?? x3 true | xF ⇒ pair ?? x4 true ]
901 [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
902 | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
903 | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true | xB ⇒ pair ?? x1 true
904 | xC ⇒ pair ?? x2 true | xD ⇒ pair ?? x3 true | xE ⇒ pair ?? x4 true | xF ⇒ pair ?? x5 true ]
906 [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
907 | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
908 | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true | xA ⇒ pair ?? x1 true | xB ⇒ pair ?? x2 true
909 | xC ⇒ pair ?? x3 true | xD ⇒ pair ?? x4 true | xE ⇒ pair ?? x5 true | xF ⇒ pair ?? x6 true ]
911 [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
912 | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
913 | x8 ⇒ pair ?? x0 true | x9 ⇒ pair ?? x1 true | xA ⇒ pair ?? x2 true | xB ⇒ pair ?? x3 true
914 | xC ⇒ pair ?? x4 true | xD ⇒ pair ?? x5 true | xE ⇒ pair ?? x6 true | xF ⇒ pair ?? x7 true ]
916 [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
917 | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
918 | x8 ⇒ pair ?? x1 true | x9 ⇒ pair ?? x2 true | xA ⇒ pair ?? x3 true | xB ⇒ pair ?? x4 true
919 | xC ⇒ pair ?? x5 true | xD ⇒ pair ?? x6 true | xE ⇒ pair ?? x7 true | xF ⇒ pair ?? x8 true ]
921 [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
922 | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true | x7 ⇒ pair ?? x1 true
923 | x8 ⇒ pair ?? x2 true | x9 ⇒ pair ?? x3 true | xA ⇒ pair ?? x4 true | xB ⇒ pair ?? x5 true
924 | xC ⇒ pair ?? x6 true | xD ⇒ pair ?? x7 true | xE ⇒ pair ?? x8 true | xF ⇒ pair ?? x9 true ]
926 [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
927 | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true | x6 ⇒ pair ?? x1 true | x7 ⇒ pair ?? x2 true
928 | x8 ⇒ pair ?? x3 true | x9 ⇒ pair ?? x4 true | xA ⇒ pair ?? x5 true | xB ⇒ pair ?? x6 true
929 | xC ⇒ pair ?? x7 true | xD ⇒ pair ?? x8 true | xE ⇒ pair ?? x9 true | xF ⇒ pair ?? xA true ]
931 [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
932 | x4 ⇒ pair ?? x0 true | x5 ⇒ pair ?? x1 true | x6 ⇒ pair ?? x2 true | x7 ⇒ pair ?? x3 true
933 | x8 ⇒ pair ?? x4 true | x9 ⇒ pair ?? x5 true | xA ⇒ pair ?? x6 true | xB ⇒ pair ?? x7 true
934 | xC ⇒ pair ?? x8 true | xD ⇒ pair ?? x9 true | xE ⇒ pair ?? xA true | xF ⇒ pair ?? xB true ]
936 [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
937 | x4 ⇒ pair ?? x1 true | x5 ⇒ pair ?? x2 true | x6 ⇒ pair ?? x3 true | x7 ⇒ pair ?? x4 true
938 | x8 ⇒ pair ?? x5 true | x9 ⇒ pair ?? x6 true | xA ⇒ pair ?? x7 true | xB ⇒ pair ?? x8 true
939 | xC ⇒ pair ?? x9 true | xD ⇒ pair ?? xA true | xE ⇒ pair ?? xB true | xF ⇒ pair ?? xC true ]
941 [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true | x3 ⇒ pair ?? x1 true
942 | x4 ⇒ pair ?? x2 true | x5 ⇒ pair ?? x3 true | x6 ⇒ pair ?? x4 true | x7 ⇒ pair ?? x5 true
943 | x8 ⇒ pair ?? x6 true | x9 ⇒ pair ?? x7 true | xA ⇒ pair ?? x8 true | xB ⇒ pair ?? x9 true
944 | xC ⇒ pair ?? xA true | xD ⇒ pair ?? xB true | xE ⇒ pair ?? xC true | xF ⇒ pair ?? xD true ]
946 [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true | x2 ⇒ pair ?? x1 true | x3 ⇒ pair ?? x2 true
947 | x4 ⇒ pair ?? x3 true | x5 ⇒ pair ?? x4 true | x6 ⇒ pair ?? x5 true | x7 ⇒ pair ?? x6 true
948 | x8 ⇒ pair ?? x7 true | x9 ⇒ pair ?? x8 true | xA ⇒ pair ?? x9 true | xB ⇒ pair ?? xA true
949 | xC ⇒ pair ?? xB true | xD ⇒ pair ?? xC true | xE ⇒ pair ?? xD true | xF ⇒ pair ?? xE true ]
951 [ x0 ⇒ pair ?? x0 true | x1 ⇒ pair ?? x1 true | x2 ⇒ pair ?? x2 true | x3 ⇒ pair ?? x3 true
952 | x4 ⇒ pair ?? x4 true | x5 ⇒ pair ?? x5 true | x6 ⇒ pair ?? x6 true | x7 ⇒ pair ?? x7 true
953 | x8 ⇒ pair ?? x8 true | x9 ⇒ pair ?? x9 true | xA ⇒ pair ?? xA true | xB ⇒ pair ?? xB true
954 | xC ⇒ pair ?? xC true | xD ⇒ pair ?? xD true | xE ⇒ pair ?? xE true | xF ⇒ pair ?? xF true ]
956 | false ⇒ match e1 with
958 [ x0 ⇒ pair ?? x0 false | x1 ⇒ pair ?? x1 false | x2 ⇒ pair ?? x2 false | x3 ⇒ pair ?? x3 false
959 | x4 ⇒ pair ?? x4 false | x5 ⇒ pair ?? x5 false | x6 ⇒ pair ?? x6 false | x7 ⇒ pair ?? x7 false
960 | x8 ⇒ pair ?? x8 false | x9 ⇒ pair ?? x9 false | xA ⇒ pair ?? xA false | xB ⇒ pair ?? xB false
961 | xC ⇒ pair ?? xC false | xD ⇒ pair ?? xD false | xE ⇒ pair ?? xE false | xF ⇒ pair ?? xF false ]
963 [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
964 | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
965 | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
966 | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ]
968 [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
969 | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
970 | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
971 | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true | xF ⇒ pair ?? x1 true ]
973 [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
974 | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
975 | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
976 | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true | xE ⇒ pair ?? x1 true | xF ⇒ pair ?? x2 true ]
978 [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
979 | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
980 | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
981 | xC ⇒ pair ?? x0 true | xD ⇒ pair ?? x1 true | xE ⇒ pair ?? x2 true | xF ⇒ pair ?? x3 true ]
983 [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
984 | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
985 | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
986 | xC ⇒ pair ?? x1 true | xD ⇒ pair ?? x2 true | xE ⇒ pair ?? x3 true | xF ⇒ pair ?? x4 true ]
988 [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
989 | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
990 | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true | xB ⇒ pair ?? x1 true
991 | xC ⇒ pair ?? x2 true | xD ⇒ pair ?? x3 true | xE ⇒ pair ?? x4 true | xF ⇒ pair ?? x5 true ]
993 [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
994 | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
995 | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true | xA ⇒ pair ?? x1 true | xB ⇒ pair ?? x2 true
996 | xC ⇒ pair ?? x3 true | xD ⇒ pair ?? x4 true | xE ⇒ pair ?? x5 true | xF ⇒ pair ?? x6 true ]
998 [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
999 | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
1000 | x8 ⇒ pair ?? x0 true | x9 ⇒ pair ?? x1 true | xA ⇒ pair ?? x2 true | xB ⇒ pair ?? x3 true
1001 | xC ⇒ pair ?? x4 true | xD ⇒ pair ?? x5 true | xE ⇒ pair ?? x6 true | xF ⇒ pair ?? x7 true ]
1002 | x9 ⇒ match e2 with
1003 [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
1004 | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
1005 | x8 ⇒ pair ?? x1 true | x9 ⇒ pair ?? x2 true | xA ⇒ pair ?? x3 true | xB ⇒ pair ?? x4 true
1006 | xC ⇒ pair ?? x5 true | xD ⇒ pair ?? x6 true | xE ⇒ pair ?? x7 true | xF ⇒ pair ?? x8 true ]
1007 | xA ⇒ match e2 with
1008 [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
1009 | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true | x7 ⇒ pair ?? x1 true
1010 | x8 ⇒ pair ?? x2 true | x9 ⇒ pair ?? x3 true | xA ⇒ pair ?? x4 true | xB ⇒ pair ?? x5 true
1011 | xC ⇒ pair ?? x6 true | xD ⇒ pair ?? x7 true | xE ⇒ pair ?? x8 true | xF ⇒ pair ?? x9 true ]
1012 | xB ⇒ match e2 with
1013 [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
1014 | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true | x6 ⇒ pair ?? x1 true | x7 ⇒ pair ?? x2 true
1015 | x8 ⇒ pair ?? x3 true | x9 ⇒ pair ?? x4 true | xA ⇒ pair ?? x5 true | xB ⇒ pair ?? x6 true
1016 | xC ⇒ pair ?? x7 true | xD ⇒ pair ?? x8 true | xE ⇒ pair ?? x9 true | xF ⇒ pair ?? xA true ]
1017 | xC ⇒ match e2 with
1018 [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
1019 | x4 ⇒ pair ?? x0 true | x5 ⇒ pair ?? x1 true | x6 ⇒ pair ?? x2 true | x7 ⇒ pair ?? x3 true
1020 | x8 ⇒ pair ?? x4 true | x9 ⇒ pair ?? x5 true | xA ⇒ pair ?? x6 true | xB ⇒ pair ?? x7 true
1021 | xC ⇒ pair ?? x8 true | xD ⇒ pair ?? x9 true | xE ⇒ pair ?? xA true | xF ⇒ pair ?? xB true ]
1022 | xD ⇒ match e2 with
1023 [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
1024 | x4 ⇒ pair ?? x1 true | x5 ⇒ pair ?? x2 true | x6 ⇒ pair ?? x3 true | x7 ⇒ pair ?? x4 true
1025 | x8 ⇒ pair ?? x5 true | x9 ⇒ pair ?? x6 true | xA ⇒ pair ?? x7 true | xB ⇒ pair ?? x8 true
1026 | xC ⇒ pair ?? x9 true | xD ⇒ pair ?? xA true | xE ⇒ pair ?? xB true | xF ⇒ pair ?? xC true ]
1027 | xE ⇒ match e2 with
1028 [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true | x3 ⇒ pair ?? x1 true
1029 | x4 ⇒ pair ?? x2 true | x5 ⇒ pair ?? x3 true | x6 ⇒ pair ?? x4 true | x7 ⇒ pair ?? x5 true
1030 | x8 ⇒ pair ?? x6 true | x9 ⇒ pair ?? x7 true | xA ⇒ pair ?? x8 true | xB ⇒ pair ?? x9 true
1031 | xC ⇒ pair ?? xA true | xD ⇒ pair ?? xB true | xE ⇒ pair ?? xC true | xF ⇒ pair ?? xD true ]
1032 | xF ⇒ match e2 with
1033 [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true | x2 ⇒ pair ?? x1 true | x3 ⇒ pair ?? x2 true
1034 | x4 ⇒ pair ?? x3 true | x5 ⇒ pair ?? x4 true | x6 ⇒ pair ?? x5 true | x7 ⇒ pair ?? x6 true
1035 | x8 ⇒ pair ?? x7 true | x9 ⇒ pair ?? x8 true | xA ⇒ pair ?? x9 true | xB ⇒ pair ?? xA true
1036 | xC ⇒ pair ?? xB true | xD ⇒ pair ?? xC true | xE ⇒ pair ?? xD true | xF ⇒ pair ?? xE true ]
1039 (* operatore somma con data → data+carry *)
1040 ndefinition plus_ex_d_dc ≝
1043 [ x0 ⇒ match e2 with
1044 [ x0 ⇒ pair ?? x0 false | x1 ⇒ pair ?? x1 false | x2 ⇒ pair ?? x2 false | x3 ⇒ pair ?? x3 false
1045 | x4 ⇒ pair ?? x4 false | x5 ⇒ pair ?? x5 false | x6 ⇒ pair ?? x6 false | x7 ⇒ pair ?? x7 false
1046 | x8 ⇒ pair ?? x8 false | x9 ⇒ pair ?? x9 false | xA ⇒ pair ?? xA false | xB ⇒ pair ?? xB false
1047 | xC ⇒ pair ?? xC false | xD ⇒ pair ?? xD false | xE ⇒ pair ?? xE false | xF ⇒ pair ?? xF false ]
1048 | x1 ⇒ match e2 with
1049 [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
1050 | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
1051 | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
1052 | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ]
1053 | x2 ⇒ match e2 with
1054 [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
1055 | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
1056 | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
1057 | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true | xF ⇒ pair ?? x1 true ]
1058 | x3 ⇒ match e2 with
1059 [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
1060 | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
1061 | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
1062 | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true | xE ⇒ pair ?? x1 true | xF ⇒ pair ?? x2 true ]
1063 | x4 ⇒ match e2 with
1064 [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
1065 | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
1066 | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
1067 | xC ⇒ pair ?? x0 true | xD ⇒ pair ?? x1 true | xE ⇒ pair ?? x2 true | xF ⇒ pair ?? x3 true ]
1068 | x5 ⇒ match e2 with
1069 [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
1070 | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
1071 | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
1072 | xC ⇒ pair ?? x1 true | xD ⇒ pair ?? x2 true | xE ⇒ pair ?? x3 true | xF ⇒ pair ?? x4 true ]
1073 | x6 ⇒ match e2 with
1074 [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
1075 | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
1076 | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true | xB ⇒ pair ?? x1 true
1077 | xC ⇒ pair ?? x2 true | xD ⇒ pair ?? x3 true | xE ⇒ pair ?? x4 true | xF ⇒ pair ?? x5 true ]
1078 | x7 ⇒ match e2 with
1079 [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
1080 | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
1081 | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true | xA ⇒ pair ?? x1 true | xB ⇒ pair ?? x2 true
1082 | xC ⇒ pair ?? x3 true | xD ⇒ pair ?? x4 true | xE ⇒ pair ?? x5 true | xF ⇒ pair ?? x6 true ]
1083 | x8 ⇒ match e2 with
1084 [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
1085 | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
1086 | x8 ⇒ pair ?? x0 true | x9 ⇒ pair ?? x1 true | xA ⇒ pair ?? x2 true | xB ⇒ pair ?? x3 true
1087 | xC ⇒ pair ?? x4 true | xD ⇒ pair ?? x5 true | xE ⇒ pair ?? x6 true | xF ⇒ pair ?? x7 true ]
1088 | x9 ⇒ match e2 with
1089 [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
1090 | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
1091 | x8 ⇒ pair ?? x1 true | x9 ⇒ pair ?? x2 true | xA ⇒ pair ?? x3 true | xB ⇒ pair ?? x4 true
1092 | xC ⇒ pair ?? x5 true | xD ⇒ pair ?? x6 true | xE ⇒ pair ?? x7 true | xF ⇒ pair ?? x8 true ]
1093 | xA ⇒ match e2 with
1094 [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
1095 | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true | x7 ⇒ pair ?? x1 true
1096 | x8 ⇒ pair ?? x2 true | x9 ⇒ pair ?? x3 true | xA ⇒ pair ?? x4 true | xB ⇒ pair ?? x5 true
1097 | xC ⇒ pair ?? x6 true | xD ⇒ pair ?? x7 true | xE ⇒ pair ?? x8 true | xF ⇒ pair ?? x9 true ]
1098 | xB ⇒ match e2 with
1099 [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
1100 | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true | x6 ⇒ pair ?? x1 true | x7 ⇒ pair ?? x2 true
1101 | x8 ⇒ pair ?? x3 true | x9 ⇒ pair ?? x4 true | xA ⇒ pair ?? x5 true | xB ⇒ pair ?? x6 true
1102 | xC ⇒ pair ?? x7 true | xD ⇒ pair ?? x8 true | xE ⇒ pair ?? x9 true | xF ⇒ pair ?? xA true ]
1103 | xC ⇒ match e2 with
1104 [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
1105 | x4 ⇒ pair ?? x0 true | x5 ⇒ pair ?? x1 true | x6 ⇒ pair ?? x2 true | x7 ⇒ pair ?? x3 true
1106 | x8 ⇒ pair ?? x4 true | x9 ⇒ pair ?? x5 true | xA ⇒ pair ?? x6 true | xB ⇒ pair ?? x7 true
1107 | xC ⇒ pair ?? x8 true | xD ⇒ pair ?? x9 true | xE ⇒ pair ?? xA true | xF ⇒ pair ?? xB true ]
1108 | xD ⇒ match e2 with
1109 [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
1110 | x4 ⇒ pair ?? x1 true | x5 ⇒ pair ?? x2 true | x6 ⇒ pair ?? x3 true | x7 ⇒ pair ?? x4 true
1111 | x8 ⇒ pair ?? x5 true | x9 ⇒ pair ?? x6 true | xA ⇒ pair ?? x7 true | xB ⇒ pair ?? x8 true
1112 | xC ⇒ pair ?? x9 true | xD ⇒ pair ?? xA true | xE ⇒ pair ?? xB true | xF ⇒ pair ?? xC true ]
1113 | xE ⇒ match e2 with
1114 [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true | x3 ⇒ pair ?? x1 true
1115 | x4 ⇒ pair ?? x2 true | x5 ⇒ pair ?? x3 true | x6 ⇒ pair ?? x4 true | x7 ⇒ pair ?? x5 true
1116 | x8 ⇒ pair ?? x6 true | x9 ⇒ pair ?? x7 true | xA ⇒ pair ?? x8 true | xB ⇒ pair ?? x9 true
1117 | xC ⇒ pair ?? xA true | xD ⇒ pair ?? xB true | xE ⇒ pair ?? xC true | xF ⇒ pair ?? xD true ]
1118 | xF ⇒ match e2 with
1119 [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true | x2 ⇒ pair ?? x1 true | x3 ⇒ pair ?? x2 true
1120 | x4 ⇒ pair ?? x3 true | x5 ⇒ pair ?? x4 true | x6 ⇒ pair ?? x5 true | x7 ⇒ pair ?? x6 true
1121 | x8 ⇒ pair ?? x7 true | x9 ⇒ pair ?? x8 true | xA ⇒ pair ?? x9 true | xB ⇒ pair ?? xA true
1122 | xC ⇒ pair ?? xB true | xD ⇒ pair ?? xC true | xE ⇒ pair ?? xD true | xF ⇒ pair ?? xE true ]
1125 (* operatore somma con data+carry → data *)
1126 ndefinition plus_ex_dc_d ≝
1127 λe1,e2:exadecim.λc:bool.
1129 [ true ⇒ match e1 with
1130 [ x0 ⇒ match e2 with
1131 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1132 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1133 | x1 ⇒ match e2 with
1134 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1135 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1136 | x2 ⇒ match e2 with
1137 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1138 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1139 | x3 ⇒ match e2 with
1140 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1141 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1142 | x4 ⇒ match e2 with
1143 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1144 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1145 | x5 ⇒ match e2 with
1146 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1147 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1148 | x6 ⇒ match e2 with
1149 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1150 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1151 | x7 ⇒ match e2 with
1152 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1153 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1154 | x8 ⇒ match e2 with
1155 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1156 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1157 | x9 ⇒ match e2 with
1158 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1159 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1160 | xA ⇒ match e2 with
1161 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1162 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1163 | xB ⇒ match e2 with
1164 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1165 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1166 | xC ⇒ match e2 with
1167 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1168 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1169 | xD ⇒ match e2 with
1170 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1171 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1172 | xE ⇒ match e2 with
1173 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1174 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1175 | xF ⇒ match e2 with
1176 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1177 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1179 | false ⇒ match e1 with
1180 [ x0 ⇒ match e2 with
1181 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1182 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1183 | x1 ⇒ match e2 with
1184 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1185 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1186 | x2 ⇒ match e2 with
1187 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1188 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1189 | x3 ⇒ match e2 with
1190 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1191 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1192 | x4 ⇒ match e2 with
1193 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1194 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1195 | x5 ⇒ match e2 with
1196 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1197 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1198 | x6 ⇒ match e2 with
1199 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1200 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1201 | x7 ⇒ match e2 with
1202 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1203 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1204 | x8 ⇒ match e2 with
1205 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1206 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1207 | x9 ⇒ match e2 with
1208 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1209 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1210 | xA ⇒ match e2 with
1211 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1212 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1213 | xB ⇒ match e2 with
1214 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1215 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1216 | xC ⇒ match e2 with
1217 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1218 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1219 | xD ⇒ match e2 with
1220 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1221 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1222 | xE ⇒ match e2 with
1223 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1224 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1225 | xF ⇒ match e2 with
1226 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1227 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1230 (* operatore somma con data → data *)
1231 ndefinition plus_ex_d_d ≝
1234 [ x0 ⇒ match e2 with
1235 [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1236 | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1237 | x1 ⇒ match e2 with
1238 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1239 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
1240 | x2 ⇒ match e2 with
1241 [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1242 | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
1243 | x3 ⇒ match e2 with
1244 [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1245 | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1246 | x4 ⇒ match e2 with
1247 [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1248 | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1249 | x5 ⇒ match e2 with
1250 [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1251 | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1252 | x6 ⇒ match e2 with
1253 [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1254 | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1255 | x7 ⇒ match e2 with
1256 [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1257 | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1258 | x8 ⇒ match e2 with
1259 [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1260 | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1261 | x9 ⇒ match e2 with
1262 [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1263 | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1264 | xA ⇒ match e2 with
1265 [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1266 | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1267 | xB ⇒ match e2 with
1268 [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1269 | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1270 | xC ⇒ match e2 with
1271 [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1272 | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1273 | xD ⇒ match e2 with
1274 [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1275 | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1276 | xE ⇒ match e2 with
1277 [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1278 | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1279 | xF ⇒ match e2 with
1280 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1281 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1284 (* operatore somma con data+carry → carry *)
1285 ndefinition plus_ex_dc_c ≝
1286 λe1,e2:exadecim.λc:bool.
1288 [ true ⇒ match e1 with
1289 [ x0 ⇒ 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 ⇒ false | xF ⇒ true ]
1292 | x1 ⇒ 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 ⇒ false | xE ⇒ true | xF ⇒ true ]
1295 | x2 ⇒ 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 ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1298 | x3 ⇒ 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 ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1301 | x4 ⇒ match e2 with
1302 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1303 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1304 | x5 ⇒ match e2 with
1305 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1306 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1307 | x6 ⇒ match e2 with
1308 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1309 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1310 | x7 ⇒ match e2 with
1311 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1312 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1313 | x8 ⇒ match e2 with
1314 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1315 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1316 | x9 ⇒ match e2 with
1317 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1318 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1319 | xA ⇒ match e2 with
1320 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1321 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1322 | xB ⇒ match e2 with
1323 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | 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 | xC ⇒ match e2 with
1326 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | 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 | xD ⇒ match e2 with
1329 [ x0 ⇒ false | x1 ⇒ false | 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 ]
1331 | xE ⇒ match e2 with
1332 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1333 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1334 | xF ⇒ match e2 with
1335 [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1336 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1338 | false ⇒ match e1 with
1339 [ x0 ⇒ 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 ⇒ false ]
1342 | x1 ⇒ 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 ⇒ false | xF ⇒ true ]
1345 | x2 ⇒ 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 ⇒ false | xE ⇒ true | xF ⇒ true ]
1348 | x3 ⇒ 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 ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1351 | x4 ⇒ 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 ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1354 | x5 ⇒ 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 ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1357 | x6 ⇒ match e2 with
1358 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1359 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1360 | x7 ⇒ match e2 with
1361 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1362 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1363 | x8 ⇒ match e2 with
1364 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1365 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1366 | x9 ⇒ match e2 with
1367 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1368 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1369 | xA ⇒ match e2 with
1370 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1371 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1372 | xB ⇒ match e2 with
1373 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1374 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1375 | xC ⇒ match e2 with
1376 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | 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 | xD ⇒ match e2 with
1379 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | 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 | xE ⇒ match e2 with
1382 [ x0 ⇒ false | x1 ⇒ false | 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 ]
1384 | xF ⇒ match e2 with
1385 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1386 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1389 (* operatore somma con data → carry *)
1390 ndefinition plus_ex_d_c ≝
1393 [ x0 ⇒ match e2 with
1394 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1395 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
1396 | x1 ⇒ match e2 with
1397 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1398 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
1399 | x2 ⇒ match e2 with
1400 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1401 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
1402 | x3 ⇒ match e2 with
1403 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1404 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1405 | x4 ⇒ match e2 with
1406 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1407 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1408 | x5 ⇒ match e2 with
1409 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1410 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1411 | x6 ⇒ match e2 with
1412 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1413 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1414 | x7 ⇒ match e2 with
1415 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1416 | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1417 | x8 ⇒ match e2 with
1418 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1419 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1420 | x9 ⇒ match e2 with
1421 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1422 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1423 | xA ⇒ match e2 with
1424 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
1425 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1426 | xB ⇒ match e2 with
1427 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1428 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1429 | xC ⇒ match e2 with
1430 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1431 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1432 | xD ⇒ match e2 with
1433 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1434 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1435 | xE ⇒ match e2 with
1436 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1437 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1438 | xF ⇒ match e2 with
1439 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
1440 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
1443 (* operatore Most Significant Bit *)
1444 ndefinition MSB_ex ≝
1445 λe:exadecim.match e with
1446 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
1447 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1448 | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
1449 | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
1451 (* esadecimali → naturali *)
1452 ndefinition nat_of_exadecim : exadecim → nat ≝
1455 [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2 | x3 ⇒ 3 | x4 ⇒ 4 | x5 ⇒ 5 | x6 ⇒ 6 | x7 ⇒ 7
1456 | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
1458 (* operatore predecessore *)
1459 ndefinition pred_ex ≝
1462 [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1463 | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1465 (* operatore successore *)
1466 ndefinition succ_ex ≝
1469 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1470 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1472 (* operatore neg/complemento a 2 *)
1473 ndefinition compl_ex ≝
1474 λe:exadecim.match e with
1475 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1476 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1477 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1478 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1480 (* iteratore sugli esadecimali *)
1481 ndefinition forall_exadecim ≝ λP.
1482 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
1483 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.