1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/exadecim.ma".
24 include "num/comp_num.ma".
25 include "num/bitrigesim.ma".
26 include "common/nat.ma".
32 ndefinition byte8 ≝ comp_num exadecim.
33 ndefinition mk_byte8 ≝ λe1,e2.mk_comp_num exadecim e1 e2.
36 notation "〈x,y〉" non associative with precedence 80
37 for @{ mk_comp_num exadecim $x $y }.
39 (* iteratore sui byte *)
40 ndefinition forall_b8 ≝ forall_cn ? forall_ex.
43 ndefinition eq_b8 ≝ eq2_cn ? eq_ex.
46 ndefinition lt_b8 ≝ ltgt_cn ? eq_ex lt_ex.
49 ndefinition le_b8 ≝ lege_cn ? eq_ex lt_ex le_ex.
52 ndefinition gt_b8 ≝ ltgt_cn ? eq_ex gt_ex.
55 ndefinition ge_b8 ≝ lege_cn ? eq_ex gt_ex ge_ex.
58 ndefinition and_b8 ≝ fop2_cn ? and_ex.
61 ndefinition or_b8 ≝ fop2_cn ? or_ex.
64 ndefinition xor_b8 ≝ fop2_cn ? xor_ex.
66 (* operatore Most Significant Bit *)
67 ndefinition getMSB_b8 ≝ getOPH_cn ? getMSB_ex.
68 ndefinition setMSB_b8 ≝ setOPH_cn ? setMSB_ex.
70 (* operatore Least Significant Bit *)
71 ndefinition getLSB_b8 ≝ getOPL_cn ? getLSB_ex.
72 ndefinition setLSB_b8 ≝ setOPL_cn ? setLSB_ex.
74 (* operatore estensione unsigned *)
75 ndefinition extu_b8 ≝ λe2.〈x0,e2〉.
77 (* operatore estensione signed *)
79 λe2.〈(match getMSB_ex e2 with
80 [ true ⇒ xF | false ⇒ x0 ]),e2〉.
82 (* operatore rotazione destra con carry *)
83 ndefinition rcr_b8 ≝ opcr_cn ? rcr_ex.
85 (* operatore shift destro *)
86 ndefinition shr_b8 ≝ opcr_cn ? rcr_ex false.
88 (* operatore rotazione destra *)
90 λb.match shr_b8 b with
91 [ pair c b' ⇒ match c with
92 [ true ⇒ setMSB_b8 b' | false ⇒ b' ]].
94 (* operatore rotazione sinistra con carry *)
95 ndefinition rcl_b8 ≝ opcl_cn ? rcl_ex.
97 (* operatore shift sinistro *)
98 ndefinition shl_b8 ≝ opcl_cn ? rcl_ex false.
100 (* operatore rotazione sinistra *)
102 λb.match shl_b8 b with
103 [ pair c b' ⇒ match c with
104 [ true ⇒ setLSB_b8 b' | false ⇒ b' ]].
106 (* operatore not/complemento a 1 *)
107 ndefinition not_b8 ≝ fop_cn ? not_ex.
109 (* operatore somma con data+carry → data+carry *)
110 ndefinition plus_b8_dc_dc ≝ opcl2_cn ? plus_ex_dc_dc.
112 (* operatore somma con data+carry → data *)
113 ndefinition plus_b8_dc_d ≝ λc,b1,b2.snd … (plus_b8_dc_dc c b1 b2).
115 (* operatore somma con data+carry → c *)
116 ndefinition plus_b8_dc_c ≝ λc,b1,b2.fst … (plus_b8_dc_dc c b1 b2).
118 (* operatore somma con data → data+carry *)
119 ndefinition plus_b8_d_dc ≝ opcl2_cn ? plus_ex_dc_dc false.
121 (* operatore somma con data → data *)
122 ndefinition plus_b8_d_d ≝ λb1,b2.snd … (plus_b8_d_dc b1 b2).
124 (* operatore somma con data → c *)
125 ndefinition plus_b8_d_c ≝ λb1,b2.fst … (plus_b8_d_dc b1 b2).
127 (* operatore predecessore *)
128 ndefinition pred_b8 ≝ predsucc_cn ? (eq_ex x0) pred_ex.
130 (* operatore successore *)
131 ndefinition succ_b8 ≝ predsucc_cn ? (eq_ex xF) succ_ex.
133 (* operatore neg/complemento a 2 *)
134 ndefinition compl_b8 ≝
135 λb:byte8.match getMSB_b8 b with
136 [ true ⇒ succ_b8 (not_b8 b)
137 | false ⇒ not_b8 (pred_b8 b) ].
139 (* operatore x in [inf,sup] o in sup],[inf *)
140 ndefinition inrange_b8 ≝
142 match le_b8 inf sup with
143 [ true ⇒ and_bool | false ⇒ or_bool ]
144 (le_b8 inf x) (le_b8 x sup).
146 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
148 λe1,e2:exadecim.match e1 with
150 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
151 | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
152 | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
153 | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
155 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
156 | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
157 | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉
158 | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ]
160 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
161 | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
162 | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉
163 | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ]
165 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
166 | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
167 | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉
168 | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ]
170 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
171 | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
172 | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉
173 | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ]
175 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
176 | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
177 | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉
178 | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ]
180 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
181 | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
182 | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉
183 | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ]
185 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
186 | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
187 | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉
188 | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ]
190 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉
191 | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉
192 | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉
193 | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ]
195 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉
196 | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉
197 | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉
198 | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ]
200 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉
201 | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉
202 | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉
203 | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ]
205 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉
206 | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉
207 | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉
208 | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ]
210 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉
211 | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉
212 | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉
213 | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ]
215 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉
216 | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉
217 | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉
218 | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ]
220 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉
221 | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉
222 | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉
223 | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ]
225 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉
226 | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉
227 | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉
228 | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ]
231 (* correzione per somma su BCD *)
232 (* input: halfcarry,carry,X(BCD+BCD) *)
233 (* output: X',carry' *)
236 match lt_b8 X 〈x9,xA〉 with
239 (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
240 [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
242 let X' ≝ match (lt_ex (cnL ? X) xA) ⊗ (⊖h) with
244 | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
245 let X'' ≝ match c with
246 [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
251 (* X' = [X:0x9A-0xFF]
252 [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
253 [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
255 let X' ≝ match (lt_ex (cnL ? X) xA) ⊗ (⊖h) with
257 | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
258 let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
262 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
263 nlet rec div_b8_ex_aux (divd:byte8) (divs:byte8) (molt:exadecim) (q:exadecim) (n:nat) on n ≝
264 let w' ≝ plus_b8_d_d divd (compl_b8 divs) in
266 [ O ⇒ match le_b8 divs divd with
267 [ true ⇒ triple … (or_ex molt q) (cnL ? w') (⊖ (eq_ex (cnH ? w') x0))
268 | false ⇒ triple … q (cnL ? divd) (⊖ (eq_ex (cnH ? divd) x0)) ]
269 | S n' ⇒ match le_b8 divs divd with
270 [ true ⇒ div_b8_ex_aux w' (ror_b8 divs) (ror_ex molt) (or_ex molt q) n'
271 | false ⇒ div_b8_ex_aux divd (ror_b8 divs) (ror_ex molt) q n' ]].
273 ndefinition div_b8_ex ≝
274 λb:byte8.λe:exadecim.match eq_ex e x0 with
275 (* la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato *)
276 [ true ⇒ triple … xF (cnL ? b) true
277 | false ⇒ match eq_b8 b 〈x0,x0〉 with
278 (* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
279 [ true ⇒ triple … x0 x0 false
280 (* 1) e' una divisione sensata che produrra' overflow/risultato *)
281 (* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
282 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
283 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
284 (* puo' essere sottratto al dividendo *)
285 | false ⇒ div_b8_ex_aux b (nat_it ? rol_b8 〈x0,e〉 nat3) x8 x0 nat3 ]].
288 ninductive rec_byte8 : byte8 → Type ≝
289 b8_O : rec_byte8 〈x0,x0〉
290 | b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n).
292 (* byte → byte ricorsivi *)
293 ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝
294 λn.λrecb:rec_byte8 〈n,x0〉.
295 b8_S 〈n,xF〉 (b8_S 〈n,xE〉 (b8_S 〈n,xD〉 (b8_S 〈n,xC〉 (
296 b8_S 〈n,xB〉 (b8_S 〈n,xA〉 (b8_S 〈n,x9〉 (b8_S 〈n,x8〉 (
297 b8_S 〈n,x7〉 (b8_S 〈n,x6〉 (b8_S 〈n,x5〉 (b8_S 〈n,x4〉 (
298 b8_S 〈n,x3〉 (b8_S 〈n,x2〉 (b8_S 〈n,x1〉 (b8_S 〈n,x0〉 recb))))))))))))))).
300 (* ... cifra esadecimale superiore *)
301 nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
302 match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
304 | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
307 (* ... cifra esadecimale inferiore *)
308 ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
309 λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
310 match n2 return λx.rec_byte8 〈n1,x〉 with
312 | x1 ⇒ b8_S 〈n1,x0〉 recb
313 | x2 ⇒ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)
314 | x3 ⇒ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))
315 | x4 ⇒ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))
316 | x5 ⇒ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
317 b8_S 〈n1,x0〉 recb))))
318 | x6 ⇒ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
319 b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))
320 | x7 ⇒ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
321 b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))
322 | x8 ⇒ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
323 b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))
324 | x9 ⇒ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
325 b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
326 b8_S 〈n1,x0〉 recb))))))))
327 | xA ⇒ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
328 b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
329 b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))
330 | xB ⇒ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
331 b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
332 b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))
333 | xC ⇒ b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (
334 b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
335 b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))
336 | xD ⇒ b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (
337 b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
338 b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
339 b8_S 〈n1,x0〉 recb))))))))))))
340 | xE ⇒ b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (
341 b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
342 b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
343 b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))))
344 | xF ⇒ b8_S 〈n1,xE〉 (b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (
345 b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
346 b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
347 b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))))))
351 nlemma b8_to_recb8 : Πb.rec_byte8 b.
352 #b; nletin K ≝ (b8_to_recb8_aux3
353 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
354 ncases b in K; #e1; #e2; #K; napply K;
358 ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
360 [ mk_comp_num h l ⇒ b8_to_recb8_aux3 h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
362 (* ottali → esadecimali *)
363 ndefinition b8_of_bit ≝
365 [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
366 | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
367 | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
368 | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
369 | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
370 | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
371 | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
372 | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉