URL: https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf
%PDF-1.4
%����
1 0 obj
<< /S /GoTo /D (chapter.1) >>
endobj
4 0 obj
(Pr\351face)
endobj
5 0 obj
<< /S /GoTo /D (chapter.2) >>
endobj
8 0 obj
(Un bref tour d'horizon)
endobj
9 0 obj
<< /S /GoTo /D (section.2.1) >>
endobj
12 0 obj
(Expressions, types et fonctions)
endobj
13 0 obj
<< /S /GoTo /D (section.2.2) >>
endobj
16 0 obj
(Propositions et preuves)
endobj
17 0 obj
<< /S /GoTo /D (section.2.3) >>
endobj
20 0 obj
(Propositions et types)
endobj
21 0 obj
<< /S /GoTo /D (section.2.4) >>
endobj
24 0 obj
(Sp\351cifications complexes et programmes certifi\351s)
endobj
25 0 obj
<< /S /GoTo /D (section.2.5) >>
endobj
28 0 obj
(L'exemple du tri)
endobj
29 0 obj
<< /S /GoTo /D (subsection.2.5.1) >>
endobj
32 0 obj
(D\351finitions inductives)
endobj
33 0 obj
<< /S /GoTo /D (subsection.2.5.2) >>
endobj
36 0 obj
(La relation \253 avoir les m\352mes \351l\351ments \273)
endobj
37 0 obj
<< /S /GoTo /D (subsection.2.5.3) >>
endobj
40 0 obj
(La sp\351cification du tri)
endobj
41 0 obj
<< /S /GoTo /D (subsection.2.5.4) >>
endobj
44 0 obj
(Une fonction auxiliaire)
endobj
45 0 obj
<< /S /GoTo /D (subsection.2.5.5) >>
endobj
48 0 obj
(Le tri proprement dit)
endobj
49 0 obj
<< /S /GoTo /D (section.2.6) >>
endobj
52 0 obj
(Apprendre Coq)
endobj
53 0 obj
<< /S /GoTo /D (section.2.7) >>
endobj
56 0 obj
(Contenu de l'ouvrage)
endobj
57 0 obj
<< /S /GoTo /D (section.2.8) >>
endobj
60 0 obj
(Conventions lexicales)
endobj
61 0 obj
<< /S /GoTo /D (chapter.3) >>
endobj
64 0 obj
(Types et expressions)
endobj
65 0 obj
<< /S /GoTo /D (section.3.1) >>
endobj
68 0 obj
(Premiers pas)
endobj
69 0 obj
<< /S /GoTo /D (subsection.3.1.1) >>
endobj
72 0 obj
(Termes, expressions, types, etc.)
endobj
73 0 obj
<< /S /GoTo /D (subsection.3.1.2) >>
endobj
76 0 obj
(Notion de port\351e)
endobj
77 0 obj
<< /S /GoTo /D (subsection.3.1.3) >>
endobj
80 0 obj
(Contr\364le de type)
endobj
81 0 obj
<< /S /GoTo /D (section.3.2) >>
endobj
84 0 obj
(Les r\350gles du jeu)
endobj
85 0 obj
<< /S /GoTo /D (subsection.3.2.1) >>
endobj
88 0 obj
(Types simples)
endobj
89 0 obj
<< /S /GoTo /D (subsection.3.2.2) >>
endobj
92 0 obj
(Identificateurs, environnements, contextes, etc. )
endobj
93 0 obj
<< /S /GoTo /D (subsection.3.2.3) >>
endobj
96 0 obj
(Les expressions et leur type)
endobj
97 0 obj
<< /S /GoTo /D (subsection.3.2.4) >>
endobj
100 0 obj
(Occurrences libres et li\351es ; -conversion)
endobj
101 0 obj
<< /S /GoTo /D (section.3.3) >>
endobj
104 0 obj
(D\351clarations et d\351finitions)
endobj
105 0 obj
<< /S /GoTo /D (subsection.3.3.1) >>
endobj
108 0 obj
(D\351clarations et d\351finitions globales)
endobj
109 0 obj
<< /S /GoTo /D (subsection.3.3.2) >>
endobj
112 0 obj
(Sections et variables locales)
endobj
113 0 obj
<< /S /GoTo /D (section.3.4) >>
endobj
116 0 obj
(Un peu de calcul)
endobj
117 0 obj
<< /S /GoTo /D (subsection.3.4.1) >>
endobj
120 0 obj
(Substitution)
endobj
121 0 obj
<< /S /GoTo /D (subsection.3.4.2) >>
endobj
124 0 obj
(R\350gles de conversion)
endobj
125 0 obj
<< /S /GoTo /D (subsection.3.4.3) >>
endobj
128 0 obj
(Notations)
endobj
129 0 obj
<< /S /GoTo /D (subsection.3.4.4) >>
endobj
132 0 obj
(Propri\351t\351s abstraites de la r\351duction)
endobj
133 0 obj
<< /S /GoTo /D (section.3.5) >>
endobj
136 0 obj
(Types, sortes et univers)
endobj
137 0 obj
<< /S /GoTo /D (subsection.3.5.1) >>
endobj
140 0 obj
(La sorte Set)
endobj
141 0 obj
<< /S /GoTo /D (subsection.3.5.2) >>
endobj
144 0 obj
(Les univers)
endobj
145 0 obj
<< /S /GoTo /D (subsection.3.5.3) >>
endobj
148 0 obj
(D\351finitions et d\351clarations de sp\351cifications)
endobj
149 0 obj
<< /S /GoTo /D (section.3.6) >>
endobj
152 0 obj
(De la sp\351cification \340 la r\351alisation)
endobj
153 0 obj
<< /S /GoTo /D (chapter.4) >>
endobj
156 0 obj
(Propositions et preuves)
endobj
157 0 obj
<< /S /GoTo /D (section.4.1) >>
endobj
160 0 obj
(La logique minimale propositionnelle)
endobj
161 0 obj
<< /S /GoTo /D (subsection.4.1.1) >>
endobj
164 0 obj
(Le monde des propositions et des preuves)
endobj
165 0 obj
<< /S /GoTo /D (subsection.4.1.2) >>
endobj
168 0 obj
(Buts et tactiques)
endobj
169 0 obj
<< /S /GoTo /D (subsection.4.1.3) >>
endobj
172 0 obj
(Un premier exemple)
endobj
173 0 obj
<< /S /GoTo /D (section.4.2) >>
endobj
176 0 obj
(R\350gles de typage et tactiques)
endobj
177 0 obj
<< /S /GoTo /D (subsection.4.2.1) >>
endobj
180 0 obj
(R\350gles de construction des propositions)
endobj
181 0 obj
<< /S /GoTo /D (subsection.4.2.2) >>
endobj
184 0 obj
(R\350gles d'inf\351rence et tactiques)
endobj
185 0 obj
<< /S /GoTo /D (section.4.3) >>
endobj
188 0 obj
(Structure d'une preuve interactive)
endobj
189 0 obj
<< /S /GoTo /D (subsection.4.3.1) >>
endobj
192 0 obj
(Activation du syst\350me de gestion de buts)
endobj
193 0 obj
<< /S /GoTo /D (subsection.4.3.2) >>
endobj
196 0 obj
(\311tape courante d'une preuve interactive)
endobj
197 0 obj
<< /S /GoTo /D (subsection.4.3.3) >>
endobj
200 0 obj
(H\351sitations)
endobj
201 0 obj
<< /S /GoTo /D (subsection.4.3.4) >>
endobj
204 0 obj
(Fin normale d'un d\351veloppement)
endobj
205 0 obj
<< /S /GoTo /D (section.4.4) >>
endobj
208 0 obj
(La non pertinence des preuves)
endobj
209 0 obj
<< /S /GoTo /D (subsection.4.4.1) >>
endobj
212 0 obj
(Theorem versus Definition)
endobj
213 0 obj
<< /S /GoTo /D (subsection.4.4.2) >>
endobj
216 0 obj
(Des tactiques pour construire des programmes?)
endobj
217 0 obj
<< /S /GoTo /D (section.4.5) >>
endobj
220 0 obj
(Utilisation de sections)
endobj
221 0 obj
<< /S /GoTo /D (section.4.6) >>
endobj
224 0 obj
(Composition de tactiques)
endobj
225 0 obj
<< /S /GoTo /D (section.4.7) >>
endobj
228 0 obj
(Quelques probl\350mes de maintenance)
endobj
229 0 obj
<< /S /GoTo /D (section.4.8) >>
endobj
232 0 obj
(Probl\350mes de compl\351tude)
endobj
233 0 obj
<< /S /GoTo /D (subsection.4.8.1) >>
endobj
236 0 obj
(Un jeu de tactiques suffisant)
endobj
237 0 obj
<< /S /GoTo /D (subsection.4.8.2) >>
endobj
240 0 obj
(Des propositions impossibles \340 montrer)
endobj
241 0 obj
<< /S /GoTo /D (section.4.9) >>
endobj
244 0 obj
(Autres tactiques)
endobj
245 0 obj
<< /S /GoTo /D (subsection.4.9.1) >>
endobj
248 0 obj
(Les tactiques cut et assert)
endobj
249 0 obj
<< /S /GoTo /D (subsection.4.9.2) >>
endobj
252 0 obj
(Tactiques et automatismes)
endobj
253 0 obj
<< /S /GoTo /D (section.4.10) >>
endobj
256 0 obj
(Un nouveau type d'abstractions)
endobj
257 0 obj
<< /S /GoTo /D (chapter.5) >>
endobj
260 0 obj
(Le produit d\351pendant)
endobj
261 0 obj
<< /S /GoTo /D (section.5.1) >>
endobj
264 0 obj
(\311loge de la d\351pendance)
endobj
265 0 obj
<< /S /GoTo /D (subsection.5.1.1) >>
endobj
268 0 obj
(De nouveaux types fl\350ches)
endobj
269 0 obj
<< /S /GoTo /D (subsection.5.1.2) >>
endobj
272 0 obj
(Les liaisons n\351cessaires)
endobj
273 0 obj
<< /S /GoTo /D (subsection.5.1.3) >>
endobj
276 0 obj
(Une nouvelle construction)
endobj
277 0 obj
<< /S /GoTo /D (section.5.2) >>
endobj
280 0 obj
(R\350gles de typage associ\351es au produit d\351pendant)
endobj
281 0 obj
<< /S /GoTo /D (subsection.5.2.1) >>
endobj
284 0 obj
(R\350gle d'application)
endobj
285 0 obj
<< /S /GoTo /D (subsection.5.2.2) >>
endobj
288 0 obj
(R\350gle d'abstraction)
endobj
289 0 obj
<< /S /GoTo /D (subsection.5.2.3) >>
endobj
292 0 obj
(Inf\351rence de type)
endobj
293 0 obj
<< /S /GoTo /D (subsection.5.2.4) >>
endobj
296 0 obj
(R\350gle de conversion)
endobj
297 0 obj
<< /S /GoTo /D (subsection.5.2.5) >>
endobj
300 0 obj
(Produit d\351pendant et ordre de convertibilit\351)
endobj
301 0 obj
<< /S /GoTo /D (section.5.3) >>
endobj
304 0 obj
(* Puissance d'expression du produit d\351pendant)
endobj
305 0 obj
<< /S /GoTo /D (subsection.5.3.1) >>
endobj
308 0 obj
(R\350gle de formation du produit d\351pendant)
endobj
309 0 obj
<< /S /GoTo /D (subsection.5.3.2) >>
endobj
312 0 obj
(Types d\351pendants)
endobj
313 0 obj
<< /S /GoTo /D (subsection.5.3.3) >>
endobj
316 0 obj
(Le polymorphisme)
endobj
317 0 obj
<< /S /GoTo /D (subsection.5.3.4) >>
endobj
320 0 obj
(L'\351galit\351 en Coq)
endobj
321 0 obj
<< /S /GoTo /D (subsection.5.3.5) >>
endobj
324 0 obj
(Types d'ordre sup\351rieur)
endobj
325 0 obj
<< /S /GoTo /D (chapter.6) >>
endobj
328 0 obj
(Logique de tous les jours)
endobj
329 0 obj
<< /S /GoTo /D (section.6.1) >>
endobj
332 0 obj
(Pratique du produit d\351pendant)
endobj
333 0 obj
<< /S /GoTo /D (subsection.6.1.1) >>
endobj
336 0 obj
(exact et assumption)
endobj
337 0 obj
<< /S /GoTo /D (subsection.6.1.2) >>
endobj
340 0 obj
(La tactique intro)
endobj
341 0 obj
<< /S /GoTo /D (subsection.6.1.3) >>
endobj
344 0 obj
(La tactique apply)
endobj
345 0 obj
<< /S /GoTo /D (subsection.6.1.4) >>
endobj
348 0 obj
(La tactique unfold)
endobj
349 0 obj
<< /S /GoTo /D (section.6.2) >>
endobj
352 0 obj
(Connecteurs logiques)
endobj
353 0 obj
<< /S /GoTo /D (subsection.6.2.1) >>
endobj
356 0 obj
(R\350gles d'introduction et d'\351limination)
endobj
357 0 obj
<< /S /GoTo /D (subsection.6.2.2) >>
endobj
360 0 obj
(Elimination du faux)
endobj
361 0 obj
<< /S /GoTo /D (subsection.6.2.3) >>
endobj
364 0 obj
(N\351gation)
endobj
365 0 obj
<< /S /GoTo /D (subsection.6.2.4) >>
endobj
368 0 obj
(Conjonction et disjonction)
endobj
369 0 obj
<< /S /GoTo /D (subsection.6.2.5) >>
endobj
372 0 obj
(\300 propos de repeat)
endobj
373 0 obj
<< /S /GoTo /D (subsection.6.2.6) >>
endobj
376 0 obj
(La quantification existentielle)
endobj
377 0 obj
<< /S /GoTo /D (section.6.3) >>
endobj
380 0 obj
(L'\351galit\351 et la r\351\351criture)
endobj
381 0 obj
<< /S /GoTo /D (subsection.6.3.1) >>
endobj
384 0 obj
(Introduction de l'\351galit\351)
endobj
385 0 obj
<< /S /GoTo /D (subsection.6.3.2) >>
endobj
388 0 obj
(Tactiques de r\351\351criture)
endobj
389 0 obj
<< /S /GoTo /D (subsection.6.3.3) >>
endobj
392 0 obj
(La tactique pattern)
endobj
393 0 obj
<< /S /GoTo /D (subsection.6.3.4) >>
endobj
396 0 obj
(* R\351\351critures conditionnelles)
endobj
397 0 obj
<< /S /GoTo /D (subsection.6.3.5) >>
endobj
400 0 obj
(Recherche de th\351or\350mes pour la r\351\351criture)
endobj
401 0 obj
<< /S /GoTo /D (subsection.6.3.6) >>
endobj
404 0 obj
(Autres tactiques li\351es \340 l'\351galit\351)
endobj
405 0 obj
<< /S /GoTo /D (section.6.4) >>
endobj
408 0 obj
(Tableau r\351capitulatif des tactiques)
endobj
409 0 obj
<< /S /GoTo /D (section.6.5) >>
endobj
412 0 obj
(*** D\351finitions impr\351dicatives)
endobj
413 0 obj
<< /S /GoTo /D (subsection.6.5.1) >>
endobj
416 0 obj
(Avertissement)
endobj
417 0 obj
<< /S /GoTo /D (subsection.6.5.2) >>
endobj
420 0 obj
(Le Vrai et le Faux)
endobj
421 0 obj
<< /S /GoTo /D (subsection.6.5.3) >>
endobj
424 0 obj
(Une curiosit\351 : l'\351galit\351 de Leibniz)
endobj
425 0 obj
<< /S /GoTo /D (subsection.6.5.4) >>
endobj
428 0 obj
(Quelques autres connecteurs logiques et quantificateurs)
endobj
429 0 obj
<< /S /GoTo /D (chapter.7) >>
endobj
432 0 obj
(Structures de donn\351es inductives)
endobj
433 0 obj
<< /S /GoTo /D (section.7.1) >>
endobj
436 0 obj
(Types sans r\351cursion)
endobj
437 0 obj
<< /S /GoTo /D (subsection.7.1.1) >>
endobj
440 0 obj
(Types \351num\351r\351s)
endobj
441 0 obj
<< /S /GoTo /D (subsection.7.1.2) >>
endobj
444 0 obj
(Raisonnements et calculs simples)
endobj
445 0 obj
<< /S /GoTo /D (subsection.7.1.3) >>
endobj
448 0 obj
(La tactique elim)
endobj
449 0 obj
<< /S /GoTo /D (subsection.7.1.4) >>
endobj
452 0 obj
(Construction de filtrage)
endobj
453 0 obj
<< /S /GoTo /D (subsection.7.1.5) >>
endobj
456 0 obj
(Types enregistrements)
endobj
457 0 obj
<< /S /GoTo /D (subsection.7.1.6) >>
endobj
460 0 obj
(Types enregistrements avec variantes)
endobj
461 0 obj
<< /S /GoTo /D (section.7.2) >>
endobj
464 0 obj
(Preuves par cas)
endobj
465 0 obj
<< /S /GoTo /D (subsection.7.2.1) >>
endobj
468 0 obj
(La tactique case)
endobj
469 0 obj
<< /S /GoTo /D (subsection.7.2.2) >>
endobj
472 0 obj
(\311galit\351s contradictoires)
endobj
473 0 obj
<< /S /GoTo /D (subsection.7.2.3) >>
endobj
476 0 obj
(** Les dessous de discriminate)
endobj
477 0 obj
<< /S /GoTo /D (subsection.7.2.4) >>
endobj
480 0 obj
(Constructeurs injectifs)
endobj
481 0 obj
<< /S /GoTo /D (subsection.7.2.5) >>
endobj
484 0 obj
(** Les dessous d'injection)
endobj
485 0 obj
<< /S /GoTo /D (subsection.7.2.6) >>
endobj
488 0 obj
(Types inductifs et \351galit\351s)
endobj
489 0 obj
<< /S /GoTo /D (subsection.7.2.7) >>
endobj
492 0 obj
(* Conseils dans l'utilisation de la tactique case)
endobj
493 0 obj
<< /S /GoTo /D (section.7.3) >>
endobj
496 0 obj
(Types avec r\351cursion)
endobj
497 0 obj
<< /S /GoTo /D (subsection.7.3.1) >>
endobj
500 0 obj
(Le type des entiers naturels)
endobj
501 0 obj
<< /S /GoTo /D (subsection.7.3.2) >>
endobj
504 0 obj
(D\351monstration par r\351currence sur les nombres naturels)
endobj
505 0 obj
<< /S /GoTo /D (subsection.7.3.3) >>
endobj
508 0 obj
(Programmation r\351cursive)
endobj
509 0 obj
<< /S /GoTo /D (subsection.7.3.4) >>
endobj
512 0 obj
(Variations dans les constructeurs)
endobj
513 0 obj
<< /S /GoTo /D (subsection.7.3.5) >>
endobj
516 0 obj
(** Constructeurs prenant des fonctions en arguments)
endobj
517 0 obj
<< /S /GoTo /D (subsection.7.3.6) >>
endobj
520 0 obj
(Raisonnement sur les fonctions r\351cursives)
endobj
521 0 obj
<< /S /GoTo /D (subsection.7.3.7) >>
endobj
524 0 obj
(Fonctions r\351cursives anonymes \(fix\))
endobj
525 0 obj
<< /S /GoTo /D (section.7.4) >>
endobj
528 0 obj
(Types polymorphes)
endobj
529 0 obj
<< /S /GoTo /D (subsection.7.4.1) >>
endobj
532 0 obj
(Le type des listes polymorphes)
endobj
533 0 obj
<< /S /GoTo /D (subsection.7.4.2) >>
endobj
536 0 obj
(Le type option)
endobj
537 0 obj
<< /S /GoTo /D (subsection.7.4.3) >>
endobj
540 0 obj
(Le type des couples)
endobj
541 0 obj
<< /S /GoTo /D (subsection.7.4.4) >>
endobj
544 0 obj
(Le type des sommes disjointes)
endobj
545 0 obj
<< /S /GoTo /D (section.7.5) >>
endobj
548 0 obj
(* Types inductifs d\351pendants)
endobj
549 0 obj
<< /S /GoTo /D (subsection.7.5.1) >>
endobj
552 0 obj
(Param\350tres du premier ordre)
endobj
553 0 obj
<< /S /GoTo /D (subsection.7.5.2) >>
endobj
556 0 obj
(Constructeurs \340 type d\351pendant variable)
endobj
557 0 obj
<< /S /GoTo /D (section.7.6) >>
endobj
560 0 obj
(* Types vides)
endobj
561 0 obj
<< /S /GoTo /D (subsection.7.6.1) >>
endobj
564 0 obj
(Types vides non d\351pendants)
endobj
565 0 obj
<< /S /GoTo /D (subsection.7.6.2) >>
endobj
568 0 obj
(D\351pendance et types vides)
endobj
569 0 obj
<< /S /GoTo /D (chapter.8) >>
endobj
572 0 obj
(Tactiques et automatisation)
endobj
573 0 obj
<< /S /GoTo /D (section.8.1) >>
endobj
576 0 obj
(Les tactiques des types inductifs)
endobj
577 0 obj
<< /S /GoTo /D (subsection.8.1.1) >>
endobj
580 0 obj
(Traitement par cas et r\351cursion)
endobj
581 0 obj
<< /S /GoTo /D (subsection.8.1.2) >>
endobj
584 0 obj
(Conversions)
endobj
585 0 obj
<< /S /GoTo /D (section.8.2) >>
endobj
588 0 obj
(Les tactiques auto et eauto)
endobj
589 0 obj
<< /S /GoTo /D (subsection.8.2.1) >>
endobj
592 0 obj
(Bases de tactiques : Hints)
endobj
593 0 obj
<< /S /GoTo /D (subsection.8.2.2) >>
endobj
596 0 obj
(* La tactique eauto)
endobj
597 0 obj
<< /S /GoTo /D (section.8.3) >>
endobj
600 0 obj
(Les tactiques num\351riques)
endobj
601 0 obj
<< /S /GoTo /D (subsection.8.3.1) >>
endobj
604 0 obj
(La tactique ring)
endobj
605 0 obj
<< /S /GoTo /D (subsection.8.3.2) >>
endobj
608 0 obj
(La tactique omega)
endobj
609 0 obj
<< /S /GoTo /D (subsection.8.3.3) >>
endobj
612 0 obj
(La tactique field)
endobj
613 0 obj
<< /S /GoTo /D (subsection.8.3.4) >>
endobj
616 0 obj
(La tactique fourier)
endobj
617 0 obj
<< /S /GoTo /D (section.8.4) >>
endobj
620 0 obj
(D\351cision pour la logique propositionnelle)
endobj
621 0 obj
<< /S /GoTo /D (section.8.5) >>
endobj
624 0 obj
(** Le langage de d\351finition de tactiques)
endobj
625 0 obj
<< /S /GoTo /D (subsection.8.5.1) >>
endobj
628 0 obj
(Liaison de param\350tres)
endobj
629 0 obj
<< /S /GoTo /D (subsection.8.5.2) >>
endobj
632 0 obj
(Constructions de filtrage)
endobj
633 0 obj
<< /S /GoTo /D (subsection.8.5.3) >>
endobj
636 0 obj
(Interactions avec la r\351duction)
endobj
637 0 obj
<< /S /GoTo /D (chapter.9) >>
endobj
640 0 obj
(Pr\351dicats inductifs)
endobj
641 0 obj
<< /S /GoTo /D (section.9.1) >>
endobj
644 0 obj
(Quelques propri\351t\351s inductives)
endobj
645 0 obj
<< /S /GoTo /D (subsection.9.1.1) >>
endobj
648 0 obj
(Quelques exemples)
endobj
649 0 obj
<< /S /GoTo /D (subsection.9.1.2) >>
endobj
652 0 obj
(Propri\351t\351s inductives et programmation logique)
endobj
653 0 obj
<< /S /GoTo /D (subsection.9.1.3) >>
endobj
656 0 obj
(Conseils pour les d\351finitions inductives)
endobj
657 0 obj
<< /S /GoTo /D (subsection.9.1.4) >>
endobj
660 0 obj
(L'exemple des listes tri\351es)
endobj
661 0 obj
<< /S /GoTo /D (section.9.2) >>
endobj
664 0 obj
(Propri\351t\351s inductives et connecteurs logiques)
endobj
665 0 obj
<< /S /GoTo /D (subsection.9.2.1) >>
endobj
668 0 obj
(Repr\351sentation de la v\351rit\351)
endobj
669 0 obj
<< /S /GoTo /D (subsection.9.2.2) >>
endobj
672 0 obj
(Repr\351sentation de la contradiction)
endobj
673 0 obj
<< /S /GoTo /D (subsection.9.2.3) >>
endobj
676 0 obj
(Repr\351sentation de la conjonction)
endobj
677 0 obj
<< /S /GoTo /D (subsection.9.2.4) >>
endobj
680 0 obj
(Repr\351sentation de la disjonction)
endobj
681 0 obj
<< /S /GoTo /D (subsection.9.2.5) >>
endobj
684 0 obj
(Repr\351sentation de la quantification existentielle)
endobj
685 0 obj
<< /S /GoTo /D (subsection.9.2.6) >>
endobj
688 0 obj
(Repr\351sentation inductive de l'\351galit\351)
endobj
689 0 obj
<< /S /GoTo /D (subsection.9.2.7) >>
endobj
692 0 obj
(*** \311galit\351 d\351pendante)
endobj
693 0 obj
<< /S /GoTo /D (subsection.9.2.8) >>
endobj
696 0 obj
(Pourquoi un principe de r\351currence exotique?)
endobj
697 0 obj
<< /S /GoTo /D (section.9.3) >>
endobj
700 0 obj
(Raisonnement sur les propri\351t\351s inductives)
endobj
701 0 obj
<< /S /GoTo /D (subsection.9.3.1) >>
endobj
704 0 obj
(Variantes structur\351es de intros)
endobj
705 0 obj
<< /S /GoTo /D (subsection.9.3.2) >>
endobj
708 0 obj
(Les tactiques constructor)
endobj
709 0 obj
<< /S /GoTo /D (subsection.9.3.3) >>
endobj
712 0 obj
(* R\351currence sur les pr\351dicats inductifs)
endobj
713 0 obj
<< /S /GoTo /D (subsection.9.3.4) >>
endobj
716 0 obj
(* R\351currence sur le)
endobj
717 0 obj
<< /S /GoTo /D (section.9.4) >>
endobj
720 0 obj
(* Relations inductives et fonctions)
endobj
721 0 obj
<< /S /GoTo /D (subsection.9.4.1) >>
endobj
724 0 obj
(Repr\351sentation de la fonction factorielle)
endobj
725 0 obj
<< /S /GoTo /D (subsection.9.4.2) >>
endobj
728 0 obj
(** Repr\351sentation de la s\351mantique d'un langage)
endobj
729 0 obj
<< /S /GoTo /D (subsection.9.4.3) >>
endobj
732 0 obj
(** Une d\351monstration en s\351mantique)
endobj
733 0 obj
<< /S /GoTo /D (section.9.5) >>
endobj
736 0 obj
(* Comportements \351labor\351s de la tactique elim)
endobj
737 0 obj
<< /S /GoTo /D (subsection.9.5.1) >>
endobj
740 0 obj
(Instancier les arguments)
endobj
741 0 obj
<< /S /GoTo /D (subsection.9.5.2) >>
endobj
744 0 obj
(Inversion)
endobj
745 0 obj
<< /S /GoTo /D (chapter.10) >>
endobj
748 0 obj
(* Les fonctions et leur sp\351cification)
endobj
749 0 obj
<< /S /GoTo /D (section.10.1) >>
endobj
752 0 obj
(Types inductifs pour les sp\351cifications)
endobj
753 0 obj
<< /S /GoTo /D (subsection.10.1.1) >>
endobj
756 0 obj
(Type \253 sous-ensemble \273)
endobj
757 0 obj
<< /S /GoTo /D (subsection.10.1.2) >>
endobj
760 0 obj
(Type sous-ensemble embo\356t\351)
endobj
761 0 obj
<< /S /GoTo /D (subsection.10.1.3) >>
endobj
764 0 obj
(Somme disjointe certifi\351e)
endobj
765 0 obj
<< /S /GoTo /D (subsection.10.1.4) >>
endobj
768 0 obj
(Somme disjointe hybride)
endobj
769 0 obj
<< /S /GoTo /D (section.10.2) >>
endobj
772 0 obj
(Sp\351cifications fortes)
endobj
773 0 obj
<< /S /GoTo /D (subsection.10.2.1) >>
endobj
776 0 obj
(Fonctions bien sp\351cifi\351es)
endobj
777 0 obj
<< /S /GoTo /D (subsection.10.2.2) >>
endobj
780 0 obj
(Construction de fonctions par preuves)
endobj
781 0 obj
<< /S /GoTo /D (subsection.10.2.3) >>
endobj
784 0 obj
(Fonctions partielles par pr\351condition)
endobj
785 0 obj
<< /S /GoTo /D (subsection.10.2.4) >>
endobj
788 0 obj
(** Complexit\351 des d\351monstrations de pr\351conditions)
endobj
789 0 obj
<< /S /GoTo /D (subsection.10.2.5) >>
endobj
792 0 obj
(** Renforcement des sp\351cifications)
endobj
793 0 obj
<< /S /GoTo /D (subsection.10.2.6) >>
endobj
796 0 obj
(*** Renforcement minimal de sp\351cification)
endobj
797 0 obj
<< /S /GoTo /D (subsection.10.2.7) >>
endobj
800 0 obj
(La tactique refine)
endobj
801 0 obj
<< /S /GoTo /D (section.10.3) >>
endobj
804 0 obj
(Variations sur la r\351cursion structurelle)
endobj
805 0 obj
<< /S /GoTo /D (subsection.10.3.1) >>
endobj
808 0 obj
(Fonctions r\351cursives structurelles \340 pas multiple)
endobj
809 0 obj
<< /S /GoTo /D (subsection.10.3.2) >>
endobj
812 0 obj
(Simplification du pas)
endobj
813 0 obj
<< /S /GoTo /D (subsection.10.3.3) >>
endobj
816 0 obj
(Fonctions r\351cursives \340 plusieurs arguments)
endobj
817 0 obj
<< /S /GoTo /D (section.10.4) >>
endobj
820 0 obj
(** Division binaire)
endobj
821 0 obj
<< /S /GoTo /D (subsection.10.4.1) >>
endobj
824 0 obj
(Division faiblement sp\351cifi\351e)
endobj
825 0 obj
<< /S /GoTo /D (subsection.10.4.2) >>
endobj
828 0 obj
(Division bien sp\351cifi\351e)
endobj
829 0 obj
<< /S /GoTo /D (chapter.11) >>
endobj
832 0 obj
(* Extraction et programmes imp\351ratifs)
endobj
833 0 obj
<< /S /GoTo /D (section.11.1) >>
endobj
836 0 obj
(Vers les langages fonctionnels)
endobj
837 0 obj
<< /S /GoTo /D (subsection.11.1.1) >>
endobj
840 0 obj
(Le m\351canisme d'extraction)
endobj
841 0 obj
<< /S /GoTo /D (subsection.11.1.2) >>
endobj
844 0 obj
(La dualit\351 Prop/Set et l'extraction)
endobj
845 0 obj
<< /S /GoTo /D (subsection.11.1.3) >>
endobj
848 0 obj
(Production effective de code OCAML)
endobj
849 0 obj
<< /S /GoTo /D (section.11.2) >>
endobj
852 0 obj
(** Description de programmes imp\351ratifs)
endobj
853 0 obj
<< /S /GoTo /D (subsection.11.2.1) >>
endobj
856 0 obj
(L'outil Why)
endobj
857 0 obj
<< /S /GoTo /D (subsection.11.2.2) >>
endobj
860 0 obj
(*** Les dessous de l'outil Why)
endobj
861 0 obj
<< /S /GoTo /D (chapter.12) >>
endobj
864 0 obj
(* \311tude de cas)
endobj
865 0 obj
<< /S /GoTo /D (section.12.1) >>
endobj
868 0 obj
(Les arbres binaires de recherche)
endobj
869 0 obj
<< /S /GoTo /D (subsection.12.1.1) >>
endobj
872 0 obj
(Les arbres de recherche en Coq)
endobj
873 0 obj
<< /S /GoTo /D (section.12.2) >>
endobj
876 0 obj
(Sp\351cification des programmes)
endobj
877 0 obj
<< /S /GoTo /D (subsection.12.2.1) >>
endobj
880 0 obj
(Test d'occurrence)
endobj
881 0 obj
<< /S /GoTo /D (subsection.12.2.2) >>
endobj
884 0 obj
(Programme d'insertion)
endobj
885 0 obj
<< /S /GoTo /D (subsection.12.2.3) >>
endobj
888 0 obj
(Programme de destruction)
endobj
889 0 obj
<< /S /GoTo /D (section.12.3) >>
endobj
892 0 obj
(Lemmes pr\351liminaires)
endobj
893 0 obj
<< /S /GoTo /D (section.12.4) >>
endobj
896 0 obj
(Vers la r\351alisation)
endobj
897 0 obj
<< /S /GoTo /D (subsection.12.4.1) >>
endobj
900 0 obj
(R\351alisation du test d'occurrence)
endobj
901 0 obj
<< /S /GoTo /D (subsection.12.4.2) >>
endobj
904 0 obj
(Insertion)
endobj
905 0 obj
<< /S /GoTo /D (subsection.12.4.3) >>
endobj
908 0 obj
(** Destruction)
endobj
909 0 obj
<< /S /GoTo /D (section.12.5) >>
endobj
912 0 obj
(Am\351liorations possibles)
endobj
913 0 obj
<< /S /GoTo /D (section.12.6) >>
endobj
916 0 obj
(Un autre exemple)
endobj
917 0 obj
<< /S /GoTo /D (chapter.13) >>
endobj
920 0 obj
(* Le syst\350me de modules)
endobj
921 0 obj
<< /S /GoTo /D (section.13.1) >>
endobj
924 0 obj
(Signatures)
endobj
925 0 obj
<< /S /GoTo /D (section.13.2) >>
endobj
928 0 obj
(Modules)
endobj
929 0 obj
<< /S /GoTo /D (subsection.13.2.1) >>
endobj
932 0 obj
(\311tapes de la construction d'un module)
endobj
933 0 obj
<< /S /GoTo /D (subsection.13.2.2) >>
endobj
936 0 obj
(Exemple : la notion de clef)
endobj
937 0 obj
<< /S /GoTo /D (subsection.13.2.3) >>
endobj
940 0 obj
(Modules param\351triques \(foncteurs\))
endobj
941 0 obj
<< /S /GoTo /D (section.13.3) >>
endobj
944 0 obj
(Une th\351orie : les relations d'ordre d\351cidables)
endobj
945 0 obj
<< /S /GoTo /D (subsection.13.3.1) >>
endobj
948 0 obj
(Enrichissement d'une th\351orie par foncteur)
endobj
949 0 obj
<< /S /GoTo /D (subsection.13.3.2) >>
endobj
952 0 obj
(Le produit lexicographique vu comme foncteur)
endobj
953 0 obj
<< /S /GoTo /D (section.13.4) >>
endobj
956 0 obj
(D\351veloppement d'un module : les dictionnaires)
endobj
957 0 obj
<< /S /GoTo /D (subsection.13.4.1) >>
endobj
960 0 obj
(Impl\351mentations enrichies)
endobj
961 0 obj
<< /S /GoTo /D (subsection.13.4.2) >>
endobj
964 0 obj
(Construction de dictionnaires par application de foncteurs)
endobj
965 0 obj
<< /S /GoTo /D (subsection.13.4.3) >>
endobj
968 0 obj
(Une impl\351mentation triviale)
endobj
969 0 obj
<< /S /GoTo /D (subsection.13.4.4) >>
endobj
972 0 obj
(Une impl\351mentation efficace)
endobj
973 0 obj
<< /S /GoTo /D (section.13.5) >>
endobj
976 0 obj
(Conclusion)
endobj
977 0 obj
<< /S /GoTo /D (chapter.14) >>
endobj
980 0 obj
(** Objets et preuves infinis)
endobj
981 0 obj
<< /S /GoTo /D (section.14.1) >>
endobj
984 0 obj
(Types co-inductifs)
endobj
985 0 obj
<< /S /GoTo /D (subsection.14.1.1) >>
endobj
988 0 obj
(La commande CoInductive)
endobj
989 0 obj
<< /S /GoTo /D (subsection.14.1.2) >>
endobj
992 0 obj
(Sp\351cificit\351 des types co-inductifs)
endobj
993 0 obj
<< /S /GoTo /D (subsection.14.1.3) >>
endobj
996 0 obj
(Listes infinies \(Flots\))
endobj
997 0 obj
<< /S /GoTo /D (subsection.14.1.4) >>
endobj
1000 0 obj
(Listes paresseuses)
endobj
1001 0 obj
<< /S /GoTo /D (subsection.14.1.5) >>
endobj
1004 0 obj
(Arbres finis ou infinis)
endobj
1005 0 obj
<< /S /GoTo /D (section.14.2) >>
endobj
1008 0 obj
(Technologie des types co-inductifs)
endobj
1009 0 obj
<< /S /GoTo /D (subsection.14.2.1) >>
endobj
1012 0 obj
(Construction d'objets finis)
endobj
1013 0 obj
<< /S /GoTo /D (subsection.14.2.2) >>
endobj
1016 0 obj
(D\351composition selon les constructeurs)
endobj
1017 0 obj
<< /S /GoTo /D (section.14.3) >>
endobj
1020 0 obj
(Construction d'objets infinis)
endobj
1021 0 obj
<< /S /GoTo /D (subsection.14.3.1) >>
endobj
1024 0 obj
(Tentatives infructueuses)
endobj
1025 0 obj
<< /S /GoTo /D (subsection.14.3.2) >>
endobj
1028 0 obj
(La commande CoFixpoint)
endobj
1029 0 obj
<< /S /GoTo /D (subsection.14.3.3) >>
endobj
1032 0 obj
(Quelques constructions par co-point-fixe)
endobj
1033 0 obj
<< /S /GoTo /D (subsection.14.3.4) >>
endobj
1036 0 obj
(Exemples de d\351finitions mal form\351es)
endobj
1037 0 obj
<< /S /GoTo /D (section.14.4) >>
endobj
1040 0 obj
(Techniques de d\351pliage)
endobj
1041 0 obj
<< /S /GoTo /D (subsection.14.4.1) >>
endobj
1044 0 obj
(D\351composition syst\351matique)
endobj
1045 0 obj
<< /S /GoTo /D (subsection.14.4.2) >>
endobj
1048 0 obj
(Simplification et d\351composition)
endobj
1049 0 obj
<< /S /GoTo /D (subsection.14.4.3) >>
endobj
1052 0 obj
(Utilisation des lemmes de d\351composition)
endobj
1053 0 obj
<< /S /GoTo /D (section.14.5) >>
endobj
1056 0 obj
(Pr\351dicats inductifs sur un type co-inductif)
endobj
1057 0 obj
<< /S /GoTo /D (subsection.14.5.1) >>
endobj
1060 0 obj
(Le pr\351dicat \253 \352tre un flot fini \273)
endobj
1061 0 obj
<< /S /GoTo /D (section.14.6) >>
endobj
1064 0 obj
(Propri\351t\351s co-inductives)
endobj
1065 0 obj
<< /S /GoTo /D (subsection.14.6.1) >>
endobj
1068 0 obj
(Le pr\351dicat \253 \352tre infini \273)
endobj
1069 0 obj
<< /S /GoTo /D (subsection.14.6.2) >>
endobj
1072 0 obj
(Construction de preuves infinies)
endobj
1073 0 obj
<< /S /GoTo /D (subsection.14.6.3) >>
endobj
1076 0 obj
(Manque de respect de la garde)
endobj
1077 0 obj
<< /S /GoTo /D (subsection.14.6.4) >>
endobj
1080 0 obj
(Techniques d'\351limination)
endobj
1081 0 obj
<< /S /GoTo /D (section.14.7) >>
endobj
1084 0 obj
(L'\351galit\351 extensionnelle \(bisimilarit\351\))
endobj
1085 0 obj
<< /S /GoTo /D (subsection.14.7.1) >>
endobj
1088 0 obj
(Le probl\350me)
endobj
1089 0 obj
<< /S /GoTo /D (subsection.14.7.2) >>
endobj
1092 0 obj
(Le pr\351dicat bisimilar)
endobj
1093 0 obj
<< /S /GoTo /D (subsection.14.7.3) >>
endobj
1096 0 obj
(Quelques r\351sultats int\351ressants)
endobj
1097 0 obj
<< /S /GoTo /D (section.14.8) >>
endobj
1100 0 obj
(Le principe de Park)
endobj
1101 0 obj
<< /S /GoTo /D (section.14.9) >>
endobj
1104 0 obj
(LTL)
endobj
1105 0 obj
<< /S /GoTo /D (section.14.10) >>
endobj
1108 0 obj
(Exemple d'\351tude : syst\350mes de transitions)
endobj
1109 0 obj
<< /S /GoTo /D (subsection.14.10.1) >>
endobj
1112 0 obj
(D\351finitions)
endobj
1113 0 obj
<< /S /GoTo /D (section.14.11) >>
endobj
1116 0 obj
(Exploration des types co-inductifs)
endobj
1117 0 obj
<< /S /GoTo /D (chapter.15) >>
endobj
1120 0 obj
(** Fondements des types inductifs)
endobj
1121 0 obj
<< /S /GoTo /D (section.15.1) >>
endobj
1124 0 obj
(R\350gles de bonne formation)
endobj
1125 0 obj
<< /S /GoTo /D (subsection.15.1.1) >>
endobj
1128 0 obj
(Le type inductif lui-m\352me)
endobj
1129 0 obj
<< /S /GoTo /D (subsection.15.1.2) >>
endobj
1132 0 obj
(Formation des constructeurs)
endobj
1133 0 obj
<< /S /GoTo /D (subsection.15.1.3) >>
endobj
1136 0 obj
(Comment se construit le principe de r\351currence)
endobj
1137 0 obj
<< /S /GoTo /D (subsection.15.1.4) >>
endobj
1140 0 obj
(Typage des r\351curseurs)
endobj
1141 0 obj
<< /S /GoTo /D (subsection.15.1.5) >>
endobj
1144 0 obj
(Principes de r\351currence des propri\351t\351s inductives)
endobj
1145 0 obj
<< /S /GoTo /D (subsection.15.1.6) >>
endobj
1148 0 obj
(La commande Scheme)
endobj
1149 0 obj
<< /S /GoTo /D (section.15.2) >>
endobj
1152 0 obj
(*** Filtrage et r\351cursion sur des preuves)
endobj
1153 0 obj
<< /S /GoTo /D (subsection.15.2.1) >>
endobj
1156 0 obj
(Restriction sur le filtrage)
endobj
1157 0 obj
<< /S /GoTo /D (subsection.15.2.2) >>
endobj
1160 0 obj
(Rel\342chement de la restriction)
endobj
1161 0 obj
<< /S /GoTo /D (subsection.15.2.3) >>
endobj
1164 0 obj
(R\351cursion)
endobj
1165 0 obj
<< /S /GoTo /D (subsection.15.2.4) >>
endobj
1168 0 obj
(\311limination forte)
endobj
1169 0 obj
<< /S /GoTo /D (section.15.3) >>
endobj
1172 0 obj
(Types mutuellement inductifs)
endobj
1173 0 obj
<< /S /GoTo /D (subsection.15.3.1) >>
endobj
1176 0 obj
(Arbres et for\352ts)
endobj
1177 0 obj
<< /S /GoTo /D (subsection.15.3.2) >>
endobj
1180 0 obj
(D\351monstration par r\351currence mutuelle)
endobj
1181 0 obj
<< /S /GoTo /D (subsection.15.3.3) >>
endobj
1184 0 obj
(*** Arbres et listes d'arbres)
endobj
1185 0 obj
<< /S /GoTo /D (chapter.16) >>
endobj
1188 0 obj
(* R\351cursivit\351 g\351n\351rale)
endobj
1189 0 obj
<< /S /GoTo /D (section.16.1) >>
endobj
1192 0 obj
(R\351cursion born\351e)
endobj
1193 0 obj
<< /S /GoTo /D (section.16.2) >>
endobj
1196 0 obj
(** Fonctions r\351cursives bien fond\351es)
endobj
1197 0 obj
<< /S /GoTo /D (subsection.16.2.1) >>
endobj
1200 0 obj
(Relations bien fond\351es)
endobj
1201 0 obj
<< /S /GoTo /D (subsection.16.2.2) >>
endobj
1204 0 obj
(Preuves d'accessibilit\351)
endobj
1205 0 obj
<< /S /GoTo /D (subsection.16.2.3) >>
endobj
1208 0 obj
(Construction de relations bien fond\351es)
endobj
1209 0 obj
<< /S /GoTo /D (subsection.16.2.4) >>
endobj
1212 0 obj
(R\351cursion bien fond\351e)
endobj
1213 0 obj
<< /S /GoTo /D (subsection.16.2.5) >>
endobj
1216 0 obj
(Le r\351curseur well\137founded\137induction)
endobj
1217 0 obj
<< /S /GoTo /D (subsection.16.2.6) >>
endobj
1220 0 obj
(Division euclidienne bien fond\351e)
endobj
1221 0 obj
<< /S /GoTo /D (subsection.16.2.7) >>
endobj
1224 0 obj
(R\351cursion imbriqu\351e)
endobj
1225 0 obj
<< /S /GoTo /D (section.16.3) >>
endobj
1228 0 obj
(** R\351cursion g\351n\351rale par it\351ration)
endobj
1229 0 obj
<< /S /GoTo /D (subsection.16.3.1) >>
endobj
1232 0 obj
(Fonctionnelle associ\351e \340 une fonction r\351cursive)
endobj
1233 0 obj
<< /S /GoTo /D (subsection.16.3.2) >>
endobj
1236 0 obj
(Construction de la fonction cherch\351e)
endobj
1237 0 obj
<< /S /GoTo /D (subsection.16.3.3) >>
endobj
1240 0 obj
(D\351monstration de l'\351quation de point fixe)
endobj
1241 0 obj
<< /S /GoTo /D (subsection.16.3.4) >>
endobj
1244 0 obj
(Utilisation de l'\351quation de point fixe)
endobj
1245 0 obj
<< /S /GoTo /D (subsection.16.3.5) >>
endobj
1248 0 obj
(Discussion)
endobj
1249 0 obj
<< /S /GoTo /D (section.16.4) >>
endobj
1252 0 obj
(*** R\351cursion sur un pr\351dicat ad-hoc)
endobj
1253 0 obj
<< /S /GoTo /D (chapter.17) >>
endobj
1256 0 obj
(* D\351monstration par r\351flexion)
endobj
1257 0 obj
<< /S /GoTo /D (section.17.1) >>
endobj
1260 0 obj
(Pr\351sentation g\351n\351rale)
endobj
1261 0 obj
<< /S /GoTo /D (section.17.2) >>
endobj
1264 0 obj
(D\351monstrations par calcul direct)
endobj
1265 0 obj
<< /S /GoTo /D (section.17.3) >>
endobj
1268 0 obj
(** D\351monstrations par calcul alg\351brique)
endobj
1269 0 obj
<< /S /GoTo /D (subsection.17.3.1) >>
endobj
1272 0 obj
(D\351monstrations modulo associativit\351)
endobj
1273 0 obj
<< /S /GoTo /D (subsection.17.3.2) >>
endobj
1276 0 obj
(Abstraire sur le type et l'op\351rateur)
endobj
1277 0 obj
<< /S /GoTo /D (subsection.17.3.3) >>
endobj
1280 0 obj
(*** Tri de variables pour la commutativit\351)
endobj
1281 0 obj
<< /S /GoTo /D (section.17.4) >>
endobj
1284 0 obj
(Conclusion)
endobj
1285 0 obj
<< /S /GoTo /D (chapter*.182) >>
endobj
1288 0 obj
(Annexes)
endobj
1289 0 obj
<< /S /GoTo /D (section*.183) >>
endobj
1292 0 obj
(Tri par insertion : le code)
endobj
1293 0 obj
<< /S /GoTo /D (chapter*.184) >>
endobj
1296 0 obj
(Index)
endobj
1297 0 obj
<< /S /GoTo /D (section*.185) >>
endobj
1300 0 obj
(Coq et biblioth\350ques)
endobj
1301 0 obj
<< /S /GoTo /D (section*.185) >>
endobj
1303 0 obj
(Exemples du livre)
endobj
1304 0 obj
<< /S /GoTo /D [1305 0 R /Fit ] >>
endobj
1307 0 obj <<
/Length 196
/Filter /FlateDecode
>>
stream
x�u�1o1 ����H�&� |��RաC���H
� @���D醺�~O~�l� l:��/b��&4X&�C<�������C����H�8rjyц{u�5��'m�b�(����������D,J#lj����J���A-R�.�K���I9�6/�itB�p�ppb ��y�9j��e���%� F��zz|���@�
endstream
endobj
1305 0 obj <<
/Type /Page
/Contents 1307 0 R
/Resources 1306 0 R
/MediaBox [0 0 612 792]
/Parent 1312 0 R
>> endobj
1308 0 obj <<
/D [1305 0 R /XYZ 105.869 699.082 null]
>> endobj
1309 0 obj <<
/D [1305 0 R /XYZ 106.869 668.127 null]
>> endobj
1306 0 obj <<
/Font << /F18 1310 0 R /F19 1311 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
1315 0 obj <<
/Length 68
/Filter /FlateDecode
>>
stream
x�3PHW0Pp�r
��w34U�Գ432SIS043�333W0�0�342WIQ��0Ҍ
��2�jB�]C���&
endstream
endobj
1314 0 obj <<
/Type /Page
/Contents 1315 0 R
/Resources 1313 0 R
/MediaBox [0 0 612 792]
/Parent 1312 0 R
>> endobj
1316 0 obj <<
/D [1314 0 R /XYZ 159.667 699.082 null]
>> endobj
1313 0 obj <<
/Font << /F15 1317 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
1353 0 obj <<
/Length 1211
/Filter /FlateDecode
>>
stream
x��Y]s�6}ϯ�-b�P}#�O�v�ig��4�Ӧ��W�L���WH"�=�;�6v^bB�9�:��k <8�����V_��q@y������`+�"Q1��j |D�P%(���0b
