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