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/byte8.ma".
29 ndefinition word16 ≝ comp_num byte8.
30 ndefinition mk_word16 ≝ λb1,b2.mk_comp_num byte8 b1 b2.
31 ndefinition ext_word16 ≝ λb2.mk_comp_num byte8 〈x0,x0〉 b2.
32 ndefinition ext2_word16 ≝ λe2.mk_comp_num byte8 〈x0,x0〉 〈x0,e2〉.
35 notation "〈x:y〉" non associative with precedence 80
36 for @{ mk_comp_num byte8 $x $y }.
38 (* iteratore sulle word *)
39 ndefinition forall_w16 ≝ forall_cn ? forall_b8.
42 ndefinition eq_w16 ≝ eq2_cn ? eq_b8.
45 ndefinition lt_w16 ≝ ltgt_cn ? eq_b8 lt_b8.
48 ndefinition le_w16 ≝ lege_cn ? eq_b8 lt_b8 le_b8.
51 ndefinition gt_w16 ≝ ltgt_cn ? eq_b8 gt_b8.
54 ndefinition ge_w16 ≝ lege_cn ? eq_b8 gt_b8 ge_b8.
57 ndefinition and_w16 ≝ fop2_cn ? and_b8.
60 ndefinition or_w16 ≝ fop2_cn ? or_b8.
63 ndefinition xor_w16 ≝ fop2_cn ? xor_b8.
65 (* operatore Most Significant Bit *)
66 ndefinition getMSB_w16 ≝ getOPH_cn ? getMSB_b8.
67 ndefinition setMSB_w16 ≝ setOPH_cn ? setMSB_b8.
69 (* operatore Least Significant Bit *)
70 ndefinition getLSB_w16 ≝ getOPL_cn ? getLSB_b8.
71 ndefinition setLSB_w16 ≝ setOPL_cn ? setLSB_b8.
73 (* operatore estensione unsigned *)
74 ndefinition extu_w16 ≝ λb2.〈〈x0,x0〉:b2〉.
75 ndefinition extu2_w16 ≝ λe2.〈〈x0,x0〉:〈x0,e2〉〉.
77 (* operatore estensione signed *)
78 ndefinition exts_w16 ≝
79 λb2.〈(match getMSB_b8 b2 with
80 [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]):b2〉.
81 ndefinition exts2_w16 ≝
82 λe2.(match getMSB_ex e2 with
83 [ true ⇒ 〈〈xF,xF〉:〈xF,e2〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,e2〉〉 ]).
85 (* operatore rotazione destra con carry *)
86 ndefinition rcr_w16 ≝ opcr_cn ? rcr_b8.
88 (* operatore shift destro *)
89 ndefinition shr_w16 ≝ opcr_cn ? rcr_b8 false.
91 (* operatore rotazione destra *)
93 λw.match shr_w16 w with
94 [ pair c w' ⇒ match c with
95 [ true ⇒ setMSB_w16 w' | false ⇒ w' ]].
97 (* operatore rotazione sinistra con carry *)
98 ndefinition rcl_w16 ≝ opcl_cn ? rcl_b8.
100 (* operatore shift sinistro *)
101 ndefinition shl_w16 ≝ opcl_cn ? rcl_b8 false.
103 (* operatore rotazione sinistra *)
104 ndefinition rol_w16 ≝
105 λw.match shl_w16 w with
106 [ pair c w' ⇒ match c with
107 [ true ⇒ setLSB_w16 w' | false ⇒ w' ]].
109 (* operatore not/complemento a 1 *)
110 ndefinition not_w16 ≝ fop_cn ? not_b8.
112 (* operatore somma con data+carry → data+carry *)
113 ndefinition plus_w16_dc_dc ≝ opcl2_cn ? plus_b8_dc_dc.
115 (* operatore somma con data+carry → data *)
116 ndefinition plus_w16_dc_d ≝ λc,w1,w2.snd … (plus_w16_dc_dc c w1 w2).
118 (* operatore somma con data+carry → c *)
119 ndefinition plus_w16_dc_c ≝ λc,w1,w2.fst … (plus_w16_dc_dc c w1 w2).
121 (* operatore somma con data → data+carry *)
122 ndefinition plus_w16_d_dc ≝ opcl2_cn ? plus_b8_dc_dc false.
124 (* operatore somma con data → data *)
125 ndefinition plus_w16_d_d ≝ λw1,w2.snd … (plus_w16_d_dc w1 w2).
127 (* operatore somma con data → c *)
128 ndefinition plus_w16_d_c ≝ λw1,w2.fst … (plus_w16_d_dc w1 w2).
130 (* operatore predecessore *)
131 ndefinition pred_w16 ≝ predsucc_cn ? (eq_b8 〈x0,x0〉) pred_b8.
133 (* operatore successore *)
134 ndefinition succ_w16 ≝ predsucc_cn ? (eq_b8 〈xF,xF〉) succ_b8.
136 (* operatore neg/complemento a 2 *)
137 ndefinition compl_w16 ≝
138 λw:word16.match getMSB_w16 w with
139 [ true ⇒ succ_w16 (not_w16 w)
140 | false ⇒ not_w16 (pred_w16 w) ].
142 (* operatore x in [inf,sup] o in sup],[inf *)
143 ndefinition inrange_w16 ≝
145 match le_w16 inf sup with
146 [ true ⇒ and_bool | false ⇒ or_bool ]
147 (le_w16 inf x) (le_w16 x sup).
149 (* word16 ricorsive *)
150 ninductive rec_word16 : word16 → Type ≝
151 w16_O : rec_word16 〈〈x0,x0〉:〈x0,x0〉〉
152 | w16_S : ∀n.rec_word16 n → rec_word16 (succ_w16 n).
154 (* word16 → word16 ricorsive *)
156 (* EX: ancora problema di tempi ???
157 ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝
158 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
159 w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
160 w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw
164 ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝
165 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
166 w16_S 〈n:〈x0,xF〉〉 (w16_S 〈n:〈x0,xE〉〉 (w16_S 〈n:〈x0,xD〉〉 (w16_S 〈n:〈x0,xC〉〉 (
167 w16_S 〈n:〈x0,xB〉〉 (w16_S 〈n:〈x0,xA〉〉 (w16_S 〈n:〈x0,x9〉〉 (w16_S 〈n:〈x0,x8〉〉 (
168 w16_S 〈n:〈x0,x7〉〉 (w16_S 〈n:〈x0,x6〉〉 (w16_S 〈n:〈x0,x5〉〉 (w16_S 〈n:〈x0,x4〉〉 (
169 w16_S 〈n:〈x0,x3〉〉 (w16_S 〈n:〈x0,x2〉〉 (w16_S 〈n:〈x0,x1〉〉 (w16_S 〈n:〈x0,x0〉〉 recw
172 ndefinition w16_to_recw16_aux1_2 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x2,x0〉〉 ≝
173 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
174 w16_S 〈n:〈x1,xF〉〉 (w16_S 〈n:〈x1,xE〉〉 (w16_S 〈n:〈x1,xD〉〉 (w16_S 〈n:〈x1,xC〉〉 (
175 w16_S 〈n:〈x1,xB〉〉 (w16_S 〈n:〈x1,xA〉〉 (w16_S 〈n:〈x1,x9〉〉 (w16_S 〈n:〈x1,x8〉〉 (
176 w16_S 〈n:〈x1,x7〉〉 (w16_S 〈n:〈x1,x6〉〉 (w16_S 〈n:〈x1,x5〉〉 (w16_S 〈n:〈x1,x4〉〉 (
177 w16_S 〈n:〈x1,x3〉〉 (w16_S 〈n:〈x1,x2〉〉 (w16_S 〈n:〈x1,x1〉〉 (w16_S 〈n:〈x1,x0〉〉 (w16_to_recw16_aux1_1 ? recw)
180 ndefinition w16_to_recw16_aux1_3 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x3,x0〉〉 ≝
181 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
182 w16_S 〈n:〈x2,xF〉〉 (w16_S 〈n:〈x2,xE〉〉 (w16_S 〈n:〈x2,xD〉〉 (w16_S 〈n:〈x2,xC〉〉 (
183 w16_S 〈n:〈x2,xB〉〉 (w16_S 〈n:〈x2,xA〉〉 (w16_S 〈n:〈x2,x9〉〉 (w16_S 〈n:〈x2,x8〉〉 (
184 w16_S 〈n:〈x2,x7〉〉 (w16_S 〈n:〈x2,x6〉〉 (w16_S 〈n:〈x2,x5〉〉 (w16_S 〈n:〈x2,x4〉〉 (
185 w16_S 〈n:〈x2,x3〉〉 (w16_S 〈n:〈x2,x2〉〉 (w16_S 〈n:〈x2,x1〉〉 (w16_S 〈n:〈x2,x0〉〉 (w16_to_recw16_aux1_2 ? recw)
188 ndefinition w16_to_recw16_aux1_4 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x4,x0〉〉 ≝
189 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
190 w16_S 〈n:〈x3,xF〉〉 (w16_S 〈n:〈x3,xE〉〉 (w16_S 〈n:〈x3,xD〉〉 (w16_S 〈n:〈x3,xC〉〉 (
191 w16_S 〈n:〈x3,xB〉〉 (w16_S 〈n:〈x3,xA〉〉 (w16_S 〈n:〈x3,x9〉〉 (w16_S 〈n:〈x3,x8〉〉 (
192 w16_S 〈n:〈x3,x7〉〉 (w16_S 〈n:〈x3,x6〉〉 (w16_S 〈n:〈x3,x5〉〉 (w16_S 〈n:〈x3,x4〉〉 (
193 w16_S 〈n:〈x3,x3〉〉 (w16_S 〈n:〈x3,x2〉〉 (w16_S 〈n:〈x3,x1〉〉 (w16_S 〈n:〈x3,x0〉〉 (w16_to_recw16_aux1_3 ? recw)
196 ndefinition w16_to_recw16_aux1_5 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x5,x0〉〉 ≝
197 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
198 w16_S 〈n:〈x4,xF〉〉 (w16_S 〈n:〈x4,xE〉〉 (w16_S 〈n:〈x4,xD〉〉 (w16_S 〈n:〈x4,xC〉〉 (
199 w16_S 〈n:〈x4,xB〉〉 (w16_S 〈n:〈x4,xA〉〉 (w16_S 〈n:〈x4,x9〉〉 (w16_S 〈n:〈x4,x8〉〉 (
200 w16_S 〈n:〈x4,x7〉〉 (w16_S 〈n:〈x4,x6〉〉 (w16_S 〈n:〈x4,x5〉〉 (w16_S 〈n:〈x4,x4〉〉 (
201 w16_S 〈n:〈x4,x3〉〉 (w16_S 〈n:〈x4,x2〉〉 (w16_S 〈n:〈x4,x1〉〉 (w16_S 〈n:〈x4,x0〉〉 (w16_to_recw16_aux1_4 ? recw)
204 ndefinition w16_to_recw16_aux1_6 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x6,x0〉〉 ≝
205 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
206 w16_S 〈n:〈x5,xF〉〉 (w16_S 〈n:〈x5,xE〉〉 (w16_S 〈n:〈x5,xD〉〉 (w16_S 〈n:〈x5,xC〉〉 (
207 w16_S 〈n:〈x5,xB〉〉 (w16_S 〈n:〈x5,xA〉〉 (w16_S 〈n:〈x5,x9〉〉 (w16_S 〈n:〈x5,x8〉〉 (
208 w16_S 〈n:〈x5,x7〉〉 (w16_S 〈n:〈x5,x6〉〉 (w16_S 〈n:〈x5,x5〉〉 (w16_S 〈n:〈x5,x4〉〉 (
209 w16_S 〈n:〈x5,x3〉〉 (w16_S 〈n:〈x5,x2〉〉 (w16_S 〈n:〈x5,x1〉〉 (w16_S 〈n:〈x5,x0〉〉 (w16_to_recw16_aux1_5 ? recw)
212 ndefinition w16_to_recw16_aux1_7 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x7,x0〉〉 ≝
213 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
214 w16_S 〈n:〈x6,xF〉〉 (w16_S 〈n:〈x6,xE〉〉 (w16_S 〈n:〈x6,xD〉〉 (w16_S 〈n:〈x6,xC〉〉 (
215 w16_S 〈n:〈x6,xB〉〉 (w16_S 〈n:〈x6,xA〉〉 (w16_S 〈n:〈x6,x9〉〉 (w16_S 〈n:〈x6,x8〉〉 (
216 w16_S 〈n:〈x6,x7〉〉 (w16_S 〈n:〈x6,x6〉〉 (w16_S 〈n:〈x6,x5〉〉 (w16_S 〈n:〈x6,x4〉〉 (
217 w16_S 〈n:〈x6,x3〉〉 (w16_S 〈n:〈x6,x2〉〉 (w16_S 〈n:〈x6,x1〉〉 (w16_S 〈n:〈x6,x0〉〉 (w16_to_recw16_aux1_6 ? recw)
220 ndefinition w16_to_recw16_aux1_8 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x8,x0〉〉 ≝
221 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
222 w16_S 〈n:〈x7,xF〉〉 (w16_S 〈n:〈x7,xE〉〉 (w16_S 〈n:〈x7,xD〉〉 (w16_S 〈n:〈x7,xC〉〉 (
223 w16_S 〈n:〈x7,xB〉〉 (w16_S 〈n:〈x7,xA〉〉 (w16_S 〈n:〈x7,x9〉〉 (w16_S 〈n:〈x7,x8〉〉 (
224 w16_S 〈n:〈x7,x7〉〉 (w16_S 〈n:〈x7,x6〉〉 (w16_S 〈n:〈x7,x5〉〉 (w16_S 〈n:〈x7,x4〉〉 (
225 w16_S 〈n:〈x7,x3〉〉 (w16_S 〈n:〈x7,x2〉〉 (w16_S 〈n:〈x7,x1〉〉 (w16_S 〈n:〈x7,x0〉〉 (w16_to_recw16_aux1_7 ? recw)
228 ndefinition w16_to_recw16_aux1_9 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x9,x0〉〉 ≝
229 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
230 w16_S 〈n:〈x8,xF〉〉 (w16_S 〈n:〈x8,xE〉〉 (w16_S 〈n:〈x8,xD〉〉 (w16_S 〈n:〈x8,xC〉〉 (
231 w16_S 〈n:〈x8,xB〉〉 (w16_S 〈n:〈x8,xA〉〉 (w16_S 〈n:〈x8,x9〉〉 (w16_S 〈n:〈x8,x8〉〉 (
232 w16_S 〈n:〈x8,x7〉〉 (w16_S 〈n:〈x8,x6〉〉 (w16_S 〈n:〈x8,x5〉〉 (w16_S 〈n:〈x8,x4〉〉 (
233 w16_S 〈n:〈x8,x3〉〉 (w16_S 〈n:〈x8,x2〉〉 (w16_S 〈n:〈x8,x1〉〉 (w16_S 〈n:〈x8,x0〉〉 (w16_to_recw16_aux1_8 ? recw)
236 ndefinition w16_to_recw16_aux1_10 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xA,x0〉〉 ≝
237 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
238 w16_S 〈n:〈x9,xF〉〉 (w16_S 〈n:〈x9,xE〉〉 (w16_S 〈n:〈x9,xD〉〉 (w16_S 〈n:〈x9,xC〉〉 (
239 w16_S 〈n:〈x9,xB〉〉 (w16_S 〈n:〈x9,xA〉〉 (w16_S 〈n:〈x9,x9〉〉 (w16_S 〈n:〈x9,x8〉〉 (
240 w16_S 〈n:〈x9,x7〉〉 (w16_S 〈n:〈x9,x6〉〉 (w16_S 〈n:〈x9,x5〉〉 (w16_S 〈n:〈x9,x4〉〉 (
241 w16_S 〈n:〈x9,x3〉〉 (w16_S 〈n:〈x9,x2〉〉 (w16_S 〈n:〈x9,x1〉〉 (w16_S 〈n:〈x9,x0〉〉 (w16_to_recw16_aux1_9 ? recw)
244 ndefinition w16_to_recw16_aux1_11 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xB,x0〉〉 ≝
245 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
246 w16_S 〈n:〈xA,xF〉〉 (w16_S 〈n:〈xA,xE〉〉 (w16_S 〈n:〈xA,xD〉〉 (w16_S 〈n:〈xA,xC〉〉 (
247 w16_S 〈n:〈xA,xB〉〉 (w16_S 〈n:〈xA,xA〉〉 (w16_S 〈n:〈xA,x9〉〉 (w16_S 〈n:〈xA,x8〉〉 (
248 w16_S 〈n:〈xA,x7〉〉 (w16_S 〈n:〈xA,x6〉〉 (w16_S 〈n:〈xA,x5〉〉 (w16_S 〈n:〈xA,x4〉〉 (
249 w16_S 〈n:〈xA,x3〉〉 (w16_S 〈n:〈xA,x2〉〉 (w16_S 〈n:〈xA,x1〉〉 (w16_S 〈n:〈xA,x0〉〉 (w16_to_recw16_aux1_10 ? recw)
252 ndefinition w16_to_recw16_aux1_12 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xC,x0〉〉 ≝
253 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
254 w16_S 〈n:〈xB,xF〉〉 (w16_S 〈n:〈xB,xE〉〉 (w16_S 〈n:〈xB,xD〉〉 (w16_S 〈n:〈xB,xC〉〉 (
255 w16_S 〈n:〈xB,xB〉〉 (w16_S 〈n:〈xB,xA〉〉 (w16_S 〈n:〈xB,x9〉〉 (w16_S 〈n:〈xB,x8〉〉 (
256 w16_S 〈n:〈xB,x7〉〉 (w16_S 〈n:〈xB,x6〉〉 (w16_S 〈n:〈xB,x5〉〉 (w16_S 〈n:〈xB,x4〉〉 (
257 w16_S 〈n:〈xB,x3〉〉 (w16_S 〈n:〈xB,x2〉〉 (w16_S 〈n:〈xB,x1〉〉 (w16_S 〈n:〈xB,x0〉〉 (w16_to_recw16_aux1_11 ? recw)
260 ndefinition w16_to_recw16_aux1_13 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xD,x0〉〉 ≝
261 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
262 w16_S 〈n:〈xC,xF〉〉 (w16_S 〈n:〈xC,xE〉〉 (w16_S 〈n:〈xC,xD〉〉 (w16_S 〈n:〈xC,xC〉〉 (
263 w16_S 〈n:〈xC,xB〉〉 (w16_S 〈n:〈xC,xA〉〉 (w16_S 〈n:〈xC,x9〉〉 (w16_S 〈n:〈xC,x8〉〉 (
264 w16_S 〈n:〈xC,x7〉〉 (w16_S 〈n:〈xC,x6〉〉 (w16_S 〈n:〈xC,x5〉〉 (w16_S 〈n:〈xC,x4〉〉 (
265 w16_S 〈n:〈xC,x3〉〉 (w16_S 〈n:〈xC,x2〉〉 (w16_S 〈n:〈xC,x1〉〉 (w16_S 〈n:〈xC,x0〉〉 (w16_to_recw16_aux1_12 ? recw)
268 ndefinition w16_to_recw16_aux1_14 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xE,x0〉〉 ≝
269 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
270 w16_S 〈n:〈xD,xF〉〉 (w16_S 〈n:〈xD,xE〉〉 (w16_S 〈n:〈xD,xD〉〉 (w16_S 〈n:〈xD,xC〉〉 (
271 w16_S 〈n:〈xD,xB〉〉 (w16_S 〈n:〈xD,xA〉〉 (w16_S 〈n:〈xD,x9〉〉 (w16_S 〈n:〈xD,x8〉〉 (
272 w16_S 〈n:〈xD,x7〉〉 (w16_S 〈n:〈xD,x6〉〉 (w16_S 〈n:〈xD,x5〉〉 (w16_S 〈n:〈xD,x4〉〉 (
273 w16_S 〈n:〈xD,x3〉〉 (w16_S 〈n:〈xD,x2〉〉 (w16_S 〈n:〈xD,x1〉〉 (w16_S 〈n:〈xD,x0〉〉 (w16_to_recw16_aux1_13 ? recw)
276 ndefinition w16_to_recw16_aux1_15 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xF,x0〉〉 ≝
277 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
278 w16_S 〈n:〈xE,xF〉〉 (w16_S 〈n:〈xE,xE〉〉 (w16_S 〈n:〈xE,xD〉〉 (w16_S 〈n:〈xE,xC〉〉 (
279 w16_S 〈n:〈xE,xB〉〉 (w16_S 〈n:〈xE,xA〉〉 (w16_S 〈n:〈xE,x9〉〉 (w16_S 〈n:〈xE,x8〉〉 (
280 w16_S 〈n:〈xE,x7〉〉 (w16_S 〈n:〈xE,x6〉〉 (w16_S 〈n:〈xE,x5〉〉 (w16_S 〈n:〈xE,x4〉〉 (
281 w16_S 〈n:〈xE,x3〉〉 (w16_S 〈n:〈xE,x2〉〉 (w16_S 〈n:〈xE,x1〉〉 (w16_S 〈n:〈xE,x0〉〉 (w16_to_recw16_aux1_14 ? recw)
284 ndefinition w16_to_recw16_aux1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈(succ_b8 n):〈x0,x0〉〉 ≝
285 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
286 w16_S 〈n:〈xF,xF〉〉 (w16_S 〈n:〈xF,xE〉〉 (w16_S 〈n:〈xF,xD〉〉 (w16_S 〈n:〈xF,xC〉〉 (
287 w16_S 〈n:〈xF,xB〉〉 (w16_S 〈n:〈xF,xA〉〉 (w16_S 〈n:〈xF,x9〉〉 (w16_S 〈n:〈xF,x8〉〉 (
288 w16_S 〈n:〈xF,x7〉〉 (w16_S 〈n:〈xF,x6〉〉 (w16_S 〈n:〈xF,x5〉〉 (w16_S 〈n:〈xF,x4〉〉 (
289 w16_S 〈n:〈xF,x3〉〉 (w16_S 〈n:〈xF,x2〉〉 (w16_S 〈n:〈xF,x1〉〉 (w16_S 〈n:〈xF,x0〉〉 (w16_to_recw16_aux1_15 ? recw)
292 (* ... cifra byte superiore *)
293 nlet rec w16_to_recw16_aux2 (n:byte8) (r:rec_byte8 n) on r ≝
294 match r return λx.λy:rec_byte8 x.rec_word16 〈x:〈x0,x0〉〉 with
296 | b8_S t n' ⇒ w16_to_recw16_aux1 ? (w16_to_recw16_aux2 t n')
299 (* ... cifra esadecimale n.2 *)
300 ndefinition w16_to_recw16_aux3 ≝
301 λb,n.λrecw:rec_word16 〈b:〈x0,x0〉〉.
302 match n return λx.rec_word16 〈b:〈x,x0〉〉 with
304 | x1 ⇒ w16_to_recw16_aux1_1 ? recw
305 | x2 ⇒ w16_to_recw16_aux1_2 ? recw
306 | x3 ⇒ w16_to_recw16_aux1_3 ? recw
307 | x4 ⇒ w16_to_recw16_aux1_4 ? recw
308 | x5 ⇒ w16_to_recw16_aux1_5 ? recw
309 | x6 ⇒ w16_to_recw16_aux1_6 ? recw
310 | x7 ⇒ w16_to_recw16_aux1_7 ? recw
311 | x8 ⇒ w16_to_recw16_aux1_8 ? recw
312 | x9 ⇒ w16_to_recw16_aux1_9 ? recw
313 | xA ⇒ w16_to_recw16_aux1_10 ? recw
314 | xB ⇒ w16_to_recw16_aux1_11 ? recw
315 | xC ⇒ w16_to_recw16_aux1_12 ? recw
316 | xD ⇒ w16_to_recw16_aux1_13 ? recw
317 | xE ⇒ w16_to_recw16_aux1_14 ? recw
318 | xF ⇒ w16_to_recw16_aux1_15 ? recw
321 ndefinition w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉 ≝
323 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x1〉〉 with
324 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? recw
325 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? recw
326 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? recw
327 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? recw
328 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? recw
329 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? recw
330 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? recw
331 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? recw
332 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? recw
333 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? recw
334 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? recw
335 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? recw
336 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? recw
337 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? recw
338 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? recw
339 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? recw
342 ndefinition w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉 ≝
344 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x2〉〉 with
345 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
346 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
347 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
348 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
349 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
350 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
351 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
352 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
353 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
354 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
355 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
356 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
357 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
358 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
359 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
360 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
363 ndefinition w16_to_recw16_aux4_3 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x3〉〉 ≝
365 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x3〉〉 with
366 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
367 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
368 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
369 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
370 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
371 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
372 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
373 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
374 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
375 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
376 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
377 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
378 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
379 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
380 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
381 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
384 ndefinition w16_to_recw16_aux4_4 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x4〉〉 ≝
386 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x4〉〉 with
387 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
388 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
389 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
390 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
391 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
392 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
393 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
394 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
395 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
396 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
397 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
398 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
399 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
400 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
401 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
402 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
405 ndefinition w16_to_recw16_aux4_5 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x5〉〉 ≝
407 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x5〉〉 with
408 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
409 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
410 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
411 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
412 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
413 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
414 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
415 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
416 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
417 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
418 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
419 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
420 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
421 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
422 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
423 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
426 ndefinition w16_to_recw16_aux4_6 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x6〉〉 ≝
428 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x6〉〉 with
429 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
430 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
431 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
432 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
433 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
434 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
435 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
436 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
437 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
438 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
439 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
440 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
441 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
442 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
443 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
444 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
447 ndefinition w16_to_recw16_aux4_7 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x7〉〉 ≝
449 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x7〉〉 with
450 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
451 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
452 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
453 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
454 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
455 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
456 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
457 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
458 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
459 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
460 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
461 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
462 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
463 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
464 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
465 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
468 ndefinition w16_to_recw16_aux4_8 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x8〉〉 ≝
470 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x8〉〉 with
471 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
472 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
473 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
474 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
475 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
476 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
477 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
478 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
479 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
480 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
481 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
482 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
483 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
484 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
485 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
486 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
489 ndefinition w16_to_recw16_aux4_9 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x9〉〉 ≝
491 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x9〉〉 with
492 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
493 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
494 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
495 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
496 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
497 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
498 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
499 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
500 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
501 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
502 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
503 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
504 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
505 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
506 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
507 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
510 ndefinition w16_to_recw16_aux4_10 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xA〉〉 ≝
512 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xA〉〉 with
513 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
514 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
515 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
516 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
517 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
518 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
519 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
520 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
521 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
522 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
523 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
524 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
525 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
526 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
527 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
528 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
531 ndefinition w16_to_recw16_aux4_11 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xB〉〉 ≝
533 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xB〉〉 with
534 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
535 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
536 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
537 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
538 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
539 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
540 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
541 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
542 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
543 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
544 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
545 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
546 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
547 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
548 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
549 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
552 ndefinition w16_to_recw16_aux4_12 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xC〉〉 ≝
554 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xC〉〉 with
555 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
556 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
557 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
558 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
559 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
560 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
561 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
562 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
563 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
564 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
565 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
566 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
567 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
568 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
569 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
570 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
573 ndefinition w16_to_recw16_aux4_13 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xD〉〉 ≝
575 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xD〉〉 with
576 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
577 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
578 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
579 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
580 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
581 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
582 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
583 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
584 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
585 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
586 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
587 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
588 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
589 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
590 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
591 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
594 ndefinition w16_to_recw16_aux4_14 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xE〉〉 ≝
596 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xE〉〉 with
597 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
598 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
599 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
600 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
601 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
602 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
603 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
604 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
605 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
606 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
607 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
608 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
609 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
610 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
611 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
612 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
615 ndefinition w16_to_recw16_aux4_15 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xF〉〉 ≝
617 match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xF〉〉 with
618 [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
619 | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
620 | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
621 | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
622 | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
623 | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
624 | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
625 | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
626 | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
627 | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
628 | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
629 | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
630 | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
631 | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
632 | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
633 | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
636 (* ... cifra esadecimale n.1 *)
637 ndefinition w16_to_recw16_aux4 ≝
638 λb,e,n.λrecw:rec_word16 〈b:〈e,x0〉〉.
639 match n return λx.rec_word16 〈b:〈e,x〉〉 with
641 | x1 ⇒ w16_to_recw16_aux4_1 … recw
642 | x2 ⇒ w16_to_recw16_aux4_2 … recw
643 | x3 ⇒ w16_to_recw16_aux4_3 … recw
644 | x4 ⇒ w16_to_recw16_aux4_4 … recw
645 | x5 ⇒ w16_to_recw16_aux4_5 … recw
646 | x6 ⇒ w16_to_recw16_aux4_6 … recw
647 | x7 ⇒ w16_to_recw16_aux4_7 … recw
648 | x8 ⇒ w16_to_recw16_aux4_8 … recw
649 | x9 ⇒ w16_to_recw16_aux4_9 … recw
650 | xA ⇒ w16_to_recw16_aux4_10 … recw
651 | xB ⇒ w16_to_recw16_aux4_11 … recw
652 | xC ⇒ w16_to_recw16_aux4_12 … recw
653 | xD ⇒ w16_to_recw16_aux4_13 … recw
654 | xE ⇒ w16_to_recw16_aux4_14 … recw
655 | xF ⇒ w16_to_recw16_aux4_15 … recw
658 ndefinition w16_to_recw16 : Πw.rec_word16 w ≝
660 match w with [ mk_comp_num h l ⇒
661 match l with [ mk_comp_num lh ll ⇒
662 w16_to_recw16_aux4 h lh ll (w16_to_recw16_aux3 h lh (w16_to_recw16_aux2 h (b8_to_recb8 h))) ]].