1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "common/ascii_lemmas1.ma".
24 include "num/bool_lemmas.ma".
26 (* ************************** *)
27 (* DEFINIZIONE ASCII MINIMALE *)
28 (* ************************** *)
30 nlemma decidable_ascii1 : ∀x:ascii.decidable (ch_0 = x).
31 #x; nnormalize; nelim x;
32 ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
33 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
37 nlemma decidable_ascii2 : ∀x:ascii.decidable (ch_1 = x).
38 #x; nnormalize; nelim x;
39 ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
40 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
44 nlemma decidable_ascii3 : ∀x:ascii.decidable (ch_2 = x).
45 #x; nnormalize; nelim x;
46 ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
47 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
51 nlemma decidable_ascii4 : ∀x:ascii.decidable (ch_3 = x).
52 #x; nnormalize; nelim x;
53 ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
54 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
58 nlemma decidable_ascii5 : ∀x:ascii.decidable (ch_4 = x).
59 #x; nnormalize; nelim x;
60 ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
61 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
65 nlemma decidable_ascii6 : ∀x:ascii.decidable (ch_5 = x).
66 #x; nnormalize; nelim x;
67 ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
68 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
72 nlemma decidable_ascii7 : ∀x:ascii.decidable (ch_6 = x).
73 #x; nnormalize; nelim x;
74 ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
75 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
79 nlemma decidable_ascii8 : ∀x:ascii.decidable (ch_7 = x).
80 #x; nnormalize; nelim x;
81 ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
82 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
86 nlemma decidable_ascii9 : ∀x:ascii.decidable (ch_8 = x).
87 #x; nnormalize; nelim x;
88 ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
89 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
93 nlemma decidable_ascii10 : ∀x:ascii.decidable (ch_9 = x).
94 #x; nnormalize; nelim x;
95 ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
96 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
100 nlemma decidable_ascii11 : ∀x:ascii.decidable (ch__ = x).
101 #x; nnormalize; nelim x;
102 ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
103 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
107 nlemma decidable_ascii12 : ∀x:ascii.decidable (ch_A = x).
108 #x; nnormalize; nelim x;
109 ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
110 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
114 nlemma decidable_ascii13 : ∀x:ascii.decidable (ch_B = x).
115 #x; nnormalize; nelim x;
116 ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
117 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
121 nlemma decidable_ascii14 : ∀x:ascii.decidable (ch_C = x).
122 #x; nnormalize; nelim x;
123 ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
124 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
128 nlemma decidable_ascii15 : ∀x:ascii.decidable (ch_D = x).
129 #x; nnormalize; nelim x;
130 ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
131 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
135 nlemma decidable_ascii16 : ∀x:ascii.decidable (ch_E = x).
136 #x; nnormalize; nelim x;
137 ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
138 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
142 nlemma decidable_ascii17 : ∀x:ascii.decidable (ch_F = x).
143 #x; nnormalize; nelim x;
144 ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
145 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
149 nlemma decidable_ascii18 : ∀x:ascii.decidable (ch_G = x).
150 #x; nnormalize; nelim x;
151 ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
152 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
156 nlemma decidable_ascii19 : ∀x:ascii.decidable (ch_H = x).
157 #x; nnormalize; nelim x;
158 ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
159 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
163 nlemma decidable_ascii20 : ∀x:ascii.decidable (ch_I = x).
164 #x; nnormalize; nelim x;
165 ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
166 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
170 nlemma decidable_ascii21 : ∀x:ascii.decidable (ch_J = x).
171 #x; nnormalize; nelim x;
172 ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
173 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
177 nlemma decidable_ascii22 : ∀x:ascii.decidable (ch_K = x).
178 #x; nnormalize; nelim x;
179 ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
180 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
184 nlemma decidable_ascii23 : ∀x:ascii.decidable (ch_L = x).
185 #x; nnormalize; nelim x;
186 ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
187 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
191 nlemma decidable_ascii24 : ∀x:ascii.decidable (ch_M = x).
192 #x; nnormalize; nelim x;
193 ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
194 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
198 nlemma decidable_ascii25 : ∀x:ascii.decidable (ch_N = x).
199 #x; nnormalize; nelim x;
200 ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
201 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
205 nlemma decidable_ascii26 : ∀x:ascii.decidable (ch_O = x).
206 #x; nnormalize; nelim x;
207 ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
208 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
212 nlemma decidable_ascii27 : ∀x:ascii.decidable (ch_P = x).
213 #x; nnormalize; nelim x;
214 ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
215 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
219 nlemma decidable_ascii28 : ∀x:ascii.decidable (ch_Q = x).
220 #x; nnormalize; nelim x;
221 ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
222 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
226 nlemma decidable_ascii29 : ∀x:ascii.decidable (ch_R = x).
227 #x; nnormalize; nelim x;
228 ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
229 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
233 nlemma decidable_ascii30 : ∀x:ascii.decidable (ch_S = x).
234 #x; nnormalize; nelim x;
235 ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
236 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
240 nlemma decidable_ascii31 : ∀x:ascii.decidable (ch_T = x).
241 #x; nnormalize; nelim x;
242 ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
243 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
247 nlemma decidable_ascii32 : ∀x:ascii.decidable (ch_U = x).
248 #x; nnormalize; nelim x;
249 ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
250 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
254 nlemma decidable_ascii33 : ∀x:ascii.decidable (ch_V = x).
255 #x; nnormalize; nelim x;
256 ##[ ##33: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
257 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
261 nlemma decidable_ascii34 : ∀x:ascii.decidable (ch_W = x).
262 #x; nnormalize; nelim x;
263 ##[ ##34: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
264 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
268 nlemma decidable_ascii35 : ∀x:ascii.decidable (ch_X = x).
269 #x; nnormalize; nelim x;
270 ##[ ##35: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
271 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
275 nlemma decidable_ascii36 : ∀x:ascii.decidable (ch_Y = x).
276 #x; nnormalize; nelim x;
277 ##[ ##36: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
278 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
282 nlemma decidable_ascii37 : ∀x:ascii.decidable (ch_Z = x).
283 #x; nnormalize; nelim x;
284 ##[ ##37: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
285 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
289 nlemma decidable_ascii38 : ∀x:ascii.decidable (ch_a = x).
290 #x; nnormalize; nelim x;
291 ##[ ##38: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
292 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
296 nlemma decidable_ascii39 : ∀x:ascii.decidable (ch_b = x).
297 #x; nnormalize; nelim x;
298 ##[ ##39: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
299 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
303 nlemma decidable_ascii40 : ∀x:ascii.decidable (ch_c = x).
304 #x; nnormalize; nelim x;
305 ##[ ##40: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
306 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
310 nlemma decidable_ascii41 : ∀x:ascii.decidable (ch_d = x).
311 #x; nnormalize; nelim x;
312 ##[ ##41: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
313 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
317 nlemma decidable_ascii42 : ∀x:ascii.decidable (ch_e = x).
318 #x; nnormalize; nelim x;
319 ##[ ##42: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
320 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
324 nlemma decidable_ascii43 : ∀x:ascii.decidable (ch_f = x).
325 #x; nnormalize; nelim x;
326 ##[ ##43: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
327 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
331 nlemma decidable_ascii44 : ∀x:ascii.decidable (ch_g = x).
332 #x; nnormalize; nelim x;
333 ##[ ##44: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
334 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
338 nlemma decidable_ascii45 : ∀x:ascii.decidable (ch_h = x).
339 #x; nnormalize; nelim x;
340 ##[ ##45: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
341 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
345 nlemma decidable_ascii46 : ∀x:ascii.decidable (ch_i = x).
346 #x; nnormalize; nelim x;
347 ##[ ##46: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
348 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
352 nlemma decidable_ascii47 : ∀x:ascii.decidable (ch_j = x).
353 #x; nnormalize; nelim x;
354 ##[ ##47: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
355 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
359 nlemma decidable_ascii48 : ∀x:ascii.decidable (ch_k = x).
360 #x; nnormalize; nelim x;
361 ##[ ##48: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
362 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
366 nlemma decidable_ascii49 : ∀x:ascii.decidable (ch_l = x).
367 #x; nnormalize; nelim x;
368 ##[ ##49: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
369 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
373 nlemma decidable_ascii50 : ∀x:ascii.decidable (ch_m = x).
374 #x; nnormalize; nelim x;
375 ##[ ##50: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
376 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
380 nlemma decidable_ascii51 : ∀x:ascii.decidable (ch_n = x).
381 #x; nnormalize; nelim x;
382 ##[ ##51: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
383 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
387 nlemma decidable_ascii52 : ∀x:ascii.decidable (ch_o = x).
388 #x; nnormalize; nelim x;
389 ##[ ##52: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
390 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
394 nlemma decidable_ascii53 : ∀x:ascii.decidable (ch_p = x).
395 #x; nnormalize; nelim x;
396 ##[ ##53: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
397 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
401 nlemma decidable_ascii54 : ∀x:ascii.decidable (ch_q = x).
402 #x; nnormalize; nelim x;
403 ##[ ##54: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
404 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
408 nlemma decidable_ascii55 : ∀x:ascii.decidable (ch_r = x).
409 #x; nnormalize; nelim x;
410 ##[ ##55: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
411 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
415 nlemma decidable_ascii56 : ∀x:ascii.decidable (ch_s = x).
416 #x; nnormalize; nelim x;
417 ##[ ##56: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
418 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
422 nlemma decidable_ascii57 : ∀x:ascii.decidable (ch_t = x).
423 #x; nnormalize; nelim x;
424 ##[ ##57: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
425 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
429 nlemma decidable_ascii58 : ∀x:ascii.decidable (ch_u = x).
430 #x; nnormalize; nelim x;
431 ##[ ##58: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
432 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
436 nlemma decidable_ascii59 : ∀x:ascii.decidable (ch_v = x).
437 #x; nnormalize; nelim x;
438 ##[ ##59: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
439 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
443 nlemma decidable_ascii60 : ∀x:ascii.decidable (ch_w = x).
444 #x; nnormalize; nelim x;
445 ##[ ##60: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
446 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
450 nlemma decidable_ascii61 : ∀x:ascii.decidable (ch_x = x).
451 #x; nnormalize; nelim x;
452 ##[ ##61: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
453 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
457 nlemma decidable_ascii62 : ∀x:ascii.decidable (ch_y = x).
458 #x; nnormalize; nelim x;
459 ##[ ##62: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
460 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
464 nlemma decidable_ascii63 : ∀x:ascii.decidable (ch_z = x).
465 #x; nnormalize; nelim x;
466 ##[ ##63: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
467 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
471 nlemma decidable_ascii : ∀x,y:ascii.decidable (x = y).
473 ##[ ##1: napply decidable_ascii1 ##| ##2: napply decidable_ascii2
474 ##| ##3: napply decidable_ascii3 ##| ##4: napply decidable_ascii4
475 ##| ##5: napply decidable_ascii5 ##| ##6: napply decidable_ascii6
476 ##| ##7: napply decidable_ascii7 ##| ##8: napply decidable_ascii8
477 ##| ##9: napply decidable_ascii9 ##| ##10: napply decidable_ascii10
478 ##| ##11: napply decidable_ascii11 ##| ##12: napply decidable_ascii12
479 ##| ##13: napply decidable_ascii13 ##| ##14: napply decidable_ascii14
480 ##| ##15: napply decidable_ascii15 ##| ##16: napply decidable_ascii16
481 ##| ##17: napply decidable_ascii17 ##| ##18: napply decidable_ascii18
482 ##| ##19: napply decidable_ascii19 ##| ##20: napply decidable_ascii20
483 ##| ##21: napply decidable_ascii21 ##| ##22: napply decidable_ascii22
484 ##| ##23: napply decidable_ascii23 ##| ##24: napply decidable_ascii24
485 ##| ##25: napply decidable_ascii25 ##| ##26: napply decidable_ascii26
486 ##| ##27: napply decidable_ascii27 ##| ##28: napply decidable_ascii28
487 ##| ##29: napply decidable_ascii29 ##| ##30: napply decidable_ascii30
488 ##| ##31: napply decidable_ascii31 ##| ##32: napply decidable_ascii32
489 ##| ##33: napply decidable_ascii33 ##| ##34: napply decidable_ascii34
490 ##| ##35: napply decidable_ascii35 ##| ##36: napply decidable_ascii36
491 ##| ##37: napply decidable_ascii37 ##| ##38: napply decidable_ascii38
492 ##| ##39: napply decidable_ascii39 ##| ##40: napply decidable_ascii40
493 ##| ##41: napply decidable_ascii41 ##| ##42: napply decidable_ascii42
494 ##| ##43: napply decidable_ascii43 ##| ##44: napply decidable_ascii44
495 ##| ##45: napply decidable_ascii45 ##| ##46: napply decidable_ascii46
496 ##| ##47: napply decidable_ascii47 ##| ##48: napply decidable_ascii48
497 ##| ##49: napply decidable_ascii49 ##| ##50: napply decidable_ascii50
498 ##| ##51: napply decidable_ascii51 ##| ##52: napply decidable_ascii52
499 ##| ##53: napply decidable_ascii53 ##| ##54: napply decidable_ascii54
500 ##| ##55: napply decidable_ascii55 ##| ##56: napply decidable_ascii56
501 ##| ##57: napply decidable_ascii57 ##| ##58: napply decidable_ascii58
502 ##| ##59: napply decidable_ascii59 ##| ##60: napply decidable_ascii60
503 ##| ##61: napply decidable_ascii61 ##| ##62: napply decidable_ascii62
504 ##| ##63: napply decidable_ascii63 ##]