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 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/exadecim.ma".
24 include "num/bitrigesim.ma".
30 nrecord byte8 : Type ≝
37 notation "〈x,y〉" non associative with precedence 80
38 for @{ 'mk_byte8 $x $y }.
39 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
42 ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
46 λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
48 | false ⇒ match gt_ex (b8h b1) (b8h b2) with
50 | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
53 ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2).
56 ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
59 ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
63 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
67 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
71 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
73 (* operatore rotazione destra con carry *)
75 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
76 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
77 [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
79 (* operatore shift destro *)
81 λb:byte8.match rcr_ex (b8h b) false with
82 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
83 [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
85 (* operatore rotazione destra *)
87 λb:byte8.match rcr_ex (b8h b) false with
88 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
89 [ pair bl' c'' ⇒ match c'' with
90 [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
91 | false ⇒ mk_byte8 bh' bl' ]]].
93 (* operatore rotazione destra n-volte *)
94 nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
97 | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
99 (* operatore rotazione sinistra con carry *)
101 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
102 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
103 [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
105 (* operatore shift sinistro *)
107 λb:byte8.match rcl_ex (b8l b) false with
108 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
109 [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
111 (* operatore rotazione sinistra *)
113 λb:byte8.match rcl_ex (b8l b) false with
114 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
115 [ pair bh' c'' ⇒ match c'' with
116 [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
117 | false ⇒ mk_byte8 bh' bl' ]]].
119 (* operatore rotazione sinistra n-volte *)
120 nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
123 | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
125 (* operatore not/complemento a 1 *)
127 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
129 (* operatore somma con data+carry → data+carry *)
130 ndefinition plus_b8_dc_dc ≝
131 λb1,b2:byte8.λc:bool.
132 match plus_ex_dc_dc (b8l b1) (b8l b2) c with
133 [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
134 [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
136 (* operatore somma con data+carry → data *)
137 ndefinition plus_b8_dc_d ≝
138 λb1,b2:byte8.λc:bool.
139 match plus_ex_dc_dc (b8l b1) (b8l b2) c with
140 [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
142 (* operatore somma con data+carry → c *)
143 ndefinition plus_b8_dc_c ≝
144 λb1,b2:byte8.λc:bool.
145 plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
147 (* operatore somma con data → data+carry *)
148 ndefinition plus_b8_d_dc ≝
150 match plus_ex_d_dc (b8l b1) (b8l b2) with
151 [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
152 [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
154 (* operatore somma con data → data *)
155 ndefinition plus_b8_d_d ≝
157 match plus_ex_d_dc (b8l b1) (b8l b2) with
158 [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
160 (* operatore somma con data → c *)
161 ndefinition plus_b8_d_c ≝
163 plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
165 (* operatore Most Significant Bit *)
166 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
168 (* operatore predecessore *)
169 ndefinition pred_b8 ≝
170 λb:byte8.match eq_ex (b8l b) x0 with
171 [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
172 | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
174 (* operatore successore *)
175 ndefinition succ_b8 ≝
176 λb:byte8.match eq_ex (b8l b) xF with
177 [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
178 | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
180 (* operatore neg/complemento a 2 *)
181 ndefinition compl_b8 ≝
182 λb:byte8.match MSB_b8 b with
183 [ true ⇒ succ_b8 (not_b8 b)
184 | false ⇒ not_b8 (pred_b8 b) ].
186 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
188 λe1,e2:exadecim.match e1 with
190 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
191 | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
192 | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
193 | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
195 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
196 | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
197 | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉
198 | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ]
200 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
201 | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
202 | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉
203 | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ]
205 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
206 | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
207 | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉
208 | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ]
210 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
211 | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
212 | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉
213 | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ]
215 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
216 | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
217 | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉
218 | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ]
220 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
221 | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
222 | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉
223 | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ]
225 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
226 | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
227 | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉
228 | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ]
230 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉
231 | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉
232 | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉
233 | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ]
235 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉
236 | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉
237 | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉
238 | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ]
240 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉
241 | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉
242 | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉
243 | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ]
245 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉
246 | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉
247 | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉
248 | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ]
250 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉
251 | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉
252 | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉
253 | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ]
255 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉
256 | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉
257 | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉
258 | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ]
260 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉
261 | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉
262 | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉
263 | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ]
265 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉
266 | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉
267 | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉
268 | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ]
271 (* correzione per somma su BCD *)
272 (* input: halfcarry,carry,X(BCD+BCD) *)
273 (* output: X',carry' *)
276 match lt_b8 X 〈x9,xA〉 with
279 (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
280 [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
282 let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
284 | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
285 let X'' ≝ match c with
286 [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
291 (* X' = [X:0x9A-0xFF]
292 [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
293 [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
295 let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
297 | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
298 let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
302 (* iteratore sui byte *)
303 ndefinition forall_b8 ≝
307 P (mk_byte8 bh bl))).
310 ninductive rec_byte8 : byte8 → Type ≝
311 b8_O : rec_byte8 〈x0,x0〉
312 | b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n).
314 (* byte → byte ricorsivi *)
315 ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝
316 λn.λrecb:rec_byte8 〈n,x0〉.
317 b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (
318 b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))).
320 (* ... cifra esadecimale superiore *)
321 nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
322 match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
324 | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
327 (* ... cifra esadecimale inferiore *)
328 ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
329 λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
330 match n2 return λx.rec_byte8 〈n1,x〉 with
333 | x2 ⇒ b8_S ? (b8_S ? recb)
334 | x3 ⇒ b8_S ? (b8_S ? (b8_S ? recb))
335 | x4 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))
336 | x5 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))
337 | x6 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))
338 | x7 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))
339 | x8 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))
340 | x9 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))
341 | xA ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))
342 | xB ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))
343 | xC ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))
344 | xD ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))
345 | xE ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))))
346 | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
349 ndefinition b8_to_recb8 : Πb.rec_byte8 b.
351 nletin K ≝ (b8_to_recb8_aux3 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
352 nelim b in K:(%) ⊢ %;
353 #e1; #e2; nnormalize; #H; napply H.
356 (* ottali → esadecimali *)
357 ndefinition b8_of_bit ≝
359 [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
360 | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
361 | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
362 | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
363 | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
364 | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
365 | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
366 | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉