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 set "baseuri" "cic:/matita/assembly/".
17 include "nat/div_and_mod.ma".
18 include "list/list.ma".
20 notation "14" non associative with precedence 80 for @{ 'x14 }.
21 interpretation "natural number" 'x14 =
22 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
23 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
24 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
25 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
26 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
27 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
28 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
29 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
30 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
31 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
32 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
33 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
34 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
35 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
36 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
38 notation "22" non associative with precedence 80 for @{ 'x22 }.
39 interpretation "natural number" 'x22 =
40 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
41 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
42 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
43 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
44 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
45 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
46 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
47 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
48 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
49 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
50 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
51 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
52 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
53 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
54 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
55 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
56 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
57 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
58 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
59 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
60 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
61 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
62 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
64 notation "30" non associative with precedence 80 for @{ 'x30 }.
65 interpretation "natural number" 'x30 =
66 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
67 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
68 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
69 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
70 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
71 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
72 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
73 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
74 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
75 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
76 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
77 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
78 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
79 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
80 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
81 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
82 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
83 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
84 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
85 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
86 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
87 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
88 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
89 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
90 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
91 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
92 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
93 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
94 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
95 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
96 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))))))))))).
98 notation "31" non associative with precedence 80 for @{ 'x31 }.
99 interpretation "natural number" 'x31 =
100 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
101 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
102 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
103 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
104 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
105 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
106 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
107 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
108 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
109 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
110 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
111 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
112 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
113 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
114 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
115 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
116 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
117 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
118 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
119 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
120 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
121 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
122 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
123 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
124 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
125 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
126 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
127 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
128 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
129 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
130 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
131 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1))))))))))))))))))))))))))))))))).
133 notation "32" non associative with precedence 80 for @{ 'x32 }.
134 interpretation "natural number" 'x32 =
135 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
136 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
137 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
138 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
139 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
140 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
141 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
142 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
143 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
144 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
145 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
146 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
147 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
148 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
149 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
150 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
151 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
152 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
153 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
154 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
155 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
156 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
157 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
158 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
159 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
160 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
161 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
162 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
163 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
164 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
165 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
166 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
167 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))))))))))))).
169 notation "255" non associative with precedence 80 for @{ 'x255 }.
170 interpretation "natural number" 'x255 =
171 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
172 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
173 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
174 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
175 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
176 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
177 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
178 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
179 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
180 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
181 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
182 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
183 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
184 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
185 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
186 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
187 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
188 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
189 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
190 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
191 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
192 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
193 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
194 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
195 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
196 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
197 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
198 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
199 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
200 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
201 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
202 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
203 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
204 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
205 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
206 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
207 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
208 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
209 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
210 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
211 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
212 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
213 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
214 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
215 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
216 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
217 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
218 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
219 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
220 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
221 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
222 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
223 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
224 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
225 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
226 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
227 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
228 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
229 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
230 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
231 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
232 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
233 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
234 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
235 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
236 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
237 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
238 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
239 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
240 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
241 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
242 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
243 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
244 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
245 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
246 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
247 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
248 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
249 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
250 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
251 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
252 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
253 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
254 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
255 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
256 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
257 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
258 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
259 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
260 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
261 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
262 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
263 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
264 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
265 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
266 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
267 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
268 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
269 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
270 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
271 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
272 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
273 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
274 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
275 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
276 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
277 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
278 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
279 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
280 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
281 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
282 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
283 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
284 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
285 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
286 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
287 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
288 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
289 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
290 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
291 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
292 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
293 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
294 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
295 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
296 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
297 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
298 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
299 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
300 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
301 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
302 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
303 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
304 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
305 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
306 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
307 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
308 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
309 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
310 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
311 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
312 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
313 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
314 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
315 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
316 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
317 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
318 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
319 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
320 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
321 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
322 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
323 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
324 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
325 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
326 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
327 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
328 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
329 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
330 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
331 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
332 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
333 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
334 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
335 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
336 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
337 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
338 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
339 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
340 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
341 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
342 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
343 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
344 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
345 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
346 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
347 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
348 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
349 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
350 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
351 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
352 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
353 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
354 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
355 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
356 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
357 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
358 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
359 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
360 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
361 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
362 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
363 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
364 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
365 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
366 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
367 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
368 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
369 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
370 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
371 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
372 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
373 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
374 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
375 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
376 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
377 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
378 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
379 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
380 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
381 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
382 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
383 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
384 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
385 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
386 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
387 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
388 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
389 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
390 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
391 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
392 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
393 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
394 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
395 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
396 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
397 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
398 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
399 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
400 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
401 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
402 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
403 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
404 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
405 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
406 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
407 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
408 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
409 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
410 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
411 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
412 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
413 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
414 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
415 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
416 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
417 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
418 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
419 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
420 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
421 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
422 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
423 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
424 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
425 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
426 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
427 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
428 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
429 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
430 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
432 notation "256" non associative with precedence 80 for @{ 'x256 }.
433 interpretation "natural number" 'x256 =
434 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
435 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
436 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
437 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
438 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
439 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
440 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
441 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
442 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
443 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
444 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
445 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
446 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
447 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
448 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
449 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
450 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
451 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
452 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
453 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
454 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
455 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
456 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
457 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
458 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
459 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
460 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
461 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
462 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
463 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
464 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
465 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
466 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
467 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
468 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
469 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
470 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
471 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
472 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
473 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
474 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
475 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
476 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
477 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
478 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
479 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
480 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
481 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
482 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
483 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
484 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
485 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
486 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
487 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
488 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
489 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
490 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
491 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
492 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
493 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
494 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
495 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
496 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
497 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
498 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
499 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
500 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
501 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
502 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
503 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
504 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
505 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
506 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
507 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
508 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
509 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
510 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
511 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
512 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
513 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
514 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
515 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
516 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
517 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
518 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
519 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
520 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
521 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
522 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
523 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
524 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
525 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
526 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
527 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
528 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
529 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
530 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
531 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
532 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
533 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
534 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
535 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
536 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
537 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
538 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
539 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
540 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
541 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
542 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
543 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
544 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
545 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
546 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
547 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
548 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
549 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
550 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
551 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
552 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
553 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
554 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
555 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
556 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
557 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
558 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
559 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
560 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
561 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
562 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
563 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
564 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
565 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
566 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
567 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
568 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
569 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
570 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
571 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
572 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
573 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
574 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
575 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
576 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
577 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
578 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
579 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
580 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
581 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
582 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
583 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
584 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
585 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
586 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
587 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
588 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
589 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
590 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
591 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
592 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
593 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
594 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
595 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
596 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
597 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
598 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
599 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
600 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
601 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
602 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
603 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
604 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
605 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
606 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
607 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
608 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
609 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
610 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
611 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
612 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
613 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
614 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
615 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
616 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
617 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
618 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
619 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
620 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
621 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
622 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
623 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
624 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
625 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
626 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
627 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
628 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
629 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
630 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
631 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
632 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
633 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
634 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
635 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
636 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
637 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
638 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
639 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
640 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
641 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
642 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
643 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
644 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
645 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
646 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
647 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
648 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
649 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
650 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
651 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
652 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
653 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
654 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
655 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
656 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
657 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
658 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
659 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
660 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
661 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
662 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
663 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
664 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
665 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
666 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
667 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
668 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
669 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
670 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
671 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
672 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
673 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
674 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
675 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
676 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
677 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
678 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
679 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
680 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
681 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
682 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
683 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
684 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
685 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
686 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
687 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
688 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
689 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
690 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
691 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
692 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
693 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
694 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
696 inductive exadecimal : Type ≝
714 record byte : Type ≝ {
724 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
725 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
726 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
727 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
730 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
731 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
732 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
733 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
736 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
737 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
738 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
739 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
742 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
743 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
744 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
745 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
748 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
749 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
750 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
751 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
754 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
755 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
756 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
757 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
760 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
761 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
762 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
763 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
766 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
767 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
768 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
769 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
772 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
773 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
774 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
775 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
778 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
779 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
780 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
781 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
784 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
785 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
786 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
787 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
790 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
791 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
792 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
793 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
796 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
797 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
798 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
799 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
802 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
803 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
804 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
805 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
808 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
809 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
810 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
811 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
814 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
815 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
816 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
817 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]].
821 λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
823 inductive cartesian_product (A,B: Type) : Type ≝
824 couple: ∀a:A.∀b:B. cartesian_product A B.
833 [ x0 ⇒ couple exadecimal bool x1 false
834 | x1 ⇒ couple exadecimal bool x2 false
835 | x2 ⇒ couple exadecimal bool x3 false
836 | x3 ⇒ couple exadecimal bool x4 false
837 | x4 ⇒ couple exadecimal bool x5 false
838 | x5 ⇒ couple exadecimal bool x6 false
839 | x6 ⇒ couple exadecimal bool x7 false
840 | x7 ⇒ couple exadecimal bool x8 false
841 | x8 ⇒ couple exadecimal bool x9 false
842 | x9 ⇒ couple exadecimal bool xA false
843 | xA ⇒ couple exadecimal bool xB false
844 | xB ⇒ couple exadecimal bool xC false
845 | xC ⇒ couple exadecimal bool xD false
846 | xD ⇒ couple exadecimal bool xE false
847 | xE ⇒ couple exadecimal bool xF false
848 | xF ⇒ couple exadecimal bool x0 true ]
851 [ x0 ⇒ couple exadecimal bool x2 false
852 | x1 ⇒ couple exadecimal bool x3 false
853 | x2 ⇒ couple exadecimal bool x4 false
854 | x3 ⇒ couple exadecimal bool x5 false
855 | x4 ⇒ couple exadecimal bool x6 false
856 | x5 ⇒ couple exadecimal bool x7 false
857 | x6 ⇒ couple exadecimal bool x8 false
858 | x7 ⇒ couple exadecimal bool x9 false
859 | x8 ⇒ couple exadecimal bool xA false
860 | x9 ⇒ couple exadecimal bool xB false
861 | xA ⇒ couple exadecimal bool xC false
862 | xB ⇒ couple exadecimal bool xD false
863 | xC ⇒ couple exadecimal bool xE false
864 | xD ⇒ couple exadecimal bool xF false
865 | xE ⇒ couple exadecimal bool x0 true
866 | xF ⇒ couple exadecimal bool x1 true ]
869 [ x0 ⇒ couple exadecimal bool x3 false
870 | x1 ⇒ couple exadecimal bool x4 false
871 | x2 ⇒ couple exadecimal bool x5 false
872 | x3 ⇒ couple exadecimal bool x6 false
873 | x4 ⇒ couple exadecimal bool x7 false
874 | x5 ⇒ couple exadecimal bool x8 false
875 | x6 ⇒ couple exadecimal bool x9 false
876 | x7 ⇒ couple exadecimal bool xA false
877 | x8 ⇒ couple exadecimal bool xB false
878 | x9 ⇒ couple exadecimal bool xC false
879 | xA ⇒ couple exadecimal bool xD false
880 | xB ⇒ couple exadecimal bool xE false
881 | xC ⇒ couple exadecimal bool xF false
882 | xD ⇒ couple exadecimal bool x0 true
883 | xE ⇒ couple exadecimal bool x1 true
884 | xF ⇒ couple exadecimal bool x2 true ]
887 [ x0 ⇒ couple exadecimal bool x4 false
888 | x1 ⇒ couple exadecimal bool x5 false
889 | x2 ⇒ couple exadecimal bool x6 false
890 | x3 ⇒ couple exadecimal bool x7 false
891 | x4 ⇒ couple exadecimal bool x8 false
892 | x5 ⇒ couple exadecimal bool x9 false
893 | x6 ⇒ couple exadecimal bool xA false
894 | x7 ⇒ couple exadecimal bool xB false
895 | x8 ⇒ couple exadecimal bool xC false
896 | x9 ⇒ couple exadecimal bool xD false
897 | xA ⇒ couple exadecimal bool xE false
898 | xB ⇒ couple exadecimal bool xF false
899 | xC ⇒ couple exadecimal bool x0 true
900 | xD ⇒ couple exadecimal bool x1 true
901 | xE ⇒ couple exadecimal bool x2 true
902 | xF ⇒ couple exadecimal bool x3 true ]
905 [ x0 ⇒ couple exadecimal bool x5 false
906 | x1 ⇒ couple exadecimal bool x6 false
907 | x2 ⇒ couple exadecimal bool x7 false
908 | x3 ⇒ couple exadecimal bool x8 false
909 | x4 ⇒ couple exadecimal bool x9 false
910 | x5 ⇒ couple exadecimal bool xA false
911 | x6 ⇒ couple exadecimal bool xB false
912 | x7 ⇒ couple exadecimal bool xC false
913 | x8 ⇒ couple exadecimal bool xD false
914 | x9 ⇒ couple exadecimal bool xE false
915 | xA ⇒ couple exadecimal bool xF false
916 | xB ⇒ couple exadecimal bool x0 true
917 | xC ⇒ couple exadecimal bool x1 true
918 | xD ⇒ couple exadecimal bool x2 true
919 | xE ⇒ couple exadecimal bool x3 true
920 | xF ⇒ couple exadecimal bool x4 true ]
923 [ x0 ⇒ couple exadecimal bool x6 false
924 | x1 ⇒ couple exadecimal bool x7 false
925 | x2 ⇒ couple exadecimal bool x8 false
926 | x3 ⇒ couple exadecimal bool x9 false
927 | x4 ⇒ couple exadecimal bool xA false
928 | x5 ⇒ couple exadecimal bool xB false
929 | x6 ⇒ couple exadecimal bool xC false
930 | x7 ⇒ couple exadecimal bool xD false
931 | x8 ⇒ couple exadecimal bool xE false
932 | x9 ⇒ couple exadecimal bool xF false
933 | xA ⇒ couple exadecimal bool x0 true
934 | xB ⇒ couple exadecimal bool x1 true
935 | xC ⇒ couple exadecimal bool x2 true
936 | xD ⇒ couple exadecimal bool x3 true
937 | xE ⇒ couple exadecimal bool x4 true
938 | xF ⇒ couple exadecimal bool x5 true ]
941 [ x0 ⇒ couple exadecimal bool x7 false
942 | x1 ⇒ couple exadecimal bool x8 false
943 | x2 ⇒ couple exadecimal bool x9 false
944 | x3 ⇒ couple exadecimal bool xA false
945 | x4 ⇒ couple exadecimal bool xB false
946 | x5 ⇒ couple exadecimal bool xC false
947 | x6 ⇒ couple exadecimal bool xD false
948 | x7 ⇒ couple exadecimal bool xE false
949 | x8 ⇒ couple exadecimal bool xF false
950 | x9 ⇒ couple exadecimal bool x0 true
951 | xA ⇒ couple exadecimal bool x1 true
952 | xB ⇒ couple exadecimal bool x2 true
953 | xC ⇒ couple exadecimal bool x3 true
954 | xD ⇒ couple exadecimal bool x4 true
955 | xE ⇒ couple exadecimal bool x5 true
956 | xF ⇒ couple exadecimal bool x6 true ]
959 [ x0 ⇒ couple exadecimal bool x8 false
960 | x1 ⇒ couple exadecimal bool x9 false
961 | x2 ⇒ couple exadecimal bool xA false
962 | x3 ⇒ couple exadecimal bool xB false
963 | x4 ⇒ couple exadecimal bool xC false
964 | x5 ⇒ couple exadecimal bool xD false
965 | x6 ⇒ couple exadecimal bool xE false
966 | x7 ⇒ couple exadecimal bool xF false
967 | x8 ⇒ couple exadecimal bool x0 true
968 | x9 ⇒ couple exadecimal bool x1 true
969 | xA ⇒ couple exadecimal bool x2 true
970 | xB ⇒ couple exadecimal bool x3 true
971 | xC ⇒ couple exadecimal bool x4 true
972 | xD ⇒ couple exadecimal bool x5 true
973 | xE ⇒ couple exadecimal bool x6 true
974 | xF ⇒ couple exadecimal bool x7 true ]
977 [ x0 ⇒ couple exadecimal bool x9 false
978 | x1 ⇒ couple exadecimal bool xA false
979 | x2 ⇒ couple exadecimal bool xB false
980 | x3 ⇒ couple exadecimal bool xC false
981 | x4 ⇒ couple exadecimal bool xD false
982 | x5 ⇒ couple exadecimal bool xE false
983 | x6 ⇒ couple exadecimal bool xF false
984 | x7 ⇒ couple exadecimal bool x0 true
985 | x8 ⇒ couple exadecimal bool x1 true
986 | x9 ⇒ couple exadecimal bool x2 true
987 | xA ⇒ couple exadecimal bool x3 true
988 | xB ⇒ couple exadecimal bool x4 true
989 | xC ⇒ couple exadecimal bool x5 true
990 | xD ⇒ couple exadecimal bool x6 true
991 | xE ⇒ couple exadecimal bool x7 true
992 | xF ⇒ couple exadecimal bool x8 true ]
995 [ x0 ⇒ couple exadecimal bool xA false
996 | x1 ⇒ couple exadecimal bool xB false
997 | x2 ⇒ couple exadecimal bool xC false
998 | x3 ⇒ couple exadecimal bool xD false
999 | x4 ⇒ couple exadecimal bool xE false
1000 | x5 ⇒ couple exadecimal bool xF false
1001 | x6 ⇒ couple exadecimal bool x0 true
1002 | x7 ⇒ couple exadecimal bool x1 true
1003 | x8 ⇒ couple exadecimal bool x2 true
1004 | x9 ⇒ couple exadecimal bool x3 true
1005 | xA ⇒ couple exadecimal bool x4 true
1006 | xB ⇒ couple exadecimal bool x5 true
1007 | xC ⇒ couple exadecimal bool x6 true
1008 | xD ⇒ couple exadecimal bool x7 true
1009 | xE ⇒ couple exadecimal bool x8 true
1010 | xF ⇒ couple exadecimal bool x9 true ]
1013 [ x0 ⇒ couple exadecimal bool xB false
1014 | x1 ⇒ couple exadecimal bool xC false
1015 | x2 ⇒ couple exadecimal bool xD false
1016 | x3 ⇒ couple exadecimal bool xE false
1017 | x4 ⇒ couple exadecimal bool xF false
1018 | x5 ⇒ couple exadecimal bool x0 true
1019 | x6 ⇒ couple exadecimal bool x1 true
1020 | x7 ⇒ couple exadecimal bool x2 true
1021 | x8 ⇒ couple exadecimal bool x3 true
1022 | x9 ⇒ couple exadecimal bool x4 true
1023 | xA ⇒ couple exadecimal bool x5 true
1024 | xB ⇒ couple exadecimal bool x6 true
1025 | xC ⇒ couple exadecimal bool x7 true
1026 | xD ⇒ couple exadecimal bool x8 true
1027 | xE ⇒ couple exadecimal bool x9 true
1028 | xF ⇒ couple exadecimal bool xA true ]
1031 [ x0 ⇒ couple exadecimal bool xC false
1032 | x1 ⇒ couple exadecimal bool xD false
1033 | x2 ⇒ couple exadecimal bool xE false
1034 | x3 ⇒ couple exadecimal bool xF false
1035 | x4 ⇒ couple exadecimal bool x0 true
1036 | x5 ⇒ couple exadecimal bool x1 true
1037 | x6 ⇒ couple exadecimal bool x2 true
1038 | x7 ⇒ couple exadecimal bool x3 true
1039 | x8 ⇒ couple exadecimal bool x4 true
1040 | x9 ⇒ couple exadecimal bool x5 true
1041 | xA ⇒ couple exadecimal bool x6 true
1042 | xB ⇒ couple exadecimal bool x7 true
1043 | xC ⇒ couple exadecimal bool x8 true
1044 | xD ⇒ couple exadecimal bool x9 true
1045 | xE ⇒ couple exadecimal bool xA true
1046 | xF ⇒ couple exadecimal bool xB true ]
1049 [ x0 ⇒ couple exadecimal bool xD false
1050 | x1 ⇒ couple exadecimal bool xE false
1051 | x2 ⇒ couple exadecimal bool xF false
1052 | x3 ⇒ couple exadecimal bool x0 true
1053 | x4 ⇒ couple exadecimal bool x1 true
1054 | x5 ⇒ couple exadecimal bool x2 true
1055 | x6 ⇒ couple exadecimal bool x3 true
1056 | x7 ⇒ couple exadecimal bool x4 true
1057 | x8 ⇒ couple exadecimal bool x5 true
1058 | x9 ⇒ couple exadecimal bool x6 true
1059 | xA ⇒ couple exadecimal bool x7 true
1060 | xB ⇒ couple exadecimal bool x8 true
1061 | xC ⇒ couple exadecimal bool x9 true
1062 | xD ⇒ couple exadecimal bool xA true
1063 | xE ⇒ couple exadecimal bool xB true
1064 | xF ⇒ couple exadecimal bool xC true ]
1067 [ x0 ⇒ couple exadecimal bool xE false
1068 | x1 ⇒ couple exadecimal bool xF false
1069 | x2 ⇒ couple exadecimal bool x0 true
1070 | x3 ⇒ couple exadecimal bool x1 true
1071 | x4 ⇒ couple exadecimal bool x2 true
1072 | x5 ⇒ couple exadecimal bool x3 true
1073 | x6 ⇒ couple exadecimal bool x4 true
1074 | x7 ⇒ couple exadecimal bool x5 true
1075 | x8 ⇒ couple exadecimal bool x6 true
1076 | x9 ⇒ couple exadecimal bool x7 true
1077 | xA ⇒ couple exadecimal bool x8 true
1078 | xB ⇒ couple exadecimal bool x9 true
1079 | xC ⇒ couple exadecimal bool xA true
1080 | xD ⇒ couple exadecimal bool xB true
1081 | xE ⇒ couple exadecimal bool xC true
1082 | xF ⇒ couple exadecimal bool xD true ]
1085 [ x0 ⇒ couple exadecimal bool xF false
1086 | x1 ⇒ couple exadecimal bool x0 true
1087 | x2 ⇒ couple exadecimal bool x1 true
1088 | x3 ⇒ couple exadecimal bool x2 true
1089 | x4 ⇒ couple exadecimal bool x3 true
1090 | x5 ⇒ couple exadecimal bool x4 true
1091 | x6 ⇒ couple exadecimal bool x5 true
1092 | x7 ⇒ couple exadecimal bool x6 true
1093 | x8 ⇒ couple exadecimal bool x7 true
1094 | x9 ⇒ couple exadecimal bool x8 true
1095 | xA ⇒ couple exadecimal bool x9 true
1096 | xB ⇒ couple exadecimal bool xA true
1097 | xC ⇒ couple exadecimal bool xB true
1098 | xD ⇒ couple exadecimal bool xC true
1099 | xE ⇒ couple exadecimal bool xD true
1100 | xF ⇒ couple exadecimal bool xE true ]
1103 [ x0 ⇒ couple exadecimal bool x0 true
1104 | x1 ⇒ couple exadecimal bool x1 true
1105 | x2 ⇒ couple exadecimal bool x2 true
1106 | x3 ⇒ couple exadecimal bool x3 true
1107 | x4 ⇒ couple exadecimal bool x4 true
1108 | x5 ⇒ couple exadecimal bool x5 true
1109 | x6 ⇒ couple exadecimal bool x6 true
1110 | x7 ⇒ couple exadecimal bool x7 true
1111 | x8 ⇒ couple exadecimal bool x8 true
1112 | x9 ⇒ couple exadecimal bool x9 true
1113 | xA ⇒ couple exadecimal bool xA true
1114 | xB ⇒ couple exadecimal bool xB true
1115 | xC ⇒ couple exadecimal bool xC true
1116 | xD ⇒ couple exadecimal bool xD true
1117 | xE ⇒ couple exadecimal bool xE true
1118 | xF ⇒ couple exadecimal bool xF true ]
1124 [ x0 ⇒ couple exadecimal bool x0 false
1125 | x1 ⇒ couple exadecimal bool x1 false
1126 | x2 ⇒ couple exadecimal bool x2 false
1127 | x3 ⇒ couple exadecimal bool x3 false
1128 | x4 ⇒ couple exadecimal bool x4 false
1129 | x5 ⇒ couple exadecimal bool x5 false
1130 | x6 ⇒ couple exadecimal bool x6 false
1131 | x7 ⇒ couple exadecimal bool x7 false
1132 | x8 ⇒ couple exadecimal bool x8 false
1133 | x9 ⇒ couple exadecimal bool x9 false
1134 | xA ⇒ couple exadecimal bool xA false
1135 | xB ⇒ couple exadecimal bool xB false
1136 | xC ⇒ couple exadecimal bool xC false
1137 | xD ⇒ couple exadecimal bool xD false
1138 | xE ⇒ couple exadecimal bool xE false
1139 | xF ⇒ couple exadecimal bool xF false ]
1142 [ x0 ⇒ couple exadecimal bool x1 false
1143 | x1 ⇒ couple exadecimal bool x2 false
1144 | x2 ⇒ couple exadecimal bool x3 false
1145 | x3 ⇒ couple exadecimal bool x4 false
1146 | x4 ⇒ couple exadecimal bool x5 false
1147 | x5 ⇒ couple exadecimal bool x6 false
1148 | x6 ⇒ couple exadecimal bool x7 false
1149 | x7 ⇒ couple exadecimal bool x8 false
1150 | x8 ⇒ couple exadecimal bool x9 false
1151 | x9 ⇒ couple exadecimal bool xA false
1152 | xA ⇒ couple exadecimal bool xB false
1153 | xB ⇒ couple exadecimal bool xC false
1154 | xC ⇒ couple exadecimal bool xD false
1155 | xD ⇒ couple exadecimal bool xE false
1156 | xE ⇒ couple exadecimal bool xF false
1157 | xF ⇒ couple exadecimal bool x0 true ]
1160 [ x0 ⇒ couple exadecimal bool x2 false
1161 | x1 ⇒ couple exadecimal bool x3 false
1162 | x2 ⇒ couple exadecimal bool x4 false
1163 | x3 ⇒ couple exadecimal bool x5 false
1164 | x4 ⇒ couple exadecimal bool x6 false
1165 | x5 ⇒ couple exadecimal bool x7 false
1166 | x6 ⇒ couple exadecimal bool x8 false
1167 | x7 ⇒ couple exadecimal bool x9 false
1168 | x8 ⇒ couple exadecimal bool xA false
1169 | x9 ⇒ couple exadecimal bool xB false
1170 | xA ⇒ couple exadecimal bool xC false
1171 | xB ⇒ couple exadecimal bool xD false
1172 | xC ⇒ couple exadecimal bool xE false
1173 | xD ⇒ couple exadecimal bool xF false
1174 | xE ⇒ couple exadecimal bool x0 true
1175 | xF ⇒ couple exadecimal bool x1 true ]
1178 [ x0 ⇒ couple exadecimal bool x3 false
1179 | x1 ⇒ couple exadecimal bool x4 false
1180 | x2 ⇒ couple exadecimal bool x5 false
1181 | x3 ⇒ couple exadecimal bool x6 false
1182 | x4 ⇒ couple exadecimal bool x7 false
1183 | x5 ⇒ couple exadecimal bool x8 false
1184 | x6 ⇒ couple exadecimal bool x9 false
1185 | x7 ⇒ couple exadecimal bool xA false
1186 | x8 ⇒ couple exadecimal bool xB false
1187 | x9 ⇒ couple exadecimal bool xC false
1188 | xA ⇒ couple exadecimal bool xD false
1189 | xB ⇒ couple exadecimal bool xE false
1190 | xC ⇒ couple exadecimal bool xF false
1191 | xD ⇒ couple exadecimal bool x0 true
1192 | xE ⇒ couple exadecimal bool x1 true
1193 | xF ⇒ couple exadecimal bool x2 true ]
1196 [ x0 ⇒ couple exadecimal bool x4 false
1197 | x1 ⇒ couple exadecimal bool x5 false
1198 | x2 ⇒ couple exadecimal bool x6 false
1199 | x3 ⇒ couple exadecimal bool x7 false
1200 | x4 ⇒ couple exadecimal bool x8 false
1201 | x5 ⇒ couple exadecimal bool x9 false
1202 | x6 ⇒ couple exadecimal bool xA false
1203 | x7 ⇒ couple exadecimal bool xB false
1204 | x8 ⇒ couple exadecimal bool xC false
1205 | x9 ⇒ couple exadecimal bool xD false
1206 | xA ⇒ couple exadecimal bool xE false
1207 | xB ⇒ couple exadecimal bool xF false
1208 | xC ⇒ couple exadecimal bool x0 true
1209 | xD ⇒ couple exadecimal bool x1 true
1210 | xE ⇒ couple exadecimal bool x2 true
1211 | xF ⇒ couple exadecimal bool x3 true ]
1214 [ x0 ⇒ couple exadecimal bool x5 false
1215 | x1 ⇒ couple exadecimal bool x6 false
1216 | x2 ⇒ couple exadecimal bool x7 false
1217 | x3 ⇒ couple exadecimal bool x8 false
1218 | x4 ⇒ couple exadecimal bool x9 false
1219 | x5 ⇒ couple exadecimal bool xA false
1220 | x6 ⇒ couple exadecimal bool xB false
1221 | x7 ⇒ couple exadecimal bool xC false
1222 | x8 ⇒ couple exadecimal bool xD false
1223 | x9 ⇒ couple exadecimal bool xE false
1224 | xA ⇒ couple exadecimal bool xF false
1225 | xB ⇒ couple exadecimal bool x0 true
1226 | xC ⇒ couple exadecimal bool x1 true
1227 | xD ⇒ couple exadecimal bool x2 true
1228 | xE ⇒ couple exadecimal bool x3 true
1229 | xF ⇒ couple exadecimal bool x4 true ]
1232 [ x0 ⇒ couple exadecimal bool x6 false
1233 | x1 ⇒ couple exadecimal bool x7 false
1234 | x2 ⇒ couple exadecimal bool x8 false
1235 | x3 ⇒ couple exadecimal bool x9 false
1236 | x4 ⇒ couple exadecimal bool xA false
1237 | x5 ⇒ couple exadecimal bool xB false
1238 | x6 ⇒ couple exadecimal bool xC false
1239 | x7 ⇒ couple exadecimal bool xD false
1240 | x8 ⇒ couple exadecimal bool xE false
1241 | x9 ⇒ couple exadecimal bool xF false
1242 | xA ⇒ couple exadecimal bool x0 true
1243 | xB ⇒ couple exadecimal bool x1 true
1244 | xC ⇒ couple exadecimal bool x2 true
1245 | xD ⇒ couple exadecimal bool x3 true
1246 | xE ⇒ couple exadecimal bool x4 true
1247 | xF ⇒ couple exadecimal bool x5 true ]
1250 [ x0 ⇒ couple exadecimal bool x7 false
1251 | x1 ⇒ couple exadecimal bool x8 false
1252 | x2 ⇒ couple exadecimal bool x9 false
1253 | x3 ⇒ couple exadecimal bool xA false
1254 | x4 ⇒ couple exadecimal bool xB false
1255 | x5 ⇒ couple exadecimal bool xC false
1256 | x6 ⇒ couple exadecimal bool xD false
1257 | x7 ⇒ couple exadecimal bool xE false
1258 | x8 ⇒ couple exadecimal bool xF false
1259 | x9 ⇒ couple exadecimal bool x0 true
1260 | xA ⇒ couple exadecimal bool x1 true
1261 | xB ⇒ couple exadecimal bool x2 true
1262 | xC ⇒ couple exadecimal bool x3 true
1263 | xD ⇒ couple exadecimal bool x4 true
1264 | xE ⇒ couple exadecimal bool x5 true
1265 | xF ⇒ couple exadecimal bool x6 true ]
1268 [ x0 ⇒ couple exadecimal bool x8 false
1269 | x1 ⇒ couple exadecimal bool x9 false
1270 | x2 ⇒ couple exadecimal bool xA false
1271 | x3 ⇒ couple exadecimal bool xB false
1272 | x4 ⇒ couple exadecimal bool xC false
1273 | x5 ⇒ couple exadecimal bool xD false
1274 | x6 ⇒ couple exadecimal bool xE false
1275 | x7 ⇒ couple exadecimal bool xF false
1276 | x8 ⇒ couple exadecimal bool x0 true
1277 | x9 ⇒ couple exadecimal bool x1 true
1278 | xA ⇒ couple exadecimal bool x2 true
1279 | xB ⇒ couple exadecimal bool x3 true
1280 | xC ⇒ couple exadecimal bool x4 true
1281 | xD ⇒ couple exadecimal bool x5 true
1282 | xE ⇒ couple exadecimal bool x6 true
1283 | xF ⇒ couple exadecimal bool x7 true ]
1286 [ x0 ⇒ couple exadecimal bool x9 false
1287 | x1 ⇒ couple exadecimal bool xA false
1288 | x2 ⇒ couple exadecimal bool xB false
1289 | x3 ⇒ couple exadecimal bool xC false
1290 | x4 ⇒ couple exadecimal bool xD false
1291 | x5 ⇒ couple exadecimal bool xE false
1292 | x6 ⇒ couple exadecimal bool xF false
1293 | x7 ⇒ couple exadecimal bool x0 true
1294 | x8 ⇒ couple exadecimal bool x1 true
1295 | x9 ⇒ couple exadecimal bool x2 true
1296 | xA ⇒ couple exadecimal bool x3 true
1297 | xB ⇒ couple exadecimal bool x4 true
1298 | xC ⇒ couple exadecimal bool x5 true
1299 | xD ⇒ couple exadecimal bool x6 true
1300 | xE ⇒ couple exadecimal bool x7 true
1301 | xF ⇒ couple exadecimal bool x8 true ]
1304 [ x0 ⇒ couple exadecimal bool xA false
1305 | x1 ⇒ couple exadecimal bool xB false
1306 | x2 ⇒ couple exadecimal bool xC false
1307 | x3 ⇒ couple exadecimal bool xD false
1308 | x4 ⇒ couple exadecimal bool xE false
1309 | x5 ⇒ couple exadecimal bool xF false
1310 | x6 ⇒ couple exadecimal bool x0 true
1311 | x7 ⇒ couple exadecimal bool x1 true
1312 | x8 ⇒ couple exadecimal bool x2 true
1313 | x9 ⇒ couple exadecimal bool x3 true
1314 | xA ⇒ couple exadecimal bool x4 true
1315 | xB ⇒ couple exadecimal bool x5 true
1316 | xC ⇒ couple exadecimal bool x6 true
1317 | xD ⇒ couple exadecimal bool x7 true
1318 | xE ⇒ couple exadecimal bool x8 true
1319 | xF ⇒ couple exadecimal bool x9 true ]
1322 [ x0 ⇒ couple exadecimal bool xB false
1323 | x1 ⇒ couple exadecimal bool xC false
1324 | x2 ⇒ couple exadecimal bool xD false
1325 | x3 ⇒ couple exadecimal bool xE false
1326 | x4 ⇒ couple exadecimal bool xF false
1327 | x5 ⇒ couple exadecimal bool x0 true
1328 | x6 ⇒ couple exadecimal bool x1 true
1329 | x7 ⇒ couple exadecimal bool x2 true
1330 | x8 ⇒ couple exadecimal bool x3 true
1331 | x9 ⇒ couple exadecimal bool x4 true
1332 | xA ⇒ couple exadecimal bool x5 true
1333 | xB ⇒ couple exadecimal bool x6 true
1334 | xC ⇒ couple exadecimal bool x7 true
1335 | xD ⇒ couple exadecimal bool x8 true
1336 | xE ⇒ couple exadecimal bool x9 true
1337 | xF ⇒ couple exadecimal bool xA true ]
1340 [ x0 ⇒ couple exadecimal bool xC false
1341 | x1 ⇒ couple exadecimal bool xD false
1342 | x2 ⇒ couple exadecimal bool xE false
1343 | x3 ⇒ couple exadecimal bool xF false
1344 | x4 ⇒ couple exadecimal bool x0 true
1345 | x5 ⇒ couple exadecimal bool x1 true
1346 | x6 ⇒ couple exadecimal bool x2 true
1347 | x7 ⇒ couple exadecimal bool x3 true
1348 | x8 ⇒ couple exadecimal bool x4 true
1349 | x9 ⇒ couple exadecimal bool x5 true
1350 | xA ⇒ couple exadecimal bool x6 true
1351 | xB ⇒ couple exadecimal bool x7 true
1352 | xC ⇒ couple exadecimal bool x8 true
1353 | xD ⇒ couple exadecimal bool x9 true
1354 | xE ⇒ couple exadecimal bool xA true
1355 | xF ⇒ couple exadecimal bool xB true ]
1358 [ x0 ⇒ couple exadecimal bool xD false
1359 | x1 ⇒ couple exadecimal bool xE false
1360 | x2 ⇒ couple exadecimal bool xF false
1361 | x3 ⇒ couple exadecimal bool x0 true
1362 | x4 ⇒ couple exadecimal bool x1 true
1363 | x5 ⇒ couple exadecimal bool x2 true
1364 | x6 ⇒ couple exadecimal bool x3 true
1365 | x7 ⇒ couple exadecimal bool x4 true
1366 | x8 ⇒ couple exadecimal bool x5 true
1367 | x9 ⇒ couple exadecimal bool x6 true
1368 | xA ⇒ couple exadecimal bool x7 true
1369 | xB ⇒ couple exadecimal bool x8 true
1370 | xC ⇒ couple exadecimal bool x9 true
1371 | xD ⇒ couple exadecimal bool xA true
1372 | xE ⇒ couple exadecimal bool xB true
1373 | xF ⇒ couple exadecimal bool xC true ]
1376 [ x0 ⇒ couple exadecimal bool xE false
1377 | x1 ⇒ couple exadecimal bool xF false
1378 | x2 ⇒ couple exadecimal bool x0 true
1379 | x3 ⇒ couple exadecimal bool x1 true
1380 | x4 ⇒ couple exadecimal bool x2 true
1381 | x5 ⇒ couple exadecimal bool x3 true
1382 | x6 ⇒ couple exadecimal bool x4 true
1383 | x7 ⇒ couple exadecimal bool x5 true
1384 | x8 ⇒ couple exadecimal bool x6 true
1385 | x9 ⇒ couple exadecimal bool x7 true
1386 | xA ⇒ couple exadecimal bool x8 true
1387 | xB ⇒ couple exadecimal bool x9 true
1388 | xC ⇒ couple exadecimal bool xA true
1389 | xD ⇒ couple exadecimal bool xB true
1390 | xE ⇒ couple exadecimal bool xC true
1391 | xF ⇒ couple exadecimal bool xD true ]
1394 [ x0 ⇒ couple exadecimal bool xF false
1395 | x1 ⇒ couple exadecimal bool x0 true
1396 | x2 ⇒ couple exadecimal bool x1 true
1397 | x3 ⇒ couple exadecimal bool x2 true
1398 | x4 ⇒ couple exadecimal bool x3 true
1399 | x5 ⇒ couple exadecimal bool x4 true
1400 | x6 ⇒ couple exadecimal bool x5 true
1401 | x7 ⇒ couple exadecimal bool x6 true
1402 | x8 ⇒ couple exadecimal bool x7 true
1403 | x9 ⇒ couple exadecimal bool x8 true
1404 | xA ⇒ couple exadecimal bool x9 true
1405 | xB ⇒ couple exadecimal bool xA true
1406 | xC ⇒ couple exadecimal bool xB true
1407 | xD ⇒ couple exadecimal bool xC true
1408 | xE ⇒ couple exadecimal bool xD true
1409 | xF ⇒ couple exadecimal bool xE true ]
1414 definition plusbyte ≝
1416 match plusex (bl b1) (bl b2) c with
1418 match plusex (bh b1) (bh b2) c' with
1419 [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
1421 alias num (instance 0) = "natural number".
1422 definition nat_of_exadecimal ≝
1443 coercion cic:/matita/assembly/nat_of_exadecimal.con.
1445 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
1447 coercion cic:/matita/assembly/nat_of_byte.con.
1449 let rec exadecimal_of_nat b ≝
1450 match b with [ O ⇒ x0 | S b ⇒
1451 match b with [ O ⇒ x1 | S b ⇒
1452 match b with [ O ⇒ x2 | S b ⇒
1453 match b with [ O ⇒ x3 | S b ⇒
1454 match b with [ O ⇒ x4 | S b ⇒
1455 match b with [ O ⇒ x5 | S b ⇒
1456 match b with [ O ⇒ x6 | S b ⇒
1457 match b with [ O ⇒ x7 | S b ⇒
1458 match b with [ O ⇒ x8 | S b ⇒
1459 match b with [ O ⇒ x9 | S b ⇒
1460 match b with [ O ⇒ xA | S b ⇒
1461 match b with [ O ⇒ xB | S b ⇒
1462 match b with [ O ⇒ xC | S b ⇒
1463 match b with [ O ⇒ xD | S b ⇒
1464 match b with [ O ⇒ xE | S b ⇒
1465 match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
1467 definition byte_of_nat ≝
1468 λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
1470 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
1478 axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
1483 definition nat_of_bool ≝
1484 λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
1486 (* Way too slow. Handles 2^32 goals!
1489 match plusbyte b1 b2 c with
1490 [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
1505 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1506 intros; elim n; [ reflexivity | unfold byte_of_nat.
1510 definition addr ≝ nat.
1534 match eqex (bl b) x0 with
1535 [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1536 | false ⇒ mk_byte (bh b) (xpred (bl b))
1539 (* Way too slow and subsumed by previous theorem
1542 match eqbyte b (mk_byte x0 x0) with
1543 [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1544 | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1553 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1555 coercion cic:/matita/assembly/addr_of_byte.con.
1557 inductive opcode: Type ≝
1558 ADDd: opcode (* 3 clock, 171 *)
1559 | BEQ: opcode (* 3, 55 *)
1560 | BRA: opcode (* 3, 48 *)
1561 | DECd: opcode (* 5, 58 *)
1562 | LDAi: opcode (* 2, 166 *)
1563 | LDAd: opcode (* 3, 182 *)
1564 | STAd: opcode. (* 3, 183 *)
1566 let rec cycles_of_opcode op : nat ≝
1577 definition opcodemap ≝
1578 [ couple ? ? ADDd (mk_byte xA xB);
1579 couple ? ? BEQ (mk_byte x3 x7);
1580 couple ? ? BRA (mk_byte x3 x0);
1581 couple ? ? DECd (mk_byte x3 xA);
1582 couple ? ? LDAi (mk_byte xA x6);
1583 couple ? ? LDAd (mk_byte xB x6);
1584 couple ? ? STAd (mk_byte xB x7) ].
1586 definition opcode_of_byte ≝
1594 match eqbyte n b with
1601 definition magic_of_opcode ≝
1612 definition opcodeeqb ≝
1613 λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1615 definition byte_of_opcode : opcode → byte ≝
1619 [ nil ⇒ mk_byte x0 x0
1623 match opcodeeqb op op' with
1630 record status : Type ≝ {
1641 λf: addr → byte.λa.λv.λx.
1646 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1649 λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1650 let opc ≝ opcode_of_byte (mem pc) in
1651 let op1 ≝ mem (S pc) in
1652 let clk' ≝ cycles_of_opcode opc in
1653 match eqb (S clk) clk' with
1657 let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1658 let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1659 let c' ≝ match res with [ couple _ c' ⇒ c'] in
1660 mk_status acc' (2 + pc) spc
1661 (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
1666 [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *)
1676 acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1683 let x ≝ bpred (mem op1) in (* signed!!! *)
1684 let mem' ≝ update mem op1 x in
1685 mk_status acc (2 + pc) spc
1686 (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
1688 mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
1691 mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
1693 mk_status acc (2 + pc) spc zf cf
1694 (update mem op1 acc) 0
1698 acc pc spc zf cf mem (S clk)
1701 let rec execute s n on n ≝
1704 | S n' ⇒ execute (tick s) n'
1708 ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
1710 generalize in match s; clear s;
1718 notation "hvbox(# break a)"
1719 non associative with precedence 80
1720 for @{ 'byte_of_opcode $a }.
1721 interpretation "byte_of_opcode" 'byte_of_opcode a =
1722 (cic:/matita/assembly/byte_of_opcode.con a).
1724 definition mult_source : list byte ≝
1725 [#LDAi; mk_byte x0 x0; (* A := 0 *)
1726 #STAd; mk_byte x2 x0; (* Z := A *)
1727 #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1728 #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *)
1729 #LDAd; mk_byte x2 x0; (* A := Z *)
1730 #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1731 #ADDd; mk_byte x1 xE; (* A += X *)
1732 #STAd; mk_byte x2 x0; (* Z := A *)
1733 #BRA; mk_byte xF x2; (* goto l1 *)
1734 #LDAd; mk_byte x2 x0].(* (l2) *)
1736 definition mult_memory ≝
1739 [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1747 definition mult_status ≝
1749 mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
1752 ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1760 definition plusbytenc ≝
1762 match plusbyte x y false with
1763 [couple res _ ⇒ res].
1765 definition plusbytec ≝
1767 match plusbyte x y false with
1770 lemma plusbytenc_O_x:
1771 ∀x. plusbytenc (mk_byte x0 x0) x = x.
1774 rewrite > plusbyte_O_x;
1780 let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1781 pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1789 let x ≝ mk_byte x0 x0 in
1790 let y ≝ mk_byte x0 x2 in
1791 let i ≝ 14 + 23 * nat_of_byte y in
1792 let s ≝ execute (mult_status x y) i in
1793 pc s = 20 ∧ mem s 32 = plusbytenc x x.
1801 let y ≝ mk_byte x0 x1 in
1802 let i ≝ 14 + 23 * nat_of_byte y in
1803 let s ≝ execute (mult_status x y) i in
1804 pc s = 20 ∧ mem s 32 = x.
1808 | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1809 rewrite > plusbytenc_O_x;
1816 let y ≝ mk_byte x0 x2 in
1817 let i ≝ 14 + 23 * nat_of_byte y in
1818 let s ≝ execute (mult_status x y) i in
1819 pc s = 20 ∧ mem s 32 = plusbytenc x x.
1823 | change in ⊢ (? ? % ?) with
1824 (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1825 rewrite > plusbytenc_O_x;
1832 (P (mk_byte x0 x0)) →
1833 (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
1835 (* Tedious proof, easy to automate but not trivial
1846 [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
1852 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
1858 axiom daemon: False.
1860 (*axiom loop_invariant:
1861 ∀x,y:byte.∀j:nat. j ≤ y →
1862 let s ≝ execute (mult_status x y) (5 + 23*j) in
1865 mem s 31 = byte_of_nat (y - j) ∧
1866 mem s 32 = byte_of_nat (x * j).
1869 apply (byte_elim ? ? ? y);
1873 [ unfold s; clear s;
1876 | (* easy *) elim daemon
1880 cut (j < S i ∨ j = S i);
1882 [ rewrite > nat_of_byte_byte_of_nat in H1;
1883 [2: apply (lt_trans ? 255);
1888 | generalize in match (H1 j); clear H1;
1892 [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro;
1897 rewrite > (injective_S ? ? H1);
1900 (* facile *) elim daemon
1919 (∀a. mem s a = mem s' a) →
1923 lemma eq_eqex_S_x0_false:
1924 ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
1926 cases n 0; [ intro; simplify; reflexivity | clear n];
1927 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1928 cases n 0; [ intro; simplify; reflexivity | clear n];
1929 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1930 cases n 0; [ intro; simplify; reflexivity | clear n];
1931 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1932 cases n 0; [ intro; simplify; reflexivity | clear n];
1933 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1934 cases n 0; [ intro; simplify; reflexivity | clear n];
1935 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1936 cases n 0; [ intro; simplify; reflexivity | clear n];
1937 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1938 cases n 0; [ intro; simplify; reflexivity | clear n];
1939 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1940 cases n 0; [ intro; simplify; reflexivity | clear n];
1944 [ elim (not_le_Sn_O ? Hcut)
1945 | do 15 (apply le_S_S_to_le);
1950 lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
1953 apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
1958 clear Hcut; clear H2; clear H; (*clear m;*)
1960 unfold in ⊢ (? ? % ?);
1962 [ elim Hcut; clear Hcut;
1964 rewrite > H; clear m;
1965 change in ⊢ (? ? % ?) with
1966 (match leb (S a1) a with
1968 | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
1970 [ apply (leb_elim (S a1) a);
1980 | elim H1; autobatch
1986 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
1987 ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
1990 cut (b < 15 ∨ b ≥ 15);
1993 change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
1994 rewrite > eq_eqex_S_x0_false;
1995 [ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
2001 change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
2002 letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
2010 rewrite > eq_eqex_S_x0_false;
2015 clear H2; clear a; clear H1; clear Hcut;
2016 elim daemon (* trivial arithmetic property over <= and div *)
2024 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
2031 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
2034 letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
2035 letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
2036 unfold lt in H K ⊢ %;
2037 letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
2038 letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
2040 cut (16*bh b ≤ 16*15);
2041 [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
2042 simplify in Hf:(? ? %);
2048 lemma exadecimal_of_nat_mod:
2049 ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
2053 cases n; [ reflexivity | ];
2054 cases n1; [ reflexivity | ];
2055 cases n2; [ reflexivity | ];
2056 cases n3; [ reflexivity | ];
2057 cases n4; [ reflexivity | ];
2058 cases n5; [ reflexivity | ];
2059 cases n6; [ reflexivity | ];
2060 cases n7; [ reflexivity | ];
2061 cases n8; [ reflexivity | ];
2062 cases n9; [ reflexivity | ];
2063 cases n10; [ reflexivity | ];
2064 cases n11; [ reflexivity | ];
2065 cases n12; [ reflexivity | ];
2066 cases n13; [ reflexivity | ];
2067 cases n14; [ reflexivity | ];
2068 cases n15; [ reflexivity | ];
2069 change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
2070 cut ((16 + n16) \mod 16 = n16 \mod 16);
2072 simplify in ⊢ (? ? % ?);
2075 change with (mod_aux (16+n16) (16+n16) 15 = n16);
2078 (match leb (16+n16) 15 with
2080 | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
2082 cut (leb (16+n16) 15 = false);
2084 change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
2085 cut (16+n16-16 = n16);
2086 [ rewrite > Hcut1; clear Hcut1;
2095 lemma eq_bpred_S_a_a:
2096 ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
2100 cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
2109 lemma plusbyteenc_S:
2110 ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
2116 lemma loop_invariant':
2117 ∀x,y:byte.∀j:nat. j ≤ y →
2118 execute (mult_status x y) (5 + 23*j)
2120 mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j))) false
2121 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
2122 (byte_of_nat (x * j)))
2126 [ do 2 (rewrite < times_n_O);
2128 [1,2,3,4,5,7: normalize; reflexivity
2132 | cut (5 + 23 * S n = 5 + 23 * n + 23);
2133 [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
2134 letin H' ≝ (H ?); clearbody H'; clear H;
2136 | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
2140 apply (transitive_eq ? ? ? ? K);
2144 cut (∃z.y-n=S z ∧ z < 255);
2145 [ elim Hcut; clear Hcut;
2151 (mk_status (byte_of_nat (x*n)) 4 O true false
2152 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2153 (byte_of_nat (x*n))) O)
2155 normalize in K:(? ? (? ? %) ?);
2156 apply transitive_eq; [2: apply K | skip | ]; clear K;
2157 change in ⊢ (? ? (? % ?) ?) with
2162 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
2165 (update (update (mult_memory x y) 30 x)
2166 31 (byte_of_nat (S a)))
2167 32 (byte_of_nat (x*n)))
2172 (mk_status (byte_of_nat (S a)) 6 O
2173 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) false
2174 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2175 (byte_of_nat (x*n))) O)
2177 normalize in K:(? ? (? ? %) ?);
2178 apply transitive_eq; [2: apply K | skip | ]; clear K;
2179 whd in ⊢ (? ? (? % ?) ?);
2180 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
2181 rewrite > K; clear K;
2182 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2186 (mk_status (byte_of_nat (S a)) 8 O
2187 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) false
2188 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2189 (byte_of_nat (x*n))) O)
2191 normalize in K:(? ? (? ? %) ?);
2192 apply transitive_eq; [2: apply K | skip | ]; clear K;
2193 whd in ⊢ (? ? (? % ?) ?);
2194 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
2195 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2196 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
2197 (* instruction DECd *)
2200 (mk_status (byte_of_nat (x*n)) 10 O
2201 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) false
2202 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
2203 (byte_of_nat (x*n))) O)
2205 normalize in K:(? ? (? ? %) ?);
2206 apply transitive_eq; [2: apply K | skip | ]; clear K;
2207 whd in ⊢ (? ? (? % ?) ?);
2208 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
2209 rewrite > (eq_bpred_S_a_a ? H3);
2210 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2211 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
2213 [2: elim daemon | ];
2214 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
2215 (* instruction ADDd *)
2218 (mk_status (byte_of_nat (x*n)) 12
2219 O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n))) false
2221 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
2222 32 (byte_of_nat (x*n))) 31
2223 (byte_of_nat (y-S n))) O)
2225 normalize in K:(? ? (? ? %) ?);
2226 apply transitive_eq; [2: apply K | skip | ]; clear K;
2227 whd in ⊢ (? ? (? % ?) ?);
2228 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
2229 (plusbytenc (byte_of_nat (x*n)) x);
2230 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
2231 (plusbytenc (byte_of_nat (x*n)) x);
2232 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2233 normalize in \vdash (? ?
2235 (? ? ? ? ? match ? ? % ? in cartesian_product return ? with [couple\rArr ?] ? ?)
2237 rewrite > plusbyteenc_S;
2238 (* instruction STAd *)
2241 (mk_status (byte_of_nat (x*S n)) 14 O
2242 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
2243 match plusbyte (byte_of_nat (x*n)) x false
2244 in cartesian_product
2245 return \lambda c:(cartesian_product byte bool).bool
2247 [couple (_:byte) (c':bool)\rArr c']
2249 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
2250 32 (byte_of_nat (x*n))) 31
2251 (byte_of_nat (y-S n))) O)
2253 normalize in K:(? ? (? ? %) ?);
2254 apply transitive_eq; [2: apply K | skip | ]; clear K;
2255 whd in ⊢ (? ? (? % ?) ?);
2256 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
2257 (* instruction BRA *)
2259 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
2261 [1,2,3,4,7: normalize; reflexivity
2269 [ rewrite < (minus_S_S y n);
2271 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
2272 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
2278 | autobatch paramodulation
2285 let i ≝ 14 + 23 * nat_of_byte y in
2286 let s ≝ execute (mult_status x y) i in
2287 pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
2289 generalize in match (loop_invariant' x y y (le_n y)); intro;
2290 generalize in match (breakpoint (mult_status x y) (5 + 23*y) 9); intro;
2291 cut (5 + 23*y +9 = 14 + 23* y);
2292 [2: autobatch paramodulation
2293 | rewrite > Hcut in H1;
2294 change in H1:(? ? % ?) with s;
2295 letin s0 ≝ (execute (mult_status x y) (S (S (S (S (S O))))+S 22*y));
2296 generalize in match H; intro K; clear H;
2299 mk_status (byte_of_nat (x*y)) 4 0 true false
2302 (update (mult_memory x y) 30 x)
2303 31 (byte_of_nat (y-y)))
2304 32 (byte_of_nat (x*y))) O);
2306 generalize in match H1; intro K1; clear H1;
2307 change in K1 with (s = execute s0 9);
2309 clear K; clear s0; clearbody s; clear i;
2310 rewrite < minus_n_n in K1;