]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly/num/exadecim.ma
mod change (-x)
[helm.git] / matitaB / matita / contribs / ng_assembly / num / exadecim.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/bool.ma".
24 include "num/quatern.ma".
25 include "num/oct.ma".
26 include "common/prod.ma".
27
28 (* *********** *)
29 (* ESADECIMALI *)
30 (* *********** *)
31
32 ninductive exadecim : Type ≝
33   x0: exadecim
34 | x1: exadecim
35 | x2: exadecim
36 | x3: exadecim
37 | x4: exadecim
38 | x5: exadecim
39 | x6: exadecim
40 | x7: exadecim
41 | x8: exadecim
42 | x9: exadecim
43 | xA: exadecim
44 | xB: exadecim
45 | xC: exadecim
46 | xD: exadecim
47 | xE: exadecim
48 | xF: exadecim.
49
50 (* iteratore sugli esadecimali *)
51 ndefinition forall_ex ≝ λP.
52  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
53  P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
54
55 (* operatore = *)
56 ndefinition eq_ex ≝
57 λe1,e2:exadecim.
58  match e1 with
59   [ x0 ⇒ match e2 with [ x0 ⇒ true  | _ ⇒ false ]
60   | x1 ⇒ match e2 with [ x1 ⇒ true  | _ ⇒ false ]
61   | x2 ⇒ match e2 with [ x2 ⇒ true  | _ ⇒ false ]
62   | x3 ⇒ match e2 with [ x3 ⇒ true  | _ ⇒ false ]
63   | x4 ⇒ match e2 with [ x4 ⇒ true  | _ ⇒ false ]
64   | x5 ⇒ match e2 with [ x5 ⇒ true  | _ ⇒ false ]
65   | x6 ⇒ match e2 with [ x6 ⇒ true  | _ ⇒ false ]
66   | x7 ⇒ match e2 with [ x7 ⇒ true  | _ ⇒ false ]
67   | x8 ⇒ match e2 with [ x8 ⇒ true  | _ ⇒ false ]
68   | x9 ⇒ match e2 with [ x9 ⇒ true  | _ ⇒ false ]
69   | xA ⇒ match e2 with [ xA ⇒ true  | _ ⇒ false ]
70   | xB ⇒ match e2 with [ xB ⇒ true  | _ ⇒ false ]
71   | xC ⇒ match e2 with [ xC ⇒ true  | _ ⇒ false ]
72   | xD ⇒ match e2 with [ xD ⇒ true  | _ ⇒ false ]
73   | xE ⇒ match e2 with [ xE ⇒ true  | _ ⇒ false ]
74   | xF ⇒ match e2 with [ xF ⇒ true  | _ ⇒ false ]
75   ].
76
77 (* operatore < *)
78 ndefinition lt_ex ≝
79 λe1,e2:exadecim.
80  match e1 with
81   [ x0 ⇒ match e2 with
82    [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
83    | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
84    | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true
85    | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ] 
86   | x1 ⇒ match e2 with
87    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
88    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
89    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true
90    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ] 
91   | x2 ⇒ match e2 with
92    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
93    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
94    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
95    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
96   | x3 ⇒ match e2 with
97    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
98    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
99    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
100    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
101   | x4 ⇒ match e2 with
102    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
103    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
104    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
105    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
106   | x5 ⇒ match e2 with
107    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
108    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
109    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
110    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
111   | x6 ⇒ match e2 with
112    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
113    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
114    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
115    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
116   | x7 ⇒ match e2 with
117    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
118    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false 
119    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
120    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
121   | x8 ⇒ match e2 with
122    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
123    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
124    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
125    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
126   | x9 ⇒ match e2 with
127    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
128    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
129    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true 
130    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
131   | xA ⇒ match e2 with
132    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
133    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
134    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
135    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
136   | xB ⇒ match e2 with
137    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
138    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
139    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
140    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
141   | xC ⇒ match e2 with
142    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
143    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
144    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
145    | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
146   | xD ⇒ match e2 with
147    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
148    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
149    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
150    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ] 
151   | xE ⇒ match e2 with
152    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
153    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
154    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
155    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] 
156   | xF ⇒ match e2 with
157    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
158    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
159    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
160    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
161   ].
162
163 (* operatore ≤ *)
164 ndefinition le_ex ≝
165 λe1,e2:exadecim.
166  match e1 with
167   [ x0 ⇒ match e2 with
168    [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true 
169    | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
170    | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true 
171    | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] 
172   | x1 ⇒ match e2 with
173    [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true 
174    | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
175    | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true 
176    | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ] 
177   | x2 ⇒ match e2 with
178    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true 
179    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
180    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true 
181    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ] 
182   | x3 ⇒ match e2 with
183    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true 
184    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
185    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
186    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
187   | x4 ⇒ match e2 with
188    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
189    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
190    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
191    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
192   | x5 ⇒ match e2 with
193    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
194    | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
195    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
196    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
197   | x6 ⇒ match e2 with
198    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
199    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
200    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
201    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
202   | x7 ⇒ match e2 with
203    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
204    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true 
205    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
206    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
207   | x8 ⇒ match e2 with
208    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
209    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
210    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
211    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
212   | x9 ⇒ match e2 with
213    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
214    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
215    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
216    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
217   | xA ⇒ match e2 with
218    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
219    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
220    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true 
221    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
222   | xB ⇒ match e2 with
223    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
224    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
225    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
226    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
227   | xC ⇒ match e2 with
228    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
229    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
230    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
231    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
232   | xD ⇒ match e2 with
233    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
234    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
235    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
236    | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
237   | xE ⇒ match e2 with
238    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
239    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
240    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
241    | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ] 
242   | xF ⇒ match e2 with
243    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
244    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
245    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
246    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
247   ].
248
249 (* operatore > *)
250 ndefinition gt_ex ≝
251 λe1,e2:exadecim.
252  match e1 with
253   [ x0 ⇒ match e2 with
254    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
255    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
256    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
257    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
258   | x1 ⇒ match e2 with
259    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
260    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
261    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
262    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
263   | x2 ⇒ match e2 with
264    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false 
265    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
266    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
267    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
268   | x3 ⇒ match e2 with
269    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false 
270    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
271    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
272    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
273   | x4 ⇒ match e2 with
274    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
275    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
276    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
277    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
278   | x5 ⇒ match e2 with
279    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
280    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
281    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
282    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
283   | x6 ⇒ match e2 with
284    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
285    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
286    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
287    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
288   | x7 ⇒ match e2 with
289    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
290    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
291    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
292    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
293   | x8 ⇒ match e2 with
294    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
295    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
296    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
297    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
298   | x9 ⇒ match e2 with
299    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
300    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
301    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
302    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
303   | xA ⇒ match e2 with
304    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
305    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
306    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false 
307    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
308   | xB ⇒ match e2 with
309    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
310    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
311    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false 
312    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
313   | xC ⇒ match e2 with
314    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
315    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
316    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
317    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
318   | xD ⇒ match e2 with
319    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
320    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
321    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
322    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
323   | xE ⇒ match e2 with
324    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
325    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
326    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
327    | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
328   | xF ⇒ match e2 with
329    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
330    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
331    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
332    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
333   ].
334
335 (* operatore ≥ *)
336 ndefinition ge_ex ≝
337 λe1,e2:exadecim.
338  match e1 with
339   [ x0 ⇒ match e2 with
340    [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
341    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
342    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
343    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
344   | x1 ⇒ match e2 with
345    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false 
346    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
347    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
348    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
349   | x2 ⇒ match e2 with
350    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false 
351    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
352    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
353    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
354   | x3 ⇒ match e2 with
355    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
356    | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
357    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
358    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
359   | x4 ⇒ match e2 with
360    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
361    | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
362    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
363    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
364   | x5 ⇒ match e2 with
365    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
366    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
367    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
368    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
369   | x6 ⇒ match e2 with
370    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
371    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
372    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
373    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
374   | x7 ⇒ match e2 with
375    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
376    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
377    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
378    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
379   | x8 ⇒ match e2 with
380    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
381    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
382    | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
383    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
384   | x9 ⇒ match e2 with
385    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
386    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
387    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false 
388    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
389   | xA ⇒ match e2 with
390    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
391    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
392    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false 
393    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
394   | xB ⇒ match e2 with
395    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
396    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
397    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
398    | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
399   | xC ⇒ match e2 with
400    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
401    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
402    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
403    | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
404   | xD ⇒ match e2 with
405    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
406    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
407    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
408    | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
409   | xE ⇒ match e2 with
410    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
411    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
412    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
413    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
414   | xF ⇒ match e2 with
415    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
416    | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
417    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
418    | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
419   ].
420
421 (* operatore and *)
422 ndefinition and_ex ≝
423 λe1,e2:exadecim.match e1 with
424  [ x0 ⇒ match e2 with
425   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
426   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
427   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 
428   | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
429  | x1 ⇒ match e2 with
430   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
431   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
432   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 
433   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
434  | x2 ⇒ match e2 with
435   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
436   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
437   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 
438   | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
439  | x3 ⇒ match e2 with
440   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
441   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
442   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
443   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
444  | x4 ⇒ match e2 with
445   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
446   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
447   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 
448   | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
449  | x5 ⇒ match e2 with
450   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
451   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
452   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 
453   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
454  | x6 ⇒ match e2 with
455   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
456   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
457   | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 
458   | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
459  | x7 ⇒ match e2 with
460   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
461   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
462   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
463   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
464  | x8 ⇒ match e2 with
465   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
466   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
467   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 
468   | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
469  | x9 ⇒ match e2 with
470   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
471   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
472   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 
473   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
474  | xA ⇒ match e2 with
475   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
476   | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
477   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA 
478   | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
479  | xB ⇒ match e2 with
480   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
481   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
482   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
483   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
484  | xC ⇒ match e2 with
485   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
486   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
487   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 
488   | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ] 
489  | xD ⇒ match e2 with
490   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
491   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
492   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 
493   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ] 
494  | xE ⇒ match e2 with
495   [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
496   | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
497   | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA 
498   | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ] 
499  | xF ⇒ match e2 with
500   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
501   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
502   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
503   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
504  ]. 
505
506 (* operatore or *)
507 ndefinition or_ex ≝
508 λe1,e2:exadecim.match e1 with
509  [ x0 ⇒ match e2 with
510   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
511   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
512   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
513   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
514  | x1 ⇒ match e2 with
515   [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3 
516   | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
517   | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB 
518   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
519  | x2 ⇒ match e2 with
520   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3 
521   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
522   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB 
523   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
524  | x3 ⇒ match e2 with
525   [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3 
526   | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
527   | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB 
528   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
529  | x4 ⇒ match e2 with
530   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 
531   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
532   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
533   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
534  | x5 ⇒ match e2 with
535   [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7 
536   | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
537   | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF 
538   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
539  | x6 ⇒ match e2 with
540   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7 
541   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
542   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF 
543   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
544  | x7 ⇒ match e2 with
545   [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7 
546   | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
547   | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF 
548   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
549  | x8 ⇒ match e2 with
550   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB 
551   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
552   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
553   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
554  | x9 ⇒ match e2 with
555   [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB 
556   | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
557   | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB 
558   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
559  | xA ⇒ match e2 with
560   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB 
561   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
562   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB 
563   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
564  | xB ⇒ match e2 with
565   [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB 
566   | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
567   | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB 
568   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
569  | xC ⇒ match e2 with
570   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF 
571   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
572   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
573   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
574  | xD ⇒ match e2 with
575   [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF 
576   | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
577   | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF 
578   | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
579  | xE ⇒ match e2 with
580   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF 
581   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
582   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF 
583   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
584  | xF ⇒ match e2 with
585   [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF 
586   | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
587   | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF 
588   | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
589  ].
590
591 (* operatore xor *)
592 ndefinition xor_ex ≝
593 λe1,e2:exadecim.match e1 with
594  [ x0 ⇒ match e2 with
595   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
596   | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
597   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
598   | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] 
599  | x1 ⇒ match e2 with
600   [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2 
601   | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
602   | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA 
603   | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ] 
604  | x2 ⇒ match e2 with
605   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1 
606   | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
607   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9 
608   | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ] 
609  | x3 ⇒ match e2 with
610   [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0 
611   | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
612   | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8 
613   | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ] 
614  | x4 ⇒ match e2 with
615   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 
616   | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
617   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
618   | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] 
619  | x5 ⇒ match e2 with
620   [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6 
621   | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
622   | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE 
623   | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ] 
624  | x6 ⇒ match e2 with
625   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5 
626   | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
627   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD 
628   | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ] 
629  | x7 ⇒ match e2 with
630   [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4 
631   | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
632   | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC 
633   | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ] 
634  | x8 ⇒ match e2 with
635   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB 
636   | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
637   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
638   | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] 
639  | x9 ⇒ match e2 with
640   [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA 
641   | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
642   | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2 
643   | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ] 
644  | xA ⇒ match e2 with
645   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9 
646   | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
647   | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1 
648   | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ] 
649  | xB ⇒ match e2 with
650   [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8 
651   | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
652   | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0 
653   | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
654  | xC ⇒ match e2 with
655   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF 
656   | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
657   | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 
658   | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] 
659  | xD ⇒ match e2 with
660   [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE 
661   | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
662   | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6 
663   | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
664  | xE ⇒ match e2 with
665   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD 
666   | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
667   | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5 
668   | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ] 
669  | xF ⇒ match e2 with
670   [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC 
671   | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
672   | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4 
673   | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ] 
674  ].
675
676 (* operatore Most Significant Bit *)
677 ndefinition getMSB_ex ≝
678 λe:exadecim.match e with
679  [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
680  | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
681  | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
682  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ].
683
684 ndefinition setMSB_ex ≝
685 λe:exadecim.match e with
686  [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
687  | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
688  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
689  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ].
690
691 ndefinition clrMSB_ex ≝
692 λe:exadecim.match e with
693  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
694  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
695  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
696  | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ].
697
698 (* operatore Least Significant Bit *)
699 ndefinition getLSB_ex ≝
700 λe:exadecim.match e with
701  [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true
702  | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true
703  | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true
704  | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ].
705
706 ndefinition setLSB_ex ≝
707 λe:exadecim.match e with
708  [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
709  | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
710  | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
711  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
712
713 ndefinition clrLSB_ex ≝
714 λe:exadecim.match e with
715  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
716  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
717  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
718  | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ].
719
720 (* operatore rotazione destra con carry *)
721 ndefinition rcr_ex ≝
722 λc:bool.λe:exadecim.match c with
723  [ true ⇒ match e with
724   [ x0 ⇒ pair … false x8 | x1 ⇒ pair … true x8
725   | x2 ⇒ pair … false x9 | x3 ⇒ pair … true x9
726   | x4 ⇒ pair … false xA | x5 ⇒ pair … true xA
727   | x6 ⇒ pair … false xB | x7 ⇒ pair … true xB
728   | x8 ⇒ pair … false xC | x9 ⇒ pair … true xC
729   | xA ⇒ pair … false xD | xB ⇒ pair … true xD
730   | xC ⇒ pair … false xE | xD ⇒ pair … true xE
731   | xE ⇒ pair … false xF | xF ⇒ pair … true xF ]
732  | false ⇒ match e with 
733   [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
734   | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
735   | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
736   | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
737   | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
738   | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
739   | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
740   | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ]
741  ].
742
743 (* operatore shift destro *)
744 ndefinition shr_ex ≝
745 λe:exadecim.match e with 
746  [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
747  | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
748  | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
749  | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
750  | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
751  | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
752  | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
753  | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ].
754
755 (* operatore rotazione destra *)
756 ndefinition ror_ex ≝
757 λe:exadecim.match e with 
758  [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
759  | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB 
760  | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD 
761  | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
762
763 (* operatore rotazione sinistra con carry *)
764 ndefinition rcl_ex ≝
765 λc:bool.λe:exadecim.match c with
766  [ true ⇒ match e with
767   [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x3
768   | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x7
769   | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xB
770   | x6 ⇒ pair … false xD | x7 ⇒ pair … false xF
771   | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x3
772   | xA ⇒ pair … true x5  | xB ⇒ pair … true x7
773   | xC ⇒ pair … true x9  | xD ⇒ pair … true xB
774   | xE ⇒ pair … true xD  | xF ⇒ pair … true xF ]
775  | false ⇒ match e with
776   [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
777   | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
778   | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
779   | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
780   | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x2
781   | xA ⇒ pair … true x4  | xB ⇒ pair … true x6
782   | xC ⇒ pair … true x8  | xD ⇒ pair … true xA
783   | xE ⇒ pair … true xC  | xF ⇒ pair … true xE ]
784  ].
785
786 (* operatore shift sinistro *)
787 ndefinition shl_ex ≝
788 λe:exadecim.match e with
789  [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
790  | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
791  | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
792  | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
793  | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x2
794  | xA ⇒ pair … true x4  | xB ⇒ pair … true x6
795  | xC ⇒ pair … true x8  | xD ⇒ pair … true xA
796  | xE ⇒ pair … true xC  | xF ⇒ pair … true xE ].
797
798 (* operatore rotazione sinistra *)
799 ndefinition rol_ex ≝
800 λe:exadecim.match e with
801  [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
802  | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
803  | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
804  | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
805
806 (* operatore not/complemento a 1 *)
807 ndefinition not_ex ≝
808 λe:exadecim.match e with
809  [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
810  | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
811  | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
812  | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
813
814 (* operatore somma con data+carry → data+carry *)
815 ndefinition plus_ex_dc_dc ≝
816 λc:bool.λe1,e2:exadecim.
817  match c with
818   [ true ⇒ match e1 with
819    [ x0 ⇒ match e2 with
820     [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
821     | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
822     | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
823     | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] 
824    | x1 ⇒ match e2 with
825     [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
826     | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
827     | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
828     | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0  | xF ⇒ pair … true x1 ] 
829    | x2 ⇒ match e2 with
830     [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
831     | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
832     | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
833     | xC ⇒ pair … false xF | xD ⇒ pair … true x0  | xE ⇒ pair … true x1  | xF ⇒ pair … true x2 ] 
834    | x3 ⇒ match e2 with
835     [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
836     | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
837     | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
838     | xC ⇒ pair … true x0  | xD ⇒ pair … true x1  | xE ⇒ pair … true x2  | xF ⇒ pair … true x3 ] 
839    | x4 ⇒ match e2 with
840     [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
841     | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
842     | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
843     | xC ⇒ pair … true x1  | xD ⇒ pair … true x2  | xE ⇒ pair … true x3  | xF ⇒ pair … true x4 ] 
844    | x5 ⇒ match e2 with
845     [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
846     | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
847     | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0  | xB ⇒ pair … true x1
848     | xC ⇒ pair … true x2  | xD ⇒ pair … true x3  | xE ⇒ pair … true x4  | xF ⇒ pair … true x5 ] 
849    | x6 ⇒ match e2 with
850     [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
851     | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
852     | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0  | xA ⇒ pair … true x1  | xB ⇒ pair … true x2
853     | xC ⇒ pair … true x3  | xD ⇒ pair … true x4  | xE ⇒ pair … true x5  | xF ⇒ pair … true x6 ] 
854    | x7 ⇒ match e2 with
855     [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
856     | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
857     | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x1  | xA ⇒ pair … true x2  | xB ⇒ pair … true x3
858     | xC ⇒ pair … true x4  | xD ⇒ pair … true x5  | xE ⇒ pair … true x6  | xF ⇒ pair … true x7 ] 
859    | x8 ⇒ match e2 with
860     [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
861     | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
862     | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x2  | xA ⇒ pair … true x3  | xB ⇒ pair … true x4
863     | xC ⇒ pair … true x5  | xD ⇒ pair … true x6  | xE ⇒ pair … true x7  | xF ⇒ pair … true x8 ] 
864    | x9 ⇒ match e2 with
865     [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
866     | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0  | x7 ⇒ pair … true x1
867     | x8 ⇒ pair … true x2  | x9 ⇒ pair … true x3  | xA ⇒ pair … true x4  | xB ⇒ pair … true x5
868     | xC ⇒ pair … true x6  | xD ⇒ pair … true x7  | xE ⇒ pair … true x8  | xF ⇒ pair … true x9 ] 
869    | xA ⇒ match e2 with
870     [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
871     | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0  | x6 ⇒ pair … true x1  | x7 ⇒ pair … true x2
872     | x8 ⇒ pair … true x3  | x9 ⇒ pair … true x4  | xA ⇒ pair … true x5  | xB ⇒ pair … true x6
873     | xC ⇒ pair … true x7  | xD ⇒ pair … true x8  | xE ⇒ pair … true x9  | xF ⇒ pair … true xA ] 
874    | xB ⇒ match e2 with
875     [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
876     | x4 ⇒ pair … true x0  | x5 ⇒ pair … true x1  | x6 ⇒ pair … true x2  | x7 ⇒ pair … true x3
877     | x8 ⇒ pair … true x4  | x9 ⇒ pair … true x5  | xA ⇒ pair … true x6  | xB ⇒ pair … true x7
878     | xC ⇒ pair … true x8  | xD ⇒ pair … true x9  | xE ⇒ pair … true xA  | xF ⇒ pair … true xB ] 
879    | xC ⇒ match e2 with
880     [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
881     | x4 ⇒ pair … true x1  | x5 ⇒ pair … true x2  | x6 ⇒ pair … true x3  | x7 ⇒ pair … true x4
882     | x8 ⇒ pair … true x5  | x9 ⇒ pair … true x6  | xA ⇒ pair … true x7  | xB ⇒ pair … true x8
883     | xC ⇒ pair … true x9  | xD ⇒ pair … true xA  | xE ⇒ pair … true xB  | xF ⇒ pair … true xC ] 
884    | xD ⇒ match e2 with
885     [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0  | x3 ⇒ pair … true x1
886     | x4 ⇒ pair … true x2  | x5 ⇒ pair … true x3  | x6 ⇒ pair … true x4  | x7 ⇒ pair … true x5
887     | x8 ⇒ pair … true x6  | x9 ⇒ pair … true x7  | xA ⇒ pair … true x8  | xB ⇒ pair … true x9
888     | xC ⇒ pair … true xA  | xD ⇒ pair … true xB  | xE ⇒ pair … true xC  | xF ⇒ pair … true xD ] 
889    | xE ⇒ match e2 with
890     [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0  | x2 ⇒ pair … true x1  | x3 ⇒ pair … true x2
891     | x4 ⇒ pair … true x3  | x5 ⇒ pair … true x4  | x6 ⇒ pair … true x5  | x7 ⇒ pair … true x6
892     | x8 ⇒ pair … true x7  | x9 ⇒ pair … true x8  | xA ⇒ pair … true x9  | xB ⇒ pair … true xA
893     | xC ⇒ pair … true xB  | xD ⇒ pair … true xC  | xE ⇒ pair … true xD  | xF ⇒ pair … true xE ]
894    | xF ⇒ match e2 with
895     [ x0 ⇒ pair … true x0  | x1 ⇒ pair … true x1  | x2 ⇒ pair … true x2  | x3 ⇒ pair … true x3
896     | x4 ⇒ pair … true x4  | x5 ⇒ pair … true x5  | x6 ⇒ pair … true x6  | x7 ⇒ pair … true x7
897     | x8 ⇒ pair … true x8  | x9 ⇒ pair … true x9  | xA ⇒ pair … true xA  | xB ⇒ pair … true xB
898     | xC ⇒ pair … true xC  | xD ⇒ pair … true xD  | xE ⇒ pair … true xE  | xF ⇒ pair … true xF ] 
899    ]
900   | false ⇒ match e1 with
901    [ x0 ⇒ match e2 with
902     [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
903     | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
904     | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
905     | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ] 
906    | x1 ⇒ match e2 with
907     [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
908     | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
909     | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
910     | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] 
911    | x2 ⇒ match e2 with
912     [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
913     | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
914     | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
915     | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0  | xF ⇒ pair … true x1 ] 
916    | x3 ⇒ match e2 with
917     [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
918     | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
919     | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
920     | xC ⇒ pair … false xF | xD ⇒ pair … true x0  | xE ⇒ pair … true x1  | xF ⇒ pair … true x2 ] 
921    | x4 ⇒ match e2 with
922     [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
923     | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
924     | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
925     | xC ⇒ pair … true x0  | xD ⇒ pair … true x1  | xE ⇒ pair … true x2  | xF ⇒ pair … true x3 ] 
926    | x5 ⇒ match e2 with
927     [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
928     | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
929     | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
930     | xC ⇒ pair … true x1  | xD ⇒ pair … true x2  | xE ⇒ pair … true x3  | xF ⇒ pair … true x4 ] 
931    | x6 ⇒ match e2 with
932     [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
933     | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
934     | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0  | xB ⇒ pair … true x1
935     | xC ⇒ pair … true x2  | xD ⇒ pair … true x3  | xE ⇒ pair … true x4  | xF ⇒ pair … true x5 ] 
936    | x7 ⇒ match e2 with
937     [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
938     | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
939     | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0  | xA ⇒ pair … true x1  | xB ⇒ pair … true x2
940     | xC ⇒ pair … true x3  | xD ⇒ pair … true x4  | xE ⇒ pair … true x5  | xF ⇒ pair … true x6 ] 
941    | x8 ⇒ match e2 with
942     [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
943     | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
944     | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x1  | xA ⇒ pair … true x2  | xB ⇒ pair … true x3
945     | xC ⇒ pair … true x4  | xD ⇒ pair … true x5  | xE ⇒ pair … true x6  | xF ⇒ pair … true x7 ] 
946    | x9 ⇒ match e2 with
947     [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
948     | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
949     | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x2  | xA ⇒ pair … true x3  | xB ⇒ pair … true x4
950     | xC ⇒ pair … true x5  | xD ⇒ pair … true x6  | xE ⇒ pair … true x7  | xF ⇒ pair … true x8 ] 
951    | xA ⇒ match e2 with
952     [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
953     | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0  | x7 ⇒ pair … true x1
954     | x8 ⇒ pair … true x2  | x9 ⇒ pair … true x3  | xA ⇒ pair … true x4  | xB ⇒ pair … true x5
955     | xC ⇒ pair … true x6  | xD ⇒ pair … true x7  | xE ⇒ pair … true x8  | xF ⇒ pair … true x9 ] 
956    | xB ⇒ match e2 with
957     [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
958     | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0  | x6 ⇒ pair … true x1  | x7 ⇒ pair … true x2
959     | x8 ⇒ pair … true x3  | x9 ⇒ pair … true x4  | xA ⇒ pair … true x5  | xB ⇒ pair … true x6
960     | xC ⇒ pair … true x7  | xD ⇒ pair … true x8  | xE ⇒ pair … true x9  | xF ⇒ pair … true xA ] 
961    | xC ⇒ match e2 with
962     [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
963     | x4 ⇒ pair … true x0  | x5 ⇒ pair … true x1  | x6 ⇒ pair … true x2  | x7 ⇒ pair … true x3
964     | x8 ⇒ pair … true x4  | x9 ⇒ pair … true x5  | xA ⇒ pair … true x6  | xB ⇒ pair … true x7
965     | xC ⇒ pair … true x8  | xD ⇒ pair … true x9  | xE ⇒ pair … true xA  | xF ⇒ pair … true xB ] 
966    | xD ⇒ match e2 with
967     [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
968     | x4 ⇒ pair … true x1  | x5 ⇒ pair … true x2  | x6 ⇒ pair … true x3  | x7 ⇒ pair … true x4
969     | x8 ⇒ pair … true x5  | x9 ⇒ pair … true x6  | xA ⇒ pair … true x7  | xB ⇒ pair … true x8
970     | xC ⇒ pair … true x9  | xD ⇒ pair … true xA  | xE ⇒ pair … true xB  | xF ⇒ pair … true xC ] 
971    | xE ⇒ match e2 with
972     [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0  | x3 ⇒ pair … true x1
973     | x4 ⇒ pair … true x2  | x5 ⇒ pair … true x3  | x6 ⇒ pair … true x4  | x7 ⇒ pair … true x5
974     | x8 ⇒ pair … true x6  | x9 ⇒ pair … true x7  | xA ⇒ pair … true x8  | xB ⇒ pair … true x9
975     | xC ⇒ pair … true xA  | xD ⇒ pair … true xB  | xE ⇒ pair … true xC  | xF ⇒ pair … true xD ] 
976    | xF ⇒ match e2 with
977     [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0  | x2 ⇒ pair … true x1  | x3 ⇒ pair … true x2
978     | x4 ⇒ pair … true x3  | x5 ⇒ pair … true x4  | x6 ⇒ pair … true x5  | x7 ⇒ pair … true x6
979     | x8 ⇒ pair … true x7  | x9 ⇒ pair … true x8  | xA ⇒ pair … true x9  | xB ⇒ pair … true xA
980     | xC ⇒ pair … true xB  | xD ⇒ pair … true xC  | xE ⇒ pair … true xD  | xF ⇒ pair … true xE ]
981    ]].
982
983 (* operatore somma con data → data+carry *)
984 ndefinition plus_ex_d_dc ≝
985 λe1,e2:exadecim.
986  match e1 with
987   [ x0 ⇒ match e2 with
988    [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
989    | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
990    | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
991    | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]  
992   | x1 ⇒ match e2 with
993    [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
994    | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
995    | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
996    | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] 
997   | x2 ⇒ match e2 with
998    [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
999    | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
1000    | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
1001    | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0  | xF ⇒ pair … true x1 ] 
1002   | x3 ⇒ match e2 with
1003    [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
1004    | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
1005    | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
1006    | xC ⇒ pair … false xF | xD ⇒ pair … true x0  | xE ⇒ pair … true x1  | xF ⇒ pair … true x2 ] 
1007   | x4 ⇒ match e2 with
1008    [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
1009    | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
1010    | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
1011    | xC ⇒ pair … true x0  | xD ⇒ pair … true x1  | xE ⇒ pair … true x2  | xF ⇒ pair … true x3 ] 
1012   | x5 ⇒ match e2 with
1013    [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
1014    | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
1015    | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
1016    | xC ⇒ pair … true x1  | xD ⇒ pair … true x2  | xE ⇒ pair … true x3  | xF ⇒ pair … true x4 ] 
1017   | x6 ⇒ match e2 with
1018    [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
1019    | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
1020    | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0  | xB ⇒ pair … true x1
1021    | xC ⇒ pair … true x2  | xD ⇒ pair … true x3  | xE ⇒ pair … true x4  | xF ⇒ pair … true x5 ] 
1022   | x7 ⇒ match e2 with
1023    [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
1024    | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
1025    | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0  | xA ⇒ pair … true x1  | xB ⇒ pair … true x2
1026    | xC ⇒ pair … true x3  | xD ⇒ pair … true x4  | xE ⇒ pair … true x5  | xF ⇒ pair … true x6 ] 
1027   | x8 ⇒ match e2 with
1028    [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
1029    | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
1030    | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x1  | xA ⇒ pair … true x2  | xB ⇒ pair … true x3
1031    | xC ⇒ pair … true x4  | xD ⇒ pair … true x5  | xE ⇒ pair … true x6  | xF ⇒ pair … true x7 ] 
1032   | x9 ⇒ match e2 with
1033    [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
1034    | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
1035    | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x2  | xA ⇒ pair … true x3  | xB ⇒ pair … true x4
1036    | xC ⇒ pair … true x5  | xD ⇒ pair … true x6  | xE ⇒ pair … true x7  | xF ⇒ pair … true x8 ] 
1037   | xA ⇒ match e2 with
1038    [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
1039    | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0  | x7 ⇒ pair … true x1
1040    | x8 ⇒ pair … true x2  | x9 ⇒ pair … true x3  | xA ⇒ pair … true x4  | xB ⇒ pair … true x5
1041    | xC ⇒ pair … true x6  | xD ⇒ pair … true x7  | xE ⇒ pair … true x8  | xF ⇒ pair … true x9 ] 
1042   | xB ⇒ match e2 with
1043    [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
1044    | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0  | x6 ⇒ pair … true x1  | x7 ⇒ pair … true x2
1045    | x8 ⇒ pair … true x3  | x9 ⇒ pair … true x4  | xA ⇒ pair … true x5  | xB ⇒ pair … true x6
1046    | xC ⇒ pair … true x7  | xD ⇒ pair … true x8  | xE ⇒ pair … true x9  | xF ⇒ pair … true xA ] 
1047   | xC ⇒ match e2 with
1048    [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
1049    | x4 ⇒ pair … true x0  | x5 ⇒ pair … true x1  | x6 ⇒ pair … true x2  | x7 ⇒ pair … true x3
1050    | x8 ⇒ pair … true x4  | x9 ⇒ pair … true x5  | xA ⇒ pair … true x6  | xB ⇒ pair … true x7
1051    | xC ⇒ pair … true x8  | xD ⇒ pair … true x9  | xE ⇒ pair … true xA  | xF ⇒ pair … true xB ] 
1052   | xD ⇒ match e2 with
1053    [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
1054    | x4 ⇒ pair … true x1  | x5 ⇒ pair … true x2  | x6 ⇒ pair … true x3  | x7 ⇒ pair … true x4
1055    | x8 ⇒ pair … true x5  | x9 ⇒ pair … true x6  | xA ⇒ pair … true x7  | xB ⇒ pair … true x8
1056    | xC ⇒ pair … true x9  | xD ⇒ pair … true xA  | xE ⇒ pair … true xB  | xF ⇒ pair … true xC ] 
1057   | xE ⇒ match e2 with
1058    [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0  | x3 ⇒ pair … true x1
1059    | x4 ⇒ pair … true x2  | x5 ⇒ pair … true x3  | x6 ⇒ pair … true x4  | x7 ⇒ pair … true x5
1060    | x8 ⇒ pair … true x6  | x9 ⇒ pair … true x7  | xA ⇒ pair … true x8  | xB ⇒ pair … true x9
1061    | xC ⇒ pair … true xA  | xD ⇒ pair … true xB  | xE ⇒ pair … true xC  | xF ⇒ pair … true xD ] 
1062   | xF ⇒ match e2 with
1063    [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0  | x2 ⇒ pair … true x1  | x3 ⇒ pair … true x2
1064    | x4 ⇒ pair … true x3  | x5 ⇒ pair … true x4  | x6 ⇒ pair … true x5  | x7 ⇒ pair … true x6
1065    | x8 ⇒ pair … true x7  | x9 ⇒ pair … true x8  | xA ⇒ pair … true x9  | xB ⇒ pair … true xA
1066    | xC ⇒ pair … true xB  | xD ⇒ pair … true xC  | xE ⇒ pair … true xD  | xF ⇒ pair … true xE ]
1067   ].
1068
1069 (* operatore somma con data+carry → data *)
1070 ndefinition plus_ex_dc_d ≝
1071 λc:bool.λe1,e2:exadecim.
1072  match c with
1073   [ true ⇒ match e1 with
1074    [ x0 ⇒ match e2 with
1075     [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1076     | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] 
1077    | x1 ⇒ match e2 with
1078     [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1079     | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] 
1080    | x2 ⇒ match e2 with
1081     [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1082     | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1083    | x3 ⇒ match e2 with
1084     [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1085     | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1086    | x4 ⇒ match e2 with
1087     [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1088     | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1089    | x5 ⇒ match e2 with
1090     [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1091     | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1092    | x6 ⇒ match e2 with
1093     [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1094     | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1095    | x7 ⇒ match e2 with
1096     [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1097     | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1098    | x8 ⇒ match e2 with
1099     [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1100     | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1101    | x9 ⇒ match e2 with
1102     [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1103     | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1104    | xA ⇒ match e2 with
1105     [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1106     | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1107    | xB ⇒ match e2 with
1108     [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1109     | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1110    | xC ⇒ match e2 with
1111      [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1112     | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1113    | xD ⇒ match e2 with
1114     [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1115     | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1116    | xE ⇒ match e2 with
1117     [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1118     | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1119    | xF ⇒ match e2 with
1120     [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1121     | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
1122    ]
1123   | false ⇒ match e1 with
1124    [ x0 ⇒ match e2 with
1125     [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1126     | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] 
1127    | x1 ⇒ match e2 with
1128     [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1129     | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] 
1130    | x2 ⇒ match e2 with
1131     [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1132     | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] 
1133    | x3 ⇒ match e2 with
1134     [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1135     | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1136    | x4 ⇒ match e2 with
1137     [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1138     | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1139    | x5 ⇒ match e2 with
1140     [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1141     | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1142    | x6 ⇒ match e2 with
1143     [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1144     | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1145    | x7 ⇒ match e2 with
1146     [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1147     | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1148    | x8 ⇒ match e2 with
1149     [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1150     | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1151    | x9 ⇒ match e2 with
1152     [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1153     | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1154    | xA ⇒ match e2 with
1155     [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1156     | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1157    | xB ⇒ match e2 with
1158     [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1159     | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1160    | xC ⇒ match e2 with
1161     [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1162     | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1163    | xD ⇒ match e2 with
1164      [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1165     | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1166    | xE ⇒ match e2 with
1167     [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1168     | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1169    | xF ⇒ match e2 with
1170     [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1171     | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1172    ]].
1173
1174 (* operatore somma con data → data *)
1175 ndefinition plus_ex_d_d ≝
1176 λe1,e2:exadecim.
1177  match e1 with
1178   [ x0 ⇒ match e2 with
1179    [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
1180    | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] 
1181   | x1 ⇒ match e2 with
1182    [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1183    | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] 
1184   | x2 ⇒ match e2 with
1185    [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
1186    | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] 
1187   | x3 ⇒ match e2 with
1188    [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
1189    | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
1190   | x4 ⇒ match e2 with
1191    [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
1192    | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
1193   | x5 ⇒ match e2 with
1194    [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
1195    | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
1196   | x6 ⇒ match e2 with
1197    [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
1198    | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
1199   | x7 ⇒ match e2 with
1200    [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
1201    | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
1202   | x8 ⇒ match e2 with
1203    [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
1204    | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
1205   | x9 ⇒ match e2 with
1206    [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
1207    | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
1208   | xA ⇒ match e2 with
1209    [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
1210    | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
1211   | xB ⇒ match e2 with
1212    [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
1213    | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
1214   | xC ⇒ match e2 with
1215    [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
1216    | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
1217   | xD ⇒ match e2 with
1218    [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
1219    | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
1220   | xE ⇒ match e2 with
1221    [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
1222    | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
1223   | xF ⇒ match e2 with
1224    [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1225    | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
1226   ].
1227
1228 (* operatore somma con data+carry → carry *)
1229 ndefinition plus_ex_dc_c ≝
1230 λc:bool.λe1,e2:exadecim.
1231  match c with
1232   [ true ⇒ match e1 with
1233    [ x0 ⇒ match e2 with
1234     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1235     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ] 
1236    | x1 ⇒ match e2 with
1237     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1238     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ] 
1239    | x2 ⇒ match e2 with
1240     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1241     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1242    | x3 ⇒ match e2 with
1243     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1244     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1245    | x4 ⇒ match e2 with
1246     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1247     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1248    | x5 ⇒ match e2 with
1249     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1250     | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1251    | x6 ⇒ match e2 with
1252     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1253     | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1254    | x7 ⇒ match e2 with
1255     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1256     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1257    | x8 ⇒ match e2 with
1258     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1259     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1260    | x9 ⇒ match e2 with
1261     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
1262     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1263    | xA ⇒ match e2 with
1264     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1265     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1266    | xB ⇒ match e2 with
1267     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1268     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1269    | xC ⇒ match e2 with
1270     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1271     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1272    | xD ⇒ match e2 with
1273     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1274     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1275    | xE ⇒ match e2 with
1276     [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1277     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
1278    | xF ⇒ match e2 with
1279     [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1280     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]  
1281    ]
1282   | false ⇒ match e1 with
1283    [ x0 ⇒ match e2 with
1284     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1285     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
1286    | x1 ⇒ match e2 with
1287     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1288     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ] 
1289    | x2 ⇒ match e2 with
1290     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1291     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ] 
1292    | x3 ⇒ match e2 with
1293     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1294     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1295    | x4 ⇒ match e2 with
1296     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1297     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1298    | x5 ⇒ match e2 with
1299     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1300     | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1301    | x6 ⇒ match e2 with
1302     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1303     | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1304    | x7 ⇒ match e2 with
1305     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1306     | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1307    | x8 ⇒ match e2 with
1308     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1309     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1310    | x9 ⇒ match e2 with
1311     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1312     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1313    | xA ⇒ match e2 with
1314     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
1315     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1316    | xB ⇒ match e2 with
1317     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1318     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1319    | xC ⇒ match e2 with
1320     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1321     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1322    | xD ⇒ match e2 with
1323     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1324     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1325    | xE ⇒ match e2 with
1326     [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1327     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1328    | xF ⇒ match e2 with
1329     [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1330     | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1331    ]].
1332
1333 (* operatore somma con data → carry *)
1334 ndefinition plus_ex_d_c ≝
1335 λe1,e2:exadecim.
1336  match e1 with
1337   [ x0 ⇒ match e2 with
1338    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1339    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
1340   | x1 ⇒ match e2 with
1341    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1342    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ] 
1343   | x2 ⇒ match e2 with
1344    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1345    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ] 
1346   | x3 ⇒ match e2 with
1347    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1348    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1349   | x4 ⇒ match e2 with
1350    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1351    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1352   | x5 ⇒ match e2 with
1353    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1354    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1355   | x6 ⇒ match e2 with
1356    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1357    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1358   | x7 ⇒ match e2 with
1359    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1360    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1361   | x8 ⇒ match e2 with
1362    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
1363    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1364   | x9 ⇒ match e2 with
1365    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
1366    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1367   | xA ⇒ match e2 with
1368    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
1369    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1370   | xB ⇒ match e2 with
1371    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1372    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1373   | xC ⇒ match e2 with
1374    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1375    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1376   | xD ⇒ match e2 with
1377    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1378    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1379   | xE ⇒ match e2 with
1380    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1381    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1382   | xF ⇒ match e2 with
1383    [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
1384    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
1385   ].
1386
1387 (* operatore predecessore *)
1388 ndefinition pred_ex ≝
1389 λe:exadecim.
1390  match e with
1391   [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
1392   | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
1393
1394 (* operatore successore *)
1395 ndefinition succ_ex ≝
1396 λe:exadecim.
1397  match e with
1398   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
1399   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
1400
1401 (* operatore neg/complemento a 2 *)
1402 ndefinition compl_ex ≝
1403 λe:exadecim.match e with
1404  [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
1405  | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
1406  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
1407  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
1408
1409 (* operatore abs *)
1410 ndefinition abs_ex ≝
1411 λe:exadecim.match getMSB_ex e with
1412  [ true ⇒ compl_ex e | false ⇒ e ].
1413
1414 (* operatore x in [inf,sup] o in sup],[inf *)
1415 ndefinition inrange_ex ≝
1416 λx,inf,sup:exadecim.
1417  match le_ex inf sup with
1418   [ true ⇒ and_bool | false ⇒ or_bool ]
1419  (le_ex inf x) (le_ex x sup).
1420
1421 (* esadecimali ricorsivi *)
1422 ninductive rec_exadecim : exadecim → Type ≝
1423   ex_O : rec_exadecim x0
1424 | ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
1425
1426 (* esadecimali → esadecimali ricorsivi *)
1427 ndefinition ex_to_recex ≝
1428 λn.match n return λx.rec_exadecim x with
1429  [ x0 ⇒ ex_O
1430  | x1 ⇒ ex_S ? ex_O
1431  | x2 ⇒ ex_S ? (ex_S ? ex_O)
1432  | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
1433  | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
1434  | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
1435  | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
1436  | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
1437  | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
1438  | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
1439  | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
1440  | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))
1441  | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))
1442  | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))
1443  | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))
1444  | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))))
1445  ].
1446
1447 (* quaternari → esadecimali *)
1448 ndefinition ex_of_qu ≝
1449 λn.match n with
1450  [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
1451
1452 (* ottali → esadecimali *)
1453 ndefinition ex_of_oct ≝
1454 λn.match n with
1455  [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
1456
1457 (* esadecimali xNNNN → ottali *)
1458 ndefinition oct_of_exL ≝
1459 λn.match n with
1460   [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
1461   | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
1462
1463 (* esadecimali NNNNx → ottali *)
1464 ndefinition oct_of_exH ≝
1465 λn.match n with
1466   [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3
1467   | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ].