Browse Source

first commit

master
zapashcanon 5 years ago
commit
8789447d8c
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. 12
      .gitignore
  2. 13
      Makefile
  3. 4
      img/simple_bdd.dot
  4. 8
      img/simple_bdd2.dot
  5. 8
      img/simple_bdd3.dot
  6. 6
      img/simple_bdd4.dot
  7. 4
      img/simple_bdd5.dot
  8. 3
      img/simple_bdd6.dot
  9. 19
      img/simple_bdd7.dot
  10. 542
      img/universite-paris-saclay.svg
  11. 13
      scripts/build.sh
  12. 10
      scripts/clean.sh
  13. 9
      scripts/mrproper.sh
  14. 16
      scripts/test.sh
  15. 3
      src/abstract.tex
  16. 1
      src/app.tex
  17. 1
      src/appendix.tex
  18. 91
      src/bdd.tex
  19. 86
      src/bib.bib
  20. 1
      src/conclusion.tex
  21. 1
      src/implem.tex
  22. 8
      src/introduction.tex
  23. 27
      src/main.tex
  24. 75
      src/packages.tex
  25. 27
      src/title.tex

12
.gitignore

@ -0,0 +1,12 @@
*.pdf
*.bbl
*.bcf
*.blg
*.log
*.run.xml
*.aux
*.out
*.cmi
*.cmx
*.o
src/svg-inkscape/

13
Makefile

@ -0,0 +1,13 @@
default: build clean
build:
scripts/build.sh
clean:
scripts/clean.sh
test:
scripts/test.sh
mrproper: clean
scripts/mrproper.sh

4
img/simple_bdd.dot

@ -0,0 +1,4 @@
digraph G {
P -> ⊥ [style="dashed"]
P -> ⊤
}

8
img/simple_bdd2.dot

@ -0,0 +1,8 @@
digraph G {
T1 [label="⊤"]
T2 [label="⊤"]
P -> Q [style="dashed"]
P -> T1
Q -> ⊥ [style="dashed"]
Q -> T2
}

8
img/simple_bdd3.dot

@ -0,0 +1,8 @@
digraph G {
T1 [label="⊤"]
T2 [label="⊤"]
Q -> P [style="dashed"]
Q -> T1
P -> ⊥ [style="dashed"]
P -> T2
}

6
img/simple_bdd4.dot

@ -0,0 +1,6 @@
digraph G {
P -> Q [style="dashed"]
P -> ⊤
Q -> ⊥ [style="dashed"]
Q -> ⊤
}

4
img/simple_bdd5.dot

@ -0,0 +1,4 @@
digraph G {
P -> ⊤
P -> ⊤ [style="dashed"]
}

3
img/simple_bdd6.dot

@ -0,0 +1,3 @@
digraph G {
⊤;
}

19
img/simple_bdd7.dot

@ -0,0 +1,19 @@
digraph G {
P;
Q1 [label="Q"];
Q2 [label="Q"];
T [label="⊤"];
B1 [label="⊥"];
B2 [label="⊥"];
B3 [label="⊥"];
P -> Q1
P -> Q2 [style="dashed"]
Q1 -> T
Q1 -> B1 [style="dashed"]
Q2 -> B2
Q2 -> B3 [style="dashed"]
}

542
img/universite-paris-saclay.svg

@ -0,0 +1,542 @@
<?xml version="1.0" encoding="utf-8"?>
<!-- Generator: Adobe Illustrator 19.1.0, SVG Export Plug-In . SVG Version: 6.00 Build 0) -->
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd" [
<!ENTITY ns_extend "http://ns.adobe.com/Extensibility/1.0/">
<!ENTITY ns_ai "http://ns.adobe.com/AdobeIllustrator/10.0/">
<!ENTITY ns_graphs "http://ns.adobe.com/Graphs/1.0/">
<!ENTITY ns_vars "http://ns.adobe.com/Variables/1.0/">
<!ENTITY ns_imrep "http://ns.adobe.com/ImageReplacement/1.0/">
<!ENTITY ns_sfw "http://ns.adobe.com/SaveForWeb/1.0/">
<!ENTITY ns_custom "http://ns.adobe.com/GenericCustomNamespace/1.0/">
<!ENTITY ns_adobe_xpath "http://ns.adobe.com/XPath/1.0/">
]>
<svg version="1.1" id="Calque_1" xmlns:x="&ns_extend;" xmlns:i="&ns_ai;" xmlns:graph="&ns_graphs;"
xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px" viewBox="0 0 258.6 87.5"
style="enable-background:new 0 0 258.6 87.5;" xml:space="preserve">
<style type="text/css">
.st0{fill:#62003C;}
</style>
<switch>
<foreignObject requiredExtensions="&ns_ai;" x="0" y="0" width="1" height="1">
<i:pgfRef xlink:href="#adobe_illustrator_pgf">
</i:pgfRef>
</foreignObject>
<g i:extraneous="self">
<g>
<circle class="st0" cx="251.3" cy="7.3" r="7.3"/>
<circle class="st0" cx="235.5" cy="21.1" r="4.5"/>
<path class="st0" d="M53.6,75.4L53.6,75.4c0-3.7-2.5-5.9-6.7-5.9h-8.1v17.7h3.9v-5.6h3.1l3.8,5.6h4.5l-4.3-6.3
C52.1,80,53.6,78.3,53.6,75.4z M49.7,75.6c0,1.5-1.1,2.5-3,2.5h-3.9V73h3.9C48.5,73,49.7,73.9,49.7,75.6L49.7,75.6z"/>
<path class="st0" d="M76.5,76.6c-3.1-0.8-3.8-1.2-3.8-2.3v0c0-0.9,0.8-1.5,2.3-1.5c1.5,0,3,0.7,4.6,1.7l2-2.9
c-1.8-1.4-4-2.2-6.6-2.2c-3.6,0-6.2,2.1-6.2,5.3v0.1c0,3.5,2.3,4.5,5.9,5.4c3,0.8,3.6,1.3,3.6,2.2v0.1c0,1-1,1.7-2.5,1.7
c-2,0-3.7-0.8-5.3-2.1l-2.3,2.8c2.1,1.9,4.8,2.8,7.5,2.8c3.8,0,6.5-2,6.5-5.5v-0.1C82.1,78.8,80.1,77.5,76.5,76.6z"/>
<rect x="86.5" y="77.5" class="st0" width="7.8" height="3.7"/>
<path class="st0" d="M23.1,69.4l-7.6,17.8h4l1.6-4h7.5l1.6,4h4.1l-7.6-17.8H23.1z M22.5,79.8l2.3-5.7l2.3,5.7H22.5z"/>
<path class="st0" d="M7.3,69.5H0.1v17.7H4v-5.3h3c4,0,7.1-2.1,7.1-6.2v0C14.1,72,11.5,69.5,7.3,69.5z M10.1,75.8
c0,1.5-1.1,2.7-3.1,2.7H4V73h3C8.9,73,10.1,74,10.1,75.8L10.1,75.8z"/>
<rect x="59.2" y="69.5" class="st0" width="3.9" height="17.7"/>
<path class="st0" d="M123.3,69.4l-7.6,17.8h4l1.6-4h7.5l1.6,4h4.1l-7.6-17.8H123.3z M122.7,79.8l2.3-5.7l2.3,5.7H122.7z"/>
<polygon class="st0" points="162.3,69.5 158.4,69.5 158.4,87.2 171.1,87.2 171.1,83.6 162.3,83.6 "/>
<path class="st0" d="M146.3,83.9c-3,0-5.1-2.5-5.1-5.5v-0.1c0-3,2.1-5.5,5.1-5.5c1.8,0,3.2,0.8,4.5,2l2.5-2.8
c-1.6-1.6-3.6-2.7-7-2.7c-5.4,0-9.2,4.1-9.2,9.1v0c0,5.1,3.9,9.1,9.1,9.1c3.4,0,5.4-1.2,7.2-3.2l-2.5-2.5
C149.6,83.1,148.3,83.9,146.3,83.9z"/>
<polygon class="st0" points="201.9,76.6 197.7,69.5 193.1,69.5 199.9,80.2 199.9,87.2 203.8,87.2 203.8,80.1 210.6,69.5
206.2,69.5 "/>
<path class="st0" d="M106.7,76.6c-3.1-0.8-3.8-1.2-3.8-2.3v0c0-0.9,0.8-1.5,2.3-1.5c1.5,0,3,0.7,4.6,1.7l2-2.9
c-1.8-1.4-4-2.2-6.6-2.2c-3.6,0-6.2,2.1-6.2,5.3v0.1c0,3.5,2.3,4.5,5.9,5.4c3,0.8,3.6,1.3,3.6,2.2v0.1c0,1-1,1.7-2.5,1.7
c-2,0-3.7-0.8-5.3-2.1l-2.3,2.8c2.1,1.9,4.8,2.8,7.5,2.8c3.8,0,6.5-2,6.5-5.5v-0.1C112.3,78.8,110.3,77.5,106.7,76.6z"/>
<path class="st0" d="M182,69.4l-7.6,17.8h4l1.6-4h7.5l1.6,4h4.1l-7.6-17.8H182z M181.4,79.8l2.3-5.7l2.3,5.7H181.4z"/>
<rect x="65.8" y="33.2" class="st0" width="4.9" height="27.4"/>
<path class="st0" d="M121.4,61.2c4.6,0,8.1-1.6,11.2-5.1l0.3-0.3l-3.1-2.8l-0.3,0.3c-2.3,2.5-4.9,3.6-8,3.6c-4.6,0-8.1-3.2-8.8-8
h20.9l0-0.4c0.1-0.5,0.1-0.9,0.1-1.3c0-8.7-5.1-14.5-12.8-14.5c-7.5,0-13.1,6.1-13.1,14.3C107.8,55.1,113.7,61.2,121.4,61.2z
M120.8,36.9c5.1,0,7.4,4.1,7.9,8.1h-16C113.4,40.2,116.7,36.9,120.8,36.9z"/>
<path class="st0" d="M10.6,61.2c3.6,0,6.4-1.4,8.6-4.2v3.6H24V33.2h-4.8v15.6c0,4.6-3.1,7.8-7.5,7.8c-4.3,0-6.9-2.8-6.9-7.5V33.2
H0v16.9C0,56.8,4.2,61.2,10.6,61.2z"/>
<path class="st0" d="M46.4,32.7c-3.6,0-6.5,1.4-8.6,4.1v-3.6h-4.9v27.4h4.9V45c0-4.6,3.1-7.8,7.5-7.8c4.3,0,6.9,2.8,6.9,7.5v15.9
H57V43.7C57,37,52.8,32.7,46.4,32.7z"/>
<polygon class="st0" points="93,60.8 104.9,33.2 99.7,33.2 91,54.4 82.4,33.2 77.1,33.2 88.9,60.8 "/>
<path class="st0" d="M145.6,38.7v-5.5h-4.9v27.4h4.9v-11c0-7.1,3.9-11.7,10-11.7h0.8v-5.1l-0.4,0
C151.7,32.6,147.9,34.8,145.6,38.7z"/>
<path class="st0" d="M210,24.2l-4.9,2.7v6.3H200v4.4h5.1v15.5c0,5.1,2.8,7.9,7.9,7.9c1.8,0,3.4-0.4,5-1.2l0.2-0.1v-4.4l-0.7,0.3
c-1.3,0.6-2.3,0.9-3.6,0.9c-2.7,0-4-1.3-4-3.9v-15h8.4v-4.4H210V24.2z"/>
<path class="st0" d="M235.8,32.7c-7.5,0-13.1,6.1-13.1,14.3c0,8.1,5.9,14.3,13.7,14.3c4.6,0,8.1-1.6,11.2-5.1l0.3-0.3l-3.1-2.8
l-0.3,0.3c-2.3,2.5-4.9,3.6-8,3.6c-4.6,0-8.1-3.2-8.8-8h20.9l0-0.4c0.1-0.5,0.1-0.9,0.1-1.3C248.6,38.5,243.5,32.7,235.8,32.7z
M227.7,45c0.7-4.8,3.9-8.1,8.1-8.1c5.1,0,7.4,4.1,7.9,8.1H227.7z"/>
<path class="st0" d="M181.5,52.7v-0.1c0-5.4-5.3-7-8.8-8l-0.1,0c-3.3-1-6.4-1.9-6.4-4.2c0-2,1.9-3.4,4.7-3.4
c2.4,0,5.1,0.9,7.6,2.5l0.4,0.3l2.3-3.8l-0.4-0.2c-2.8-1.9-6.5-3-9.8-3c-5.6,0-9.5,3.3-9.5,8v0.1c0,5.3,5.2,6.8,9.1,7.9
c3.5,1,6.3,1.9,6.3,4.3c0,2.2-2,3.7-5,3.7c-2.9,0-6-1.1-8.9-3.3l-0.4-0.3l-2.5,3.6l0.3,0.3c3,2.5,7.3,4,11.2,4
C177.6,61.1,181.5,57.7,181.5,52.7z"/>
<rect x="189.3" y="33.2" class="st0" width="4.9" height="27.4"/>
</g>
</g>
</switch>
<i:pgf id="adobe_illustrator_pgf">
<![CDATA[
eJzsvfleMknSMHpugHsAFUWRolaqyl1B3HB53HdFQOURAVm6p+eP73rOXMfc2InI2rKqshaWfpfz
TfevbaCiMiMjY8+MzHTq7CK3Xe+8NXISxycT6XSx16gOOr2VJPk1edBqDfuDHv6UOV9MCirHA9D2
gfZiAl43ev1mp72SFHROIA/L+HZmZ/jPf1a/qqVtcTGZWYSfL5uDVgMeVDofndzV2UW11qr+xfX/
+Fi0eoVmStUBwAhqnpfyIi8UkoKyoggIUG3/Ue33m//ExwVJk+C3nc6wXW+2P3Y6/1hJ6kJSLEhJ
SRHwP3i63zxv9D0gXEFQeV6WdFmRBAlf4ISCLgmCIkqypMGbPCfyuqqqmiTykkB+KMiarGsKtKoU
oN1Spzb8brQHZ71OrdHvFzutTq+/kiz+VW0nj6sf8KSavGu0Wp0/kzutau0rAdRSXsrNVgMI810d
JAUJybR9IIgvO8Nmq34y/H5rAMlEHX+VXkiLV31oClrFz/iz+nLwDb9cNAYDGA70h5QuHt8d0WgA
acx/Mw/nje6//9WDV54WzWZ7ne53tffVnxIhsM3Lxne3BVNGyCuLPKfAKArwl/psQsL4CVRO0ESO
1woFXtO0giroSVHlZF7TeYUXdXhDTxZ4ntMFSdIFQZBETUgqWoEGUY0mnYlo/NFs/LmSPOm0Gwa1
t3uDC4NVZJnnjb/Gk/Nhq9G7ajcHQAYyCN2g93Gn3mjBHNjvl1tVQmbyr+D8NQAuq72PxgAYrNMa
Dgj7a1YPMJ2V6l8N5AmBTLP6stP4aLahn/YA0H1pvr/8YQjNy8dgRVANMP3ltNtoX3auyVAUheMl
UeLlgi5rBUVMwlRxmq4LvAJjKWhJmVNVCSZOFEFGREGDKSQ4yvAVfrfQFpy/Ji7brUGj14Y5s/D5
r+x8t11/MRVGo04joBAEsHuLdjDJ6TNg39NeE4i3wgPjGHKw12vWHTFQxaRm/CGzw8E04D+CoAP7
inrcX3Tyj1oQFE2QxTi/GGQDLhnAGKypFl+Kx5SI8tzxKQwDRl3sfCOr9lFrITOA1LY6H8Yz+zN5
Aq8PuwZJDLYBrj7rNdvYZuKEPNFezlpDeLTX6wy7B+33TiJjKOszRKbXPm3Dh8/kTm/Y/0xedjot
0MDA38D5ycY/EKBhKndUSI1kvZH87gya7wAFfG+8TN7FV7lqs7v4P69T+53QDo2uqr1Bsz9o/gxN
DP73dFmstlrNj161+9msxei15oDTPdOtjNA5sHYPZpc8hFbIV+v/0W9f1AhbxOeH5vv7sI8dmG+O
gOl/ZV/XjRo4PWBb6snTt9/wBVoxf+sTDwY5u7XQRGPtPPpnDIqdgdrrAnjzD4vqSQKDvBMFQD2K
LbDJ3XoTcAvoKxTm4s/qoPZZab71o3urNNs+dG2nEumFAPhbvVF1nKQYk/7VABxCWzZAxmjbkPJW
o13v+zmp9CgKBRCnOv4fZ/sdmapvi1sFJsF4N8Yg/vp+67Sa/W8kqvXZkdwz1CO1VuPir/6g8R3d
XKmBuDgyy5SB3fYfjVan28UOjBdiEKRVbVd7NpU97Z41wDwNQVnU/2pXv4nuqS/YY4BXG4PbsD6Q
3O/Ndh1E+GLYHBAtYyi0zne300c60zSxgC/sNhXiWFCGMpeLsqCGFSaYGHJsDdVQIscw3g/A57QH
HS2GP0uGKus8/B0Co/of5xeTnIEMOgE0KlMeUpAZSWSCUINH6E6JclJA95k3PDrR8OymirZuPEGH
ffBXq9FP5I/anT/b5EtyJZF5ABlI1v/9r/fqcPC0mMyfVIEvlhP5iyZEHg0LjE+eJnjT7/yCT+cJ
ywc9SljeO5+8/Qu+HMKH3/DTnzCs5HHy4YlP1uHn2/MEuqq39UT+rAoYJlcTyTyIB/yfYAnDcnCM
HOhZtQVeYINgcfaWYEZliFA/4Q7UzmqJsx27eauVUQhYAb/DSzXfCAjQOLMl8MYjQ1dhM/+P+TM0
5PkxoHETXyt4g4C/mki/5K3vMJn4rVlDDV7t/WV8vz2unECAxny4msz847vVhsc5MFq95ttw0AC1
vYyg271e9b+miSm0T0HVPputeq/RNmDEZP4AKGM/xT+Dv1CB49PMfLv/8ke1118F8biA1tsfbtA/
qq2hBYu/9wPgQHebYCYmfde3/6XUaXfQvYgkTKtT+2rU41DGglz+7x3XW5MktoQYYwPmgKjyhAwi
enw09JSmf0JKCKGUiDX+ZvWt1YjD+JGz+t8s6DVwbzvff5eo/2/SYit/xB4cgsZn5b+PD1f6VfRa
0OaBiMVlx79dLgCX/0Go/LeT5bsxqNZhiibFQ58Qj9m66RPF4XMKGH/hzb4x6b/da1S3SW7Ar7U9
Iq5qBZFeGkhqgqRymPDnBRnT/8n8eaPaOus0MW37ksyQdLqRonV3XGr2u63qX8fV3pc5HAwEMVyG
6PyParOVFGFYV+1mDUZijc4xOoLREYR72+fGL74VCd+ahYPaeaN12Tk30CJonnX6TRwneSqa0+Nd
BPEuccRuULBx3oGwKpk56IOj/dap9uoQQFSHLZcxNefLgiBzYVLo4fzf/7IWFJLfnb8a7TbGCV4q
gb8tJG1/meSLk2YeGqLSs16j3xgkKVIqvEVM8L6Txw0I/86rfQjdm/808iTOMoZJat71xulw0B0O
It6xtDsLuUq1/TGEACd51uli/mCZwXlSweqyW63XPQTtdzsOXxs/VVvNvuen72rf5DXFRKbWafWM
X1QLv3q3ydlCs32Q3B4OOvbQGt6x6Mit7X63CkJd+yv50WvWk30bThFlUaNgq+acJmu4ogTh8pst
zDaShD6WrCabQMTqoAGADeLNhQJ/tcHz7MBMfBhpGA+onuxWu8AA/eb3sFV1ZkYIxDDmKD56DUul
RcL2LM+4oIAQBUMKI0BS/UfCOhQni8Q2qMWRxjLyhT2FgovURHZ6fzSSl41/DEjus/rWbDUHloDy
nLFylLQ+UJr54nrvBdevdjr/uL0zqaXpmkV9KkOLC1gvlcb7YMdGVhLVghoAWW51Or1zi1qiI81e
wH1MNHfa+43mx+fAkv0g4GKj1Sp2hpa9CG6VdH/ardZsMtDsySffbc0DrNnCZG9/0Ot8WX5VxtgW
QBHqa/ugPGy1rBkxlwPhqb/1AtV6tT1oJkHqq31LSYUNzZnhKGwHMNVRNMDJcpFADqTrORK/XK01
ttsfrRizS+D3KAkLRIJAurCI5BqHwRTNYlleFJRA7HGgu/8Y+NwIJi5O67RYMkFt9o2JB3mJRkTW
AumCQgeMBQ7HoNqumRhpAph3sOs8r0qgs8SkJss8JxUEXdcVQUBz4HZkvK1eDKq2fTclryAKcog0
U5MYzB4I6OEOWdHUoHbJLFINR0jp+3u/YWEb0OKl7YBiQjKKCLVqqxHOCbiVwmGCEPLYLBDUEgKR
xYLrZr9pqF2chIj+ycDDXsspljcTPE5w76r4hTR2XW03+5/AUdTch8pBcO+4v8XiQllRVXCn9ZG4
kLQ/EkKOP37Qrjf+UW72+oMpiYQz2J3OYND5ptBRoQWrbUGS5aQmCcoobduTj8qbFvyJsbZb9iEd
l4YXjVqnXQ9AR9XHJeJlp0tTUBXshnmxMDqr4DhZnDIxxjYB3QgLAXa1a/lQnT8avS6m/k2DrcmS
jQhYi1E5xCGcl0VwecoOPmhUesStz/1B1uCTb9WWYx+CsK+1ml2y7Nhq/ANc1A8wAXYWHBCsdXr1
Rt0fwCTzJ52B6zHVQbIIjRpu6sU3eKz2xgFaT1cAVysmPCiNH8T7MYGIWUiqmi5yqigBtXkRBXR6
cbwwWhyvyQKn6byZT4CwnR81cOeTiq5w4PuAE6GrBaUg/VdH6q6QWhCTMMd7vWq9iVFatV03Y+yw
qNp4ieyNgPbJSyTm8L7k7klI7p5djNyV8VZ0X/9X5R8EOnBudxxtlWy2zX0HTcuMRwjY/6TUBcwh
bpdgzSI1fYT5QqbMHYNhVxh8bWPwZScpaA1K2kMtlyyaqvOcVp0+0FMz9rqgI0U+COrSjtBUJ/Y3
QIzR541dVskdj4Z3gZ56zFE8ShmyE5tUCBxBK6PFeMQyYCOp5QZjk8uACaHX/7+SXtHWmQwg7ywD
5X933jjCINVWyxqUQ2wmeK+BG7kbHbIRKFbDBpTDYj443FkE6qoR3nH/CzwKmLyvcDCYkpYdjGT8
mtwLbw2bwmDVTo2hbjzsvOGWrSRSN152UfCyoFcO/570Y8T8+7YVhRAGidggjbncGh/B+4MWVze8
CDI+iyUi6I6vmfDOgk6cd7r1b6xZaMdGqluP3bixymy/weKvbrdnggX3jjBm7+YE6nZmxAv3Z7M+
+LRcRDEI6pNKbgZx/Vtz8F3FMMTlIPDMJj++vzjQQ4165/2deyMRopnNCAQnNTRecOboXY0P+w1w
S3bwq6XptaBRkt3DXAsCr3iQg46pGTHHEArZc8in8UI4LD2+TAlkpdlugrqFEK/Z6qBWCeMibKZN
W0l/TzXPtAcDeWY9qKkOlf8KacwD5ps3AkVMYDif1Rv95ke76vdBmcr/DSvRIlokgJ33pjfpxrYm
fYPRY2t313T4R93qcahQwiFqnTbo7wF6tSFjQUjboX7DIjjLlWVC9+pcp4cRTdUlrkzAd3CcPju9
f7q9ZS9U1wz6wniB9PrBhTKfCfMHlWhgQ/UxU2q1FQn3R/gY+7Vuq/ZXsGIxYGrtfhgTA8yg2aLd
q4DxwTy1qt1oOphwIbgThddo4z6OMMOBUH3chhqLcwm4YWgcwYjzDrD8AEtOTUw4kW16EBRsFLrO
bl0Uos8jYGq9TjcCBP28JnhSEWCYgbLKGaI6RRfordrrh8yj2yI59iUG8IAaUhQsZWRimFEHjRjA
NhoxYCk0WFL03h5w9Va4yjNgur33TjtM3yFYf/hmyaPEmqM+DPSPRivEXeiD54IOa8hE97l246Pq
ZAEDgDB/Af5PP5xrEA7MTTu8rZaArVWtobFVG8D1P6sQBTVCqIRAjQHmWtuAmyc/6AF0Q6ksPf+P
LudK6Uo8q1OA6nldQZKRYkF+MJxGFpxpBZ2lY9Z8OnDGgng4JJi10C5x+bvqSioEAHa6tRCtQgD6
ITNOAOrDYIcGAPrDLmGvPz+bg4YlkHGzh562wp0SCEX70RaFQL0P27UQnjJgzDyOxVcRZoS8U223
rQweO2wnUFGRUO2bcq4yV9wFl7xpvCWLHQjP68nHzMXN6dnjYvIPxqY4TzPdHuUgsiYIYDCapBdq
WDDWOk3t+6+QLAIF2Bl8WiGtOymwbYFTaYH/9u0/dDpJcRLCZ81/NFpnjd67vQDzN+wTsoEvrvcQ
wqj79eBFnhmnJ7jnEh7stoEB/NlDeHL28e6eLPitdFlyzzT8VgbNTi/12w8A9VrTMQyS84RUBjHf
2f1+a9SN1KEfI8xCHzV6bSYKlU7N7bvYr91WWRsBGZkaXAfstNuYNP/3v0bP1ESIOA==
]]>
<![CDATA[
ZofPSuUXZ4KYjgXOOoIZOyzKvc73dm/wZ6f3VbGdF5lpVKwXjzvtTqnzZ9vYAE6O8th+61hmnFoi
cb8ca7lkHM1r4WVmtnHJmGS2HcIVQkZDTswoOk7GUdNaH2ebVuu9vV71L4cKvrUu9pvxlmdjzrOx
llTstOskPjyog6w335sWY482+efhDmYQtX4Nq46uEEWWb8MmmJdt5AiGq30Crg32PIW8amm3bYhj
3qoD40COcehzafkG4YMk9Ake5Ugze0BOFDkzbKTDzKISyc54QI1r12AUL/o3ELL8fqcPdKKbHjMR
c+KpeWM6udZbFxCDwAyA4j1HVRFn7NhRrKHT6uKSWh+KfmkPyQVm7vJz+P3WrjZb/dDxy/iOlSoN
bZ3MO+DS7UYAOrO8YwfIYdS31yiiQQmWlWbYSoxNPNDi4PThfkWTs8+qver3v//fAQgcSayaCxLJ
+kKjbYb+DeK21BeG7eR7s/YJmoo+kivZaDtLZWapfqnMJa8w9dNv/DNZM1q2e8GzqrA+/4/OEB70
/v2vP8Bc/NM4jaVOFCF+bneGfzSqw2SrYXdahxl39dwZuhurQ3T7z2Tzu9vp4Vkc3leHICkwUa1m
zT4l4xswxAFgLmQZxAiMd/JnuHDQLpHE6jJ28dYEAFc/bTwWAPyBZh/H163CmKrQWn/QNFKx0C04
C41kfWghwMVTINBrrdfsRqQNXfMe2wAYGhjUYjSXnDc+cLNNWBrHhcMOlaWPhr4My0zZBgAm5CA0
OWVBXvaa3xS2AUQg5L0YVNt18NXjYup4VmGtBmj9sw4w2l8hyYP4O8XYaQW/mR3Zr3HZWkqyMJwA
Ji1Wu0ZQ0Ww4xjdUjTMNfQDyYTvrQ1nDWKnEOXdChZgW+tzQaH+N7JyXHOkOX4JlvEBzwng+Ynj+
2CsJN40RnEKWhWeF9HaUYnD4QbsG3OIZXAzvmVmgMZpLtxOx5hnAjy6XNyCHGHurV3iM4SHsKMLI
EuZIl1mkXPy2ea4fPS+ryQxAGNFV0Q5QY8W+rB7B02j1Bxz8T+CcYlIWQRxInmv2qTQPpyrGUXa8
XJBEhbliTHcDMVLfKf7hCoJxep4s8YogMIWC7tr9dji0yFVbg1qrJ1khdVTjVaeMIqJpyd10BLRg
QsuxoHkfdOhkDHw5liCUKR80vFHRSjWbis46h/RnWK33movsxCU93Iilev8UxaOMBS3Gm1CJntBw
4oge4sSZexOLDDmqNSZpeC58gw0NGXu6BLdAxuPFeJwrjcKLkpttBE41SrNktaBJKnMTDv2yV7RD
p2uEEVvyJFgqRzAVVkEWAS1mfp/uahSVI7j7iuJQYQSVI7jZLuagR4OOxxSiZ5DBU1VzSkJZjgjd
ZHzr42ayCMkYXaxjTp3ombpQuaC5NXNYxeg1psIQI5a06LG6CMPKHtEoUWelnHSavbj4SBQ+hUiK
vvcaEGmHpnVcOPWqXdaRFkHwuG/IWaiLJqUbPoRvbWyovbhRo+W9o43S7572I+38SMThPYON4p3R
Whc8rYcLtzAqKYXRGEf0YB/O+uKo2IhebKz1yoP2VxLPp6MWKql1wovqH43jYWvQBLd/270B/D+V
/P+p5I+a3f9U8v+nkv//ukp+ZxsALj5gdq4PfO3fQoBrUsbq1MC3gek/BwH85yCA/xwE8J+DAP73
HATgTdQ6Z0S7jzVGp9M47hi3gVnPEiThTP+Cyd/ti+LBgaaUGrg8ga1mN5RXNbt5/Zbn89njXHbz
cyDhJ1Fe+7Ui2Q9+2Z/Ig1Vp83KwU3rX9772Z8/Xq6V3/m7Dfipm188Ln6lFaX89lcsvnCfSqezG
11pq8eReTy1/NuHR6zuXyg5XLlLLx7elVI4/Fvn8+l2GdK+kiou/5L7YPwbkSl/y5unrhrSjSVrh
vvB9v5Z7LXfUG4mvO0/5/ZdGMZHu9TbW37aXuyeHW0d6f0PbX7vhyp17+Xq393jPl+7Ld5fl9e31
mrC0rbb5/GnjKrtx9yTyh2fnRX7/VcmLr6n9U2F54fM6EJFEOgYqvd5marjzejw83t4v1E5X5tvN
pT1lcLwFOFxfbOUHfHnl6bTU0V8vctvw7uE3X5+/K9mddsm87LU29P2536RtQPlt156DeQK50V1c
65K3zZ6r5zvmp9fDTfIal+8rP/DpousDIRTra+X2pZjR7+YAAaGNfZ86M9h77H9onFTRhtmNvdS8
QwloVtuTblZn3wmaJvIGcpV+r7fav+89rZ6d8nn5IgNjQWydbuFd4VG+/awsMzt9+tjZD+y0IP7O
p1id4uyv9t96z/nsDenW1+nJzuLsVbdVYXXan30u7AR1ur/xS21fk04Tad9Y5cXb7Grt9JjZ6Uz5
WQ7slC/vHG2xOk2kodvC7Fy7t7jOJrB898yX308u2J3updbmhcOXS2ane/viJekUecxPYPF+4/KV
dOpiOWNWb3qPw40Kdrron9PMnfTQEhahU7njdAq9GLNa4S0Cny0seDpVlO+XblCnL72nz/ZlQKdb
1YJanhPIvNDdGp0+b76eB3W6PydlVh/Zna6lnvqzn41zT6fQi9Htr+Lixs/cd4XVaXa1tbIR0Glh
dvZneK+yO5XvHvjy0doZ9MIa60z5W0/LJ6VfrE75cqd5GNjp/PFpY8/TKfZidtvg937N3rMJfHLD
p7/y1xfQqdr1Cs3C3otkdnqXy3g6VX6+Ls5NPSbsPn6VXWO93+ArB7qEnS75Rrr/9aPKO5syq1O+
8v3e8HRKejG71Y53n9+COn3mT1unF+xOjxbujziu02N2enEsqSCVQWOt7MlHckCnDzJ/eXCxGNDp
cHBR2XtQnU4Taarba37QDOz0snGS/wzq9IC/fl7YYHda0RcS6etM6mSTOdab3PV8YKc325nV2aBO
m/z98vqz0ymMher25KDxO1VbyjA7fXqbOQ7s9GultXAY0OnjJnDy8/O2zB7raXamuwQyyez0VbrN
BHY6c/e8lHc6RStGK4hUr1c++8JOsz6hORW3sjPaWg06Xfnx6qSh0L42O/3SlzydJtI/L+p3j3Qr
Lmxk9t2W5iy70hnsYqfLfkm9zKdPm8fn0OlW3zvS3ZMub3Y62MzCvLhVYZqfezGERnwarBy6tdIv
fnf3qoydcp5Oe8PXdGqhkVHvoNPy0NMpav587sbodlM4ynk6nbk8vDwnnUqbV5UK3ak4aKfE4qCG
nfK+kV5Lj79vS2tL0OlhKpH2ErjX281aVvXs2/M0JeoH78FPpdpBjvXUtGLZjfVOK/BtUL3zvcCn
/O5afdl6euEzy5Wt/Qdbw+xd+xR85fzyJeRp/bUW/PQ41fpwnvooxh/Lc1zw26fDr9/BTy+udZ31
1KQYf/G5uxP89uV55zTwaW+wLFpGbe/OJ73XV+qPQ7FHr6Dx1x/FYfDTm7mzuZCnhceM89RPsZv9
z1Lw2/fKQzb46dNX5pT11KLYc0a+DX77+eO5EfgUzPvGRvBT+TpXDaGYsM69XwU/3dFlOfjpyYbU
CaGYcPqzshr49sp8t/MS+DQ1ny0q1tOXno9iqbnjjS/r+ZtX96VEvvQd+DS7JlZKIU9Xz8sOxYzn
XTo2lJeJk3geEJodt0NDs/31Swjtijv5w5tEujTbOLwobWYvLrVcan4In/bOIFRcKJZvH8t1sAYz
JfIiNDG7wAjMZ/PN9bdFYIGZXbAGm+cuvdmbERfWz3Imxfqz13dn1Fg3ZqUFEkga4c5K8eHOUdb5
Y629ANH57ZAEO0CM9zVWp2ANVgSP3Te7NX1Ufuk4oFMIdtTzxaeATu8eWZ0m0sZYZ8pdiTVWM9yZ
vb8K7HTh4I37sDrda9GdrqUWSae23Zcv5mgCnyki1Wl9fn7W6bS/oM47bCq5OlU+FzObDy1Pp+iN
mwR+osfq7nSmXOUCOyWxQ0CnhVmMHF4du+8eq3z3EtLp3lwhuFOMHDydEm/cZCX0SKpBnZ4Hd6qd
HF0Hd4r+iEvDQLdz+HzZ/pQzna2l9XwsOKnIs+BwLC5I/nVpZTtGi8RRc7QFJrdk4w2/4C74sj0b
+t5tUVzY5A+QMJI3FbexvLtM/Snmlop2qA86SZr7hb+dO9IERFVAXrI7nf6JgQV8KmH4v0t69qgm
6P7qDL7OY7w7XLI6MBxoswMKm7P5rgVysWXGYo7a4w+VdNr5s9HN1C9Nf5u04wguAAOiWz8GiCvf
SBDeyX82Smn8A36yTZ0lVqoORvBQEqpzC/s2AWnKb2zsps0/y8edQJQw3jeQKvdDkZoVlq+EZfzz
QOdrTLxOKZJvZnaPPCQ3KUYTnfyp3pacmJw1Pmlu9agSNT78g5NDMiSBM7gw48xg4PyhfN7QYZh/
fCSndPYdYwZjzB/f+N24ZvFnIh1ErLDG+l83IzG7oWFY7N4Rdp/6e5NwlsVXq1wiPR3KE9cokO6J
9GiUfy9yD6NrBrQvDOWz+7ix5FY9u17VY48+hupxInGk991yz0VAG2W36mmccfOGU+an3S5G4gce
bNxS+TJcAN1+vGzTjrlSAcDPu+LTcOeIrbYDpNLI5vkZ7S43M/nQNld+HZv2JYTUr4vzRIYCEFnu
2hIWPCoi+0fz5uwz2H33sZSbeECkl7suzem2GLo0zDz+OQ+cJv5dmLkLJEsiHZcwYVZ6J2Myzfpx
3hq4kRBic3JX3LnXD8dszCt11Zm9LJE6K6MIn8uTyB2NzZs49Myk7fNbc5lvzq4skz+mFiRrDQy2
qM68zERPJ/lj55ONNLaPO8o+LUg3tsU3Bld5H15v0mKA3a/OHIuBDJv/7GTX/V5YyJQYfqKtCA1/
bC/KC4uteup7wtLO77LHLJE8fzyfkZrfL20QbpY8VLTXkvzzC8g/D6fiPe1hL25N7SfWEm14g1Fq
zAShBJrfxicOUiyXzkLp9NyWWe/82d6FawajXLrY86dT9iXWDIYR6zoXzgyJkRrjRuIspyn3OrLZ
WH7MxhhN8dOkmDBNionTpJg0CcVMs2wy2rKp+V2B68c+X1+o7k7sHYs7t3VKbxh6LDiUYMvBYDMV
270OksqPfbeNH18qB5tzUTzmC5TJai6TOoN0eJiViEGd+ZGow6INjKVRfbmKGSwwHUMYy0uEHCfi
oDJKiMdEJJFGVCJENw4iHt/SjYjtW0bRJEJSvZFhdWaw5xgoyuvbJ6nrUWLyrCfFTZm8zUypBwL+
UKQ9JfGp/zEYpYOgpMbvA1ZobfswLPURJCBP/Z9AG89EydSWLKSmpADAU0jHivfjKICnQWZ+tHg/
mOjS5vXlcXyNbaHkty9P/c8ISfZybYAnf0AWBC3fclKm4t8Xfm7DNUPCHfgExOTA/YMR04qu+aOj
JCSWPDVi0QIeZSt9xPKIuHDYd0ScYCPN6d2hJ66iNMwoeb3vQ7eIB2RIrEyClVNyM5o0t5KZCw0a
4wYVh8R/j5EhiZGS/T50++/eoSW8gwsYmpyZJL1BsqPfh16zPHreB/hg6A4pqQEl0g==
]]>
<![CDATA[
rNliD0j/kQLD6PC8D8Vjh2RpeMK8D5DlfSVzH5rr8+ZAXBG9mzoh+Rq/KsBeXLkGtzOd968BdY/c
rnREB8SVDpCXzavs7IS06x45ZtCYFz8+cQ3hyq+FGByRiGMIYWgrk8tL98htAyO0UgAiaSFwVIl0
OKfbKB85lm/0ATmcDLzjMXpjKICVXym3tZOC/LEowhRiTLfHl6X8MTd13L4smzqxfFlcqjJ2257T
0w2/ji53rIGjCs56Ir4xct5YmyCHaz7D2hmZq3B7h42txCCgkW9luR2UTsbG1gcT6pXbC7JIEa2T
w3PxOGsjmzxbW3racQeSYyyZYCu2/Fle37jthK1UOK0k0lHt+C3f6HbPXOH1rhCO1Jg7LY7LvBmP
v4lZhd8NLlxpxE2hYVM8qykzeh0p7sLGlkIWfQLW+AKcCNwJGouUtPvJ1GiWVKLx8Gs0+G0qGg3n
pf818Spe0belwqU3zMxVTA8eG6t4g5MYGo1pX7Cxs9SkGu3K0WiTyD7MWkyNFi772M7kGg13Dk/u
UxBsprH2StpxazTX0ssvZxWH5QvQe+CNKQtLkrmWDtkZty4tKq+LWVZu/PZ6Wguwe3ddJ4wO8sYj
PTOcTqZmZCnZRDpCzUJjwculcZWspZOhsXGDRkqYdx8fmWGPsfYaV5yvfZua4ikFL49dT+Lau1qh
N0AYHux47cQPqAOzo6SdkK1HUS65qyniXUwtV43j89tC3J0+Jf8e9Fh+8oivCIrkNtyABdtC1z5Y
s7H4+ylC04rY1NusOwc7DqPdsPz70a0YzOXEKS1z9qdgDQGbUFsY14phO/H8e1YrdiRO2hnfGnon
LDyfPLo1zPmTW7e3HltIr4qOag1feiFJZXrr1DK1czhw/LeYqNsPmBKalI5ABq++FaHbt3CPMran
C019zsbR/HGkGxr7Cs+h+/Zah1AsjoiHBZcOJ7/0Ysl52OopigLHSl07u6Eit9O52StMSH3CZcxL
qGF66/sN01t/JLOEtjLQMBW54FRknJ1r7nj/rc9KA7LEK5pV7qa42xYa8+y+Cg2e6cp6dmPCUWU6
GZK3fqx8suNi+Hch2jOZZ22+DVoTD3AxcD9BsKfv4ggaJfZqAkEqJkeE7VU1hcLwkysqO7Jw1cup
7w/vqnWIyk5lt/e8/uLU0IVX0KEem0YNXXgFHTm7Ywo1dKxOnQo6O9szYQ1deAWdVZE6aQ2dbV+Y
FXROhmSyGrrwCjqnWnCyGrrwCrqAasGRa+iyoRV0TrXgZDV07jn11rFZJ7dMWkMXXkFHVdhNVEPH
cDCLoeuVY9XQhVfQEZ8/dENycCXQejc66HXvgQ+uBLrL7QXEAfFRIvJSDA/rZ10KPrg8sB+4y8Xe
1xezVsCb6Q2jU0Smt+S19mNP3cVMxD6luHTquA09Y5/ZcScRsxjsoj0andxNUfFLyZe0Gn98ns19
7voXa4TxxvcYXiZKoRRe+TjfidzcFwulOJmrEDrFLJkL3acUk2F3Hw8CS2ToncMRBVRRa2CRW0Fs
D/Yul5o4bWwN7c6b+mLuUosY2uhbQXw7IbHYLTuFwkSX6I2Z6cVitxGWbYLqXu+WuyE+f7wFBySL
t84iViAS1FhElJtIhzfm3oK15HciquWomDymTi6zwt6Rgl4nRq6WRyoyDSkxfRN/PHLs1smjxfZA
rJC1bDpNQu9UCUscyv78/ZfWC3QnRlyxglHdBi/5xa0Cs+v4otyu+HV8jB3G7ng/fh1YRP0LMm7G
QSlwlae+597r6DKTo5UW6rMhe+CdyYtXG+XOYDL2wMcuLvRmMGPOH7uOL6omZgRmIKcguOz+RI2F
lcgYe+DjNxaxq340ioXWzIyI10rmfmoUCz0KIZpinsTvYOPHs9VJ3Ll9jnAbMXMVw8EebAzjCntQ
3jKyXi68CWwg4iQRtJVntwL5EyHdO7c/wdIdvtThXRXdjx/ssV2xfZZ68Gato5qIPBrFCRAo78lV
MxJdKhc5Qxv90Dpxd8zDFgsscYuSfSYxPFVpsYO40Wrk6H19bgMX5LnggMKPPPEEV57cuNuPZKx2
/j6Iqop1h5mBnHwwYnonXnkcs2LIHa4GVkTtzk7NH3sapCOKWmMsbhr+2MGI6Z3gMrvsAgslagdR
TDqVBjHSOx4WYGauDkbNyIQVs2FGxhVXxuRLP0pRwuyxYiFIjZaRCdyd7i2LG41O7oyMNKd/5b1n
dxxG7eaLl5GR5lZmmDt2Rtql9n04ZkbGvwceJGd+OhkZGJqwMPEOou/DuBkZI7IILEOL2OsYnZE5
NPfBTqEMLTIjk4hVnzdpRiaRRsIoo5fnBFCHXZzj5eR4peYrZwNvHermVTp4L4194kG0swze3OyY
zEBpmKOJkzoWcPfIk9Jh5MZjJnVgaJm4Q0NODipDi7lpL7x8jNp3MUldXZytwInourqJzw3rHuEe
+PH36zmECVfWdnVtZBIUqaOOKb2Gb+nZqpdhrKReTGLoXCeD2RVx066H8+b5Y++pG6keLuL8sSnV
w6HsTyp80fVwcXeoTlYP5+zroyviJhoVQ/7GqhYcuR4uaGVkuvVwRu2btyJu2vVwnhzs2B5eeD2c
+5QAynZNtR7OnbX2brUcrx7Ov+obWC+2NempBFh8ZPkRQfVi8fdEXsXYE5nwkDBwT+RVrD2RkbJ/
3Zm4vB6VUDbmTsjIdgKPtYi/wmu0M8pRJsHY2E78+JVc2E5I3OzakpmIFkMsrgtOiEWXE4AQuk9o
B9/LL4bw28hiyMz2FGPsaohVERXgztsnTscXw+uRtiYTIQyrsZpADB1qEyGczBtHG77MEkNPK1Gn
AZN2RhdDX/RqtDOxGJJWgmLp+GfdkHZiVYf7HXu/hiGNBS+7Rm4jd2elF8iRwN5bALDIqxJxuESs
1ae9x5+pVKQKM8F7OkauSBVmYhWRxqtIFWbkiUMXoHaDWXQzWkXqzZQqUm+mUpF6M6WK1JspVaTe
xD8GOiqlVUyk/cdAuzYsRO9Y8oih5xhosxf49SrcgMUUw5BSOLIbarRqnTFK4QjF2MScYikcodhn
jDOtJiqFi5m3nLAULjCunGopXJDdn24pHH16drwa7XFK4RJx9+UWPccIh6gC/4nwDItc5CY7Ed49
SKpacNxdtFRjoXsCXT5MxK5ArF4LPchwFB+myI2bnvTP5AsX6zStsK0LWH8YYvIojkjERSomR7CN
g5WBd+QXb41jsrM5B+SCzP5HKtf+9ZJavn7eTeW2pedU7lDfxWvWi/jpLrX8+fsS/2ylsjXuMJFO
LZfOi/gHL+TU5+wJnfegbH5y1Z31+kK6R8usq0JJnhFXdHqHqqsEbGY+rNiNy9H84uo0uyZ+/GJ1
at6OjddqPwQVu92HFbv9Dquwez+5cK3yuEvA8FrtWlCn9bBarJ0LqlO7Fsu+j++z4ShFbwkYXjVt
j9Rb7HYX2CmQdz2swo4v6/xJQKeF2bnzb/E5qNgtosKuL7PGaha7Lb9eB3aKd8l+BtUScqEVduXK
QmCnvf7VRiqw09TWU+7SNacN3czzk8/ORCwW7+vfHkgm3PPwux0JR277fd69PY2EVD5NvjNNJxYd
PW57HFErS5P59phTHEt5GHxLUowtt24PlrFC9FDynqkybh0NRmDlgLQTvWYR69KvqHu6AlDy7rkq
eZ3gsUvFylGnNE90kxwru5SYxk1yMbNwpeg91DHptLrECriC9/WNcYlcUBZuKTCujL5ELv74clHn
wMceX+RdA/GRir2z1IOSJ6sQfX9cfJSoXBD7ZknmdteY1XQRmd4pVdPFyMNMoZqOVUvn3gM/jWo6
1tAS6WlX0/kRKWXjrVeOUk03duXjxMvY5OSWqVbTsciCY5luNV3UCSHTqaaLY5Enr6ZzUHLi5tCs
9VjVdKw8i7EPdprVdKxaOtbensmq6ViOoas2YSrVdKxaOua5ChNV07FUq6NhplVNx0KJ2JepVtOF
eEpTrKZjOackDzPVajrW/EXfMDVqNR2rqdFXeKOq6VhNhdRXjllNF0CxKVfTTY1ikY5hOMWmUU3H
WkZhnAM/YTUdq5aOcUfqhNV0rFo69pldk1TTuWXbqKWLqK8co5qO1UDw/uRxq+lcFHnJe/LJ06qm
Y7k0gbI/djWdixjmwmmcU2jGvXHOIQbjhMMJq+nYuzsQKWUMMXQHgOJT/41zB4AHTgBoS+W4hXTt
VAw2TERu28/sRgo77V0wszlEJ0/1vrqoPMx07qtj1WIFrIoCUgsT08moyES3IqYei2CBzxj3vcZE
KrYq8KPkvV0utjhHoeTyAKJPOQuhU2xhDj+rE5GqyI8jq0x3PLQ+8N/+g0VVUfuP4mTm6Gvuxt4N
NdI1dyYnB7nkh6PvRwzUMFEX3U18zR11f2VUId0EZ4JbO4dDL7qb+Jo7v7aMqjAc55o7T0aRfdGd
jzCjXnMXysmxtj/FueZu3HPhjry18eOccwWeaUSqMW5ALW1eqQtxakVjON1H4RuA49XywNAWJ8mi
Gqs8R2PuPfQU0gUWFdlxZcwL6sbb+0vbSqyhi1MBG1lf6Nt0GHFHapADjZf3jVBP5L9hyu3/oo5c
8NUTVV8imMFj6IL3W16MJHeBNVRT3A0FjU1vN9TZ95jWzlv5GLGxOV7l46K3uNeXVYjZztJI2LCr
n3hy09E0RrUca2dXdDtx7iaLtbMLG4souAvdudZ174V7XVz0W77byymeCgiNTcXDM/FyKbN4N00E
krI+LwbfkxN032toKYP/MGasxFsJX97zRuKBe6ivOxNXlBi3zESMOn7FZv+LqTzGu8Gw/xXrnq4I
2XdOPp6gdODKcSYmumPoKm4hQ/hqNWln4lMCbklWYfLbqgk2wVdrbSGPjVDKgPsp+MD4e4wV3gXG
zgqsxCuGEzBuBt51x90EhV3UmNk7ImKLYcwb7mLdWz3xDXdO5SP7jrsRKx8DfPrRb8obp56IdVPe
5GLoveFukpvy4t9wF54bJ41N4YY7575X9h13ExfWOtVP5zGOx4gs7Apzc0Y6dxSvkxvLzWGdO4qN
TV5Y+/jj7HGaqPIxF6OwNuqcK9LOxNks0grM/uT6F7EJ3eiUiN1O3Pp2VkrLnVMi1+VNWN9OL0Rj
WRQKoacX+HUqYgijehgE67GIMiYfKVcycTZ6WWenR1eETbJ50UexaR1tDk05Yfs4eUs3xQrTiith
Lq/jBKmBRUwkP0ZuT4xVxhQTJS9H0FmFMWpcd27vch7H0Lc1g3VqU7wa17d+3Ose41jku4mve6T9
MRjmV3hYFP+6R++ejaCMYqwa153bQYxcdCwf5m7i6x7tfbBY6jl5jSveRxdk8rxVz9E1roDSKNc9
ElIx9yk5Ljtur630Gf2Zrh+WKaWWjlYFUqKHZX0XqeWX+mVq6XK7gJ/OSG1fIp3KHb0ofP72SzVN
z3rni0bPyi65a6cywfVw2lmep+n50pshO1Tte9jmOl3a1LnuYcu8zZ1/BV1zF3rj3A==
]]>
<![CDATA[
c86dH/OU4e0UTgM6LczOtaXVl6AivGdPp4ZOtu9hSynBne7t9e7sTr1FeLM/heFjUGnaUyIdUvv3
a4u+R9BdmpZdbV0FFeEpn0tbN0tdp1MYi2uswbV/QOAPPrBTvvy0H1RuiFVp6a/89VtQ7V81pNM9
fiWw017/43DW6dS4940uw3ucLVwFEXg5bKQH8545RdHMke6NavScVYQ5rAdC0nCns404cDOn6yl3
nj8Asjd8+UpTZhLH7HM6LcGFd5czHtNJwqfAu59OzxknOoRdQnA2/+1ZDXJyp5PfYtYN3+LByJAE
1/9sxb7li4WSfTLY2XzkLvd41VasCGS8m1nO5iO2l3rSuTj7QYU6S9tncbagRU7dwszUqtJCd2yP
VpWWHYlOTlP+O7mgseUpjc/epRVz92DI+LgYKFF3cIchFXwBfCyUzNWE8DzxiHTy79JyVqxOr9g3
TXjU1d1y26uuonPMMe9MuVsOLoyOnYPdnVo10vMuK/xlnHAYIwC+y82MNDTmKs/uFE6ivVvuOnmt
sfNjWJ8WJ26OONd6dxqZZawBhAAh9DbGeISJXS8WGbVgY66iotEO+bEzinbVLJ4W5/ZDyhPfd2Bp
mOrMbeChPCPFyGVWMph1GnCMVW8suAveM+dLBFhnQQdkVcqBh+HHTdnZUmlOY9a/gaC+F3nqQix/
BMfypQXf0ztqIdnDgOWP0HemxC8FjDp6YYQaq5EuFglBabB5GLhvPNobd6Pk0vfeQsDECB7llz43
Zimnz1MC5NvhF/GMMH++9f2JGou413iWOn8surGoW3QCm/LWI+/5rMpEg4yu5RmhsYiVy9EoFnWf
zkgUazC1BLNcONg7dNUAmvZlzCrAuDWA7HNIApoY+0Y92+sbqwowbg3guPnk0W7UY/qWsasA49YA
RtxiFlEFGHeGmLWisasAAwyBrwYwtMomsgowmu0DTjUfqQowbg1gzBg5YPUtvAbQxMbe13fu8Z9s
SkzpUr6gG9mmeylf3CzcZJfyJdJxvLlJL+Vz3cj2t13KF76SOK1L+cgZd4E34E3rUj7vvou/51I+
1m1Z07+Uj3F/5QSX8nlQ8pzc4vaeDXwiSoM99/pZFVhTORsq8F6/ESu5pnQ2lPtWv8nOhnLu9Ztk
t238e/1Cq+5i3mUTfa/fxGdDxbrXL/JsqKnc6xd+q1+CmulJ7vUL37Jo77ib8F6/cIfdtYNognv9
7P6Yt/p573oe916/8P1MpP5lCvf6hd/qN2He0r7XL3xUUTeAxL3XL3xApJcp3OsXfqtf7PrKiHv9
wneceWsSJzk4O/hWP6piaKJ7/eiKEv+tfmNWpfnu9QvPLwSfQDXavX6hflSRzP4U7vULX0sZ5T6+
yWveJ73Xj2qFYfLGu49v1Hs1WTUj49zrF4IShLDR2jLevX7ht/qFVD7GrxL73Yi44TgxQpVY2L1+
4bf6seZlnHv9wjZc4y3M/rqHce71Y0m8s/Vk0qq0eAvD1Pr+RPf6hS90UZp/onv9HGqz/Pdx7uOL
W/cQkrka814/ZitTuMeq4brXL7yVsGqOxgj3+sXYbTuFe/1cYui71c/0x6YkhkGnK49clTbW/gxm
xdAY9/oF4+U7SW8cMTTv9ZvMG497r19k1fNU7vULv9VvxPv4xoylXR6s/16/0a7i8zblOVFn8nv9
vFW47lv9mJWPY9zrN74eG+Vev3A3xzjddPJ7/Wy8mLf6jXZqU/C9fqPVvY57r1/4rX6T3McXP7QO
v49v8mJ441a/ROBaxGg1T+G3+sU6Oz3GvX7ht/qxMvDj3OsXfqsf04qNca9f+K1+Eedcxa95Cr3V
jzoXbqJ7/WLmLSe81y9wJv0nT45R82Td6zeV3YOR9/qFO4aox6Zxr1+4Y0it8U10r5+PlK5b/Xwr
I2Pe6xe+YuOprh37Xr/w/cCe6tqx7/VjUEwNodiY9/qFW/NEcEnsxij3+oWj5FRxTnavn9c4uI8g
tnp56n8EphW3DMGNOsR0kfdvbLh9IInd4Iqh8I337rLFsielVaRzWK/plueed3Ta7D3EhmI2ibBI
EWZDOes49PREolj7tq/lUvPD3ZudmxT8dtF1aqwaxV5vXdzZuHq6y6TSbVVOLazw5dRS5+JXSly5
OM6utlZ2shvrva3s1dHnAr970pX4sr67xZd3jnb5veXhOV9Rdx74ysN9jT9e6nP8xeqCwl+8bKJv
efX7rc5fL7Q/+euK8MNfdw/n+JvNtxL/dPp1xD8NuFv+5SDX5l+XztP869rzYq93klvo9befCr1+
Z/6gN1wZPPRnuzvvnFTRhmZl50fnbKOwkDq+2kmLaiKdqS40zmav7y835tq9fHlelF9OFl4vVrSZ
y8NaLntZPlvY+LXWKGTtUsCF/cbjbk6tzP+GKcmWsewtl+o1n/Lp0+bxOXH3mZleur50sdnSU9mW
/Mt1BSTeJykv3mXX1nIrTGIRYsBw5/nX48wvz0gTac9Ys6s1Gd7mNzf48uVNmd+b7Zz1+tpNnVSS
2sWhl9n1fI7cRTlj1CTu7v7O9/qPnVX8bdZ3srEhJY53tbHepXxnw50w860VnV6TcfuJxmw87aXx
0sx6avn4dj81V9LOUtlaDrRlKvtrZjWVyy8c4qeTlF7dXcALNE8R6B7v07w1rtyEF7cQUUe/zht+
TWOwpZFZ2/7uVPrbRzc3z9nScnpYzuwfHEAk+v2YSJdfFh+OQLrvFPQ+5lDXQOj9OpszwtAN5bGP
X/OmOlb2F+xPGbzLr4VZIbxeZ3/JqP8Fy72MX5fNr0WOI7K/z9kv5rO717f7iM+jtHnd3Sk2q3mB
z2/IGRvRJ76eyaxYD1aWnAfC7vPKmvVga9l5QPKWlQ3rUZlzHoHZet6yHlR45wHd/d7KIo50ke55
byvr0I70nEhbj8o55xHxreG3St6wEfm9Ux7PhctKc/ogBV+vRGx7CTTMQDcbOCtmEWQZ/qht+HqQ
s7TK0DrfEn6tcASIXGgDX8951N4C/Knj11ujWWnzss0Z87c4xy2S8JDP3x2QmYReisKq2endKUd6
kXY0SUukVxvPi+/Fz0L5dKelzWoUc9qFmUZj7jjWE39Cs+d5p1lPoy7ZH7HZK95ptnC1vlLcvppf
fS1+qkfd7cvt9g2RMHHnYenZ4uTF2m1za7WS6gGjXUo2o73SM/1WcdimCuLKfcNv5xwSaxlLexaN
T9WZ6xz5BMS/WCKf8BaAe2kfFcAdMNXaAfkEk/w9gCY+FCI5xBLx+a8rDrMhAsyftkAeQNvbGeNT
da64bmLzVRVtbN6g+atNm8e+PuTyrniMQnyv2GN5kzavyhgvvcKDwn2ulK+uza98tBeuymu78m/H
0JvGeO/2l5m3M/6Y6UAnsqis0Xw5eMgjjsh320vGp93Hw6zxicJ78CGR38Sdu+yuB5vC/fd+q/Se
7l8m0ltrm7fy9tEtD4pUeVJAr/zKEF6V5pvp+d3a148ebtQdN4DPV3802yk5cbJVhMfIZcSDeTQt
G3gj8SNRpKnsfWYLVeYjnlpwiH82Da26/NM9NUDI6Qbw2zU+LaWWfmZ7/mMN8vNkVXQ2Y+mx47Yp
7KeNJUP4bD4hmhHPmMeia4UnTUibN7tVwqQYcnGmBkV5AA267GhQI6eUF0u5hyyfV9aXLRbYzxFP
CX4rcug43Zoqeu9o0QzHlXKenfhVDngPH9h3cYLWxRNSOI/CJSMFjVd/ICgLy5Us7lo9yhEcheWP
9XzpcK3DezQt7mFr7bRm2mUhN3fwCbNvyuLJIpkow5Hbq8xw5vhAw+JMHyMbqsBoWx2iWlHL8UDP
8x9DqypvR+iPnRikFPYLlU+7ZfRgya9vz+mcx4V0h33zLq/vZRDu9RV3OF4Er+/uZHu5y0NksV37
dVIubWaVw+3lztZi+XJTvdveL7ye7Lwe3xT1Xa22vNt7Xnleva+0N/Za17eP2/vKA7+V73c/ieNI
VdYDeRdw6rLEQJsnDJRfssRWXnQptTfbLRZ3vhbajyVOXeivNvTe1/bFMPWp/uyfV3ar1QVu974+
80ncCcrNS3eeip7QxOmU9EJ36+t0pXK+tbLbaO58ZTK/dvfPmsLWz3Z+u3Tw3eyXSy1hx/LWSk2g
8fkA7wE/MVyojeF8ypdRDBywp+fVo7nSY2lvb/1r+7Ik/cQYrnlvNRkwtph3QilHh5CFFOukhjxK
6hlHhE9c2JgpWdprtr+bbd5/bl9e3/Q8PSfS4aTGnkVQhcLBWD3fiCWOW7tBKzZ4ErZWD7/ORyP6
5urGfOB0/108tvTR921BN7WluGCd3GIerXHcRlWYM2SRX5zTeL5fau+cnm09lUuK8rp9ufo7Uzp4
KBxCz5kZsBplzpbFH2LKiFRuXL0s7Trz7DnZeER6x6U2yVoTeg8WOHl/+xs01YUcOPQxBw4aJt7Q
J2K0RHqkofsH/qhT4f+Gcv3jJFAdNWqu77MUqUuNXvGlYfXzhqjRrffL7upu7+ntVGm9Pc/Bg7PT
rXxvMLfzeiJelPVZZaOsz53Xi0+Hs/urw48N8Md2OLl3DY7/0t4Uhd3D8eREHa+wT6Bm5uZAtf48
rkjF0sv2ZfH5kcwA2MpYwo5nz4yv24DHogc8sW5D2Y8cMHu4wGi5dk5r8fV0u9Trba78Chyzc57S
FCYZlFl3jiVr6PNPqNZjyFoiPbFaj2HD4/IYbcVH7zmR/luclmgrNoHTEkRoY69CJKlHGC6L0Xyr
PJNMcqBcJdJ+yZqMx1jeGrFi4+gVEkvTyTZGumy5dC5ipHaC+TEM7LItuYzx2yF+XcCs2BMmyU7M
7JmWO00tdK/mzGBv4ws+ieULzLhtUGm3xV5vObWcel3AsO/aiRese6waZ+sQq6zfmQoHE9F2gLgq
bV4OtorN8nxv63rh9mers9+7K78s789un36sVYAw8lzp/Vf/nOSL+6mnhZI5A+v3s8Q/SKSl7V6q
5B71fNyed6uvu19b7Z/8K3R/fhfoR4EVc7sT+c90Z3m8Tn+V3ue7s6jP36D72kt8HwY6bffcTsQY
3hPY/fEdx9imjJxzFct2x/OedhZY1MaT88end9wxT2LFRvGUAs3o+N37SA6x2FT8h/CecfZHihOY
PUfp1+lF4uJgng7NSA7LovuYUdJoftu8y09GBKZoVUIi8dTSc6trC1rGR3SSBqr+5L0Kh1pzEgeF
1OLJvY6mYwv/7AAng6E4MX5YWphdQwtSQdNTQTNyhA84NDcX+LWcWlw7WcHlGP7vsS/jKgCibrGG
928IV2PYF6LqJ+n5urF1fbR+APJ3mdp9LZx+YoYkpmn9L7Yvo1s2UsEdNeDA4aKGOYuRjCHVHNOa
ZFOpX8+VPHkBwmPjG3Wx9rK0tfr4+VLizl97xff19htr4OS0RrYTNYEL5RUujJFHm/NxWBzGMkEa
LG7Pztm2scRrTOEyM/BTZjSmHpvEcYw1XJPH4orXmGNOpEcSrzEHbvFYTPGKI1y4QA==
]]>
<![CDATA[
J+7cflLJATPXR2+K2fxQV57OjvXt/UJhC/6s7ey8nsyekK/6rjYU95ShcLF7s3NR2coPNo+295Ur
rnRfvr6Ar3x5Zb5TWinN1gu8k/oDze9O/o2f+gvx6nBeppttZzl0ifS08xSxMiSjL65QvB+kZP/e
GNnyotGDnW6egjVway1p+kEMHUPhvouxUpGT5GBHXPEI8afHyY+NkZmjex47PzYSx2P0Gh5K/J05
2LD4jc6PfelLY+bHFnqp3KF+a4QkEJyoI8UqLCknFtkr59vll6/WUnm7Vf0dQ8TJJ7KPsDd8raj2
Pg/O4XOy7yKuoC1kis3Uw2Jc3ebs+kukc4u94sq4M715vvS4fXn1+znmSiLh9PJLCj6tLo+/rMMe
bshqtTPg3NL8weokw0U/OXLA/uEuvo00XI8eG3t+w2c3Mg8Tc37DZ9c5fe7vZGfTik08v+HDda9Y
jT+/4cNNpKczv5ErVlOZ39HzyeOzMzW7ZoZLpCqGuln3TnxA6qxIbQ2ksc226aCCHKxCnbyNi9zm
a1ln/5S9Q9VXgmrt9MS9wdRGPmOvfP6349fwjRkl73RFfkvLJ6VfVvDRy7rzlqSJtc0LqomDx2XO
3cSn6S6ZbvOV6w4eYmf7s5Sdnb8XD11VA8YG8LVTp4lf/iaGrib25/fpPYryhXGVDNlNnN1YPhHx
bloSiS/vZ/EzZ/+at3/j4dMFWNJBpkf2RPJ8hrv3WF/jIp70WurVvMvldV0kfrl9AdIjuSVT3oNH
Auea5My3xbqLT8hFKWOH/Nrq97ktuHfGfnf/ZUDWxl0yLzuLR6a2JHPwxM38vrIMOIebBM86BJ/F
zOZDi2IlckEvoZiknn6Zu+/FoeDwdHa1dnqM+ylnCDbum4yyx0sUER560ptFhBXBIcJi8b7+bJGA
y7lIIP/YJHh2SABjWRM/ftlEuKeJAPjQRCAH/FpEYJOgunbikEB6aAkaHSMbtTcG5UmnZgnCUyAR
3CTgHN6/TXXyuwYJejt3D2ZG0eGEAD7YGlqMPUw5REjJ/Yd5mwS3IXywd/bt+DDkXi0mK4U2cdGO
0QCZ/cAmrjsT4nBn+PnEio0nEcZtt7FwMC2yvwlyV+ckwyCVjaZYGxQbeRiNwUg4wFh8TXxOylSt
lKcBKxKP3cTZdZsl3eGy7a4XO7vrjN6Eq4HH7qQa5uyFqaRicIR9C/PZWy+6ifswUjb6gdOJsm80
sTRHNbFZ/Om4mvgcjak8OBBP6Ws4mWycdVLhdDBkP9To9WasJu6+nSb4/eO7mstnerQ5547ClVxu
5+axuxcmi7gZJGxUd29MrYM8Fpcwd40ABolkUpvH7j6DWSQeDl/BDOLwWHgT7eEk4oo8dtfz6p1R
hzGcCcfB4LEwib+fnY3CQew/Og2kFq4/L+gG3t66lEUeS3G9NX5i4EBbZD8Wn+MyldXAV5+yyGNJ
/Ft7EDmdptqyLLJXcb39jKl1MODCgh50Ed9XMrrFYwSBzMOSjFm4W2MXwfLx7anh15GqHrsmE68o
y5tRxPqd7F7lyZIaI7qYr/zyQopgiG951rHqhC66wvLHx0aWbM02SgG/ZozyQKNSDSKLPPmKhUgZ
89PvBqniXDTLNhd+MEbez5pfVzI5o4ozZ/4AiBovvl+tDIyABauMqAJOqqRsQ12kCjipEWysZ6kH
WFxm175tFHNUASeWxVkPDvJ0vdHqx7b14FRwKjLNIHxvfYkq4LR7RnnZKy5Tj6jCtr0DDui9vCTu
3D6SsrdF8Np/A1vsnQtGUefmVQq+nm05bb+Qww7gtzKpuVyCYKCxY/r8mAXAIKCigUt+ClJydpo3
ijrxDgz4eiUYVZxGGeHZg5Q/vviS4N1LIP/s2iyp4jTrFO8qDllenV4iSgGtI1eNEjC7Nox1opdY
0QHNdtHTaCI9cbOuvMfiofZL1/bKWwuNy9JB3b69FEZ4K1icfCk6siEutl5mTUa7q8pUASfFaG+n
RsWmWVP7dpU3BeDtlhfeKgeL8OlBsE6ezL89ixv6gQjz9laVrE91mTRhTvLXec4o6sRDNuDrrVXh
+/XAW5+eBaqA065BxrF81SXq0XNKejGqVF+Pf9LmWL6+C4Gls6x0ijEg+499e6lTNTu4dQryaibb
DJ55YU/YysCnqmB9qjuFpzWz1m7wW/ZhowyuE+ny0uLGqnqdmzkuvx6nScXmjjT/0lf5w72sAnP1
VDALVI1Cz+O2Oxe2YGovsxZ20SqiPOuYVLz9yhon6syRG3MMndWcOZu3dVbfUjOccae7KXKKjCk2
ZdEsHlRWssL+3G9Uf/vLTqE5vHGNp1Psc8Z5F1t4KDlH2FTYe+bwkNb9fMBxvPs8OSHDPhZq3npw
ZOh7YZlvv1rliEdWFaewXEx3TZQ3tohayJhUBhVmVTQecVRJ/nK3yFtVlR5ldrhpzi5oNGt8J1nz
TBWzqvKZZF9OcnghQU/Y667k8Sv8Ua/3i69f2w2zbBz0mNO2o8yso4v6/2cjoaqqkNRkTUvmz4et
Ru+01/xotpPLidVEfvtAEK7a9U6512hcNv4xKHVqw+9Ge5BcSea3L4oHB5pSatQ69UZy2dBNqq0w
cuYgTLamz3xxpQ/JOtJO6V3f+9qfPV+vlt75uw3fERLS/jqudZ3jWtfG15qxg2/5swmPXt+5VHa4
coGmtpTK8cciWlTmeaZU0vu+8H2/lnstd9Qbia97NjWgX7Kx/ra93D053DrS+xva/toNV+7cy9e7
vcd7vnRfvrssr2+v10ztc9q4AgfxSeQPz87xCGglL76m9k+F5YXP68AyVaNa3l2oamaqAwtVNwrp
C2pzRFZXumfb+9LnL6Og6mbn+HDr/ery5OvX7M3C9n6hBn58Vi/o94By47Y0Wx/uFp8OXpvEY/Ck
sIXsl4p3X989Wwx+3HasnlNfD7FSizNrn42DI+56ibSpfQcZzFu9DExRBwG2PgkZNLUZk2KKSuqO
8RTBgy6pfSZfQXYfeqTs2XqtnLeLovHGBUqCFj5fbElcpB/og6r9IEs/qGRr9oMc/eBZbdgP8u5e
usUP+5FAPdjb+UEv6mSJ/u0q82bXKi/TDz7kuv2AIxoetMb+3BZv6Mr9XBmdgBOBJF+F/c1z/PqL
bvvtI4uU/WUctiHU5tQV01wsH3cMrVDLrWN69FfeaKW2eUB2Niu/BPOdX1ekWYlyNfZfeqYqXszJ
qFMuc7Qh3txatYX0fKfFfSxtn9XeK6Wjg9SFw5pk36FxfXjRrVM9F3HsiIv75bUYLbLaSwS0+Kuy
7igSZXA219h7utc+ti+Gc83d+/oZ2oJLweFf+oiQu2fJ9kBkMnCwf2TopU3VZpYbwxUWS7+KqGdv
8hbj30Dbb0+L+EmwzNwNObGgg58k+5NsNLC7+o2H69znzF104kuNTPy9fejKPW9/orhNfBWf7bMu
7iX6QelrznIvfiv2ERIF956w1kV6d1lfBMHmr+doZWesFYBCss4XsP6YJ3uZh8CBzaeMlzS/eIpE
fYI/dzcZwmNPAvmMn0Qa8vhDxt9kegOoic2v8uv1XbGU1RbL5d3ja83yab4VvvG2UiAnTkhza2uv
6Ejd26d7m9sj/KfymMdI7VinVNDX27s2rKkLdNk+KE9SqwpqchPi3q38YO0Q6/g3iTYllakEqLSZ
vbiE336uAWSptPEz912x/Fx7+dGYusNvU3sB5oaAV2cOyVEjWftUXKOYdplDeiPZrMN3bDcGvqo9
ojcNn2dpe73r0psXshmWrWR+LH9pK0cWIjFouyerUNc9y4FU14wTNyCKe2Ce4fb+vPXo5QN8gJo2
z1CyWaJfoRcL5SdTmUM8Z7hAT/23L+OECJeG5W03pe45lcc5HwJoowkG7UCraiQb9XFq6FWizECl
KqY2JcdEzG1Zp1TsnfLE76QDRudUHnMJlHkGibn7xHMYme+kTp+SOqFclbndZyVsPbGfc9VOzNe0
I8+SZCo1yNgpt/6Zrwl5aY9sFLXWTjtL/pXTnHXbCvEaxIx+J7nWTguzqfTOnL33szbva2Inf+w0
IJRv9wRHwsxIA7yshLFZMN/cuNolLn6+ubyyQRwZ67frH+u3u16+edrO2jJ9BLN/cuTyQibKEpK4
CQdkLpaaZ5gtbd0sVa1VS4ELXLU09ugvjrRu6V6yWwxfsiOdJtJhS3ZCjJRxWGbtS+sSEoAHO3zd
kigikKVkkwhy3iECYvPlEIGEWxEk2Fz5Ij7vDMnfLXmWbnNx168DSLDuTeyNuj5kXPQUvnTrX712
nWDSqL4sWKxElpxZrBSyAG5euuFvIJGO30T/a3FMHMxsFKb2liaRCDydKBuIA9kRGDkMsE7Lk5AS
z0gqcrnJhlGRuXAciLyEDuNqJT86U9ENPG/x6CeP3wTaYZupQmTbzBGzpBvTF4sxmghpQB8sTaZh
MFmSZeLA4Ahzl4OPEpXscmQTNA6+Bq6EXPQel4ANHmYTz2oEU3mmM5H2YfGxnp9ENkgWyUMHk2Jx
ZQPP7hKM3bkze/s7Fg6FWdx280PBQby7aMKVfwsOxQqzuJHrlYaszCxF8ljYqMDhyzo8NhZh9p45
NoMwmJTaSUOzKTiYuYnEda+7QjEIxWPxh4Fe7UjiangX9DD2c2V+omHsFypCAI/Flfj9zXMxAofe
Rl6wG9iXB9zVGm2R8cC3aKYKw+HtI5tl4ZBIh2NBN9EVYjOVBwfTImPaJjeRxNdy61wgKW2LHKq4
aoXiWFqHJC8hHMXzBcBJdGJfgoCWS9VkiJFfbiFk3qsUnw71WTOih6jUziM+ksS0ka9a2n7cztJ7
d28yxqmLVB6GPgP2tNE249zbr5z4sl9fxq2wOSN9hScwkpSBeQLj1QzJUS5Ya1TwCc87J4sIRgSN
iwgYWSgrWSP3aGTsAVvj61O/YSQlnYAFrbiTDszQ8bB7XYB6UEy/OWcjHtFZQTBCdlbQvTjwsf5O
RcvOAzxokTpm0QiEKzNVZ234hE54gha0c1gndMITVBMmcE7stBOetkgyj4UK5mtORPuYRTuV+itr
7tFHOUDu+JWzff45YIYMnlP6izNzj4UiOmq/eGOBorZ/Sr6azdbuHwTr5Npy1l4CNSJ7cbGwUnco
dskxUkeRiSxfesNOZF3mnfZg9qfRIk9hKORn+2vZq9VeYeNKPtlWn+oZY1fQjrh4f5GyVjUfnPW4
V4e9xMVh/ctOOlKsIpb219GG33BmIvL+wEiOiKXaqXGcM0hlqXUlmr8OH56N8s3dxeqL+Un8wITJ
jWJmHu+3sMV7+PMmdsSXVsXIRYsvw3Oz7dfFW5vb7kVXdvR1tf7bfiRT59U6Y3m9SRVHzvTOU/c3
ezO9Unp4YCeRnvKGnM+LV7J5xOzqg2J+KlXtZOmTZMJdf297sEmkt0+Ll0/lUmumtn1++biw+5bb
IucMr6E2sVZ/B92CkVY1lFn5RfGcFRt+Uiw5G3EKZ8WGnxRL9NgUzooNPynWPBV34g==
]]>
<![CDATA[
s2LDT4olOzamcFas76TY7f+zkViFWT8QhJfddp1e0Eyk0/DLRWMw7CKA8rLT+Gi2K9W/Gr2EkDT+
5eFf/KvqSUHUkqKiwBcFf628JTLFautn2EgKi8lKO8Ent3cT6Zf8dm9QatYGzU672vsruYI/3R5X
rg5KyZWk+cYLvLGazABS/AuAw7NFXEx9AURfsB347/ZP/NBIDOF/pwmeEyWd/CMXJEXRRESKE1Se
/COomiZIOvxSMH4QJU0WNEVLfiV4cxDQ4l/w5RA+/Iaf/kwKfPI4+fDEJ+vY23lCkkVO56FpUVUk
nS8kJQXakzVZ1xRJEZRC8jshSRqnqTx0p6iyKOh+GElSOEXXVV2UNV4uAISscpKqyarO80azfgiJ
g/8U6FvRJVVJ1hJ+GEnnJF5XeF1UVUmWk35MpAIHHciarsoFXgcI33i8ENCPXOB0SdcEHXrUJY3R
CgxQ5HVVVTVJ5CWBgYkPgjEeP4yXKj5MfJSNnJ9a4j0hiSonFARVloSCzBekpCQqHK/KMg/8oCAp
YRZFnSsoqirAy4ifD0SSBK6g6gWNPISIVy/AeOAR+cH1UId5kmECJK2gwizg1FGPJRHehQFKfAGx
Sfp6lmROEHhZEBVdLeAgfeh7IaAHUeYK8A9MvyCoZOp9rYhAGUmVVOAgnQzIh4gXgjESP4yXFD5M
fJSMnA6cNCLoS0NQOqWEICucKOqC3SZMNyfKqiTIsiLBEGEC2TC6JoI48MB0crLCgtGAw3hRVzXk
FikpAEOpQBlBkQymFDWBE0SghMADAPQEtOAUVRR5WdF0DXjdB1FMCBLPKTxIoCoWyE8+mAoDpiBx
sipIAshBAXFBGJkD0osSb9A2FogO866LBfgApDFAVA6mTAAJFolaYMHIAlAG0DGZkNUTEE9VdFEo
SAY9mTACJ8sqRRzoSlXhjYKgiKgZEEbiCrogiubswSSgjlZFXUe9pmlJxjSJHOgBSVBkYDo2hIch
ioSFSsbAdAUUBK+AZhQIJA+QvCga2uybBSNxCgy1oAgSYXxBBl0FKAPRJE0kECJAAOOIhlQjVwDD
CDpvYugFKPpnygPBmEtV5QoC9FcQJOjUmEsNxilDT4UCshITBpAFvIObYYy3wKkFUSxopipgUw1Y
1VTNEo4nkrIVmIOlq4RQ0DiYfaAe0YFIGxkMiga8QaiF6lcoKBzIhqAXRI20jzCg+OF/Ok8YB3QF
WBBZUFWzdezOkR7G4wInKRRXAcYsGBk4D6hkKMkKC0blxEIB8DSVIEEVZEfkVZ6wGkLosoNIAagt
w0hUwxa6H9cMcgCNwFobDXrfB3MAqhAMo2HSCAI6TB2v8YTOwPAc6iatwBs2Doch8oCihrxpaCDg
YJc8qyDyoLwL8JpkKkNoBlQwKHcwuqQjDTRSwUVyHVysAjTNK4SEqMYkYBQNmidiQAZbALdKVpAY
kh8CxytxlIlmwAgFnpM1uh/AVoS5s7FlQIBPosigqE1+wdllwQCHGTMJ7kOFBQNCCDzNK4KqEOIW
wABogqBpOvoROH0Cpwiu+QfGklRaF3j0F44ZBqCploqTiB4EE2OMBycEITQdZELQBWIEEQIUqSNh
DAjQMWBpATeicMmYWTAw0bpkzAgZsw8GGMp0ugjDoQ2UqPnBSZVpbQsvQHuUcfAA1Ij8gl0Hf85g
ZFYjoPYLNhcbaMiaI0mE9LyqCLqhwXEoqg6NSrpIpgaGq4A10YCrRdngUOyFlykYHK4Aw7V8RoKt
TNQPeAICmVEUcUUvGOQwDS/Opq4bDgkZL0wHSAuvmgbTA1Ej0sOrrgF7WwERVBXwaSSBJ16NiIoD
mE+1jYYfQiOmEQIVQ1MaguyDAdfJpfB9MICcW3nCDyoIC1FJhj6QQAnJ4LTzmmgQP0pJo1MGQRW4
bq5J1MHgaxIP/EPIAKpcU9CnMuRJVPwgFT8IYgMAAk/iA0M7eXuKA+PvyuNICjIQD3Qeb7AGaCJR
oaQfsOfBOQXlxEMMYeh/hpcjgDcHqlcHERcCYUCPyDpoGsUgH2F32tUEGBG9CgkY3tTsTBiYStHD
Z96+wH/WQNvYBomFDvonHq/VNfRKJHEqlksFcOBTUvaP58AWgeZSRGLxgIoCGFbNxW8FDqYN5FUg
bGui5B6Zt51KdFemi0HPsY7qTBQ0XZdNfed1vr8TOogDbR397rkXwk9SXQGtDx3xMkyzgBITCwak
t6DCsHX8RUcYiCcUk2EtteeGAG8BTBDlcHhBQOxBb5jhk+HyAZ0gBBZkgwgsCJnTaWRB1fhhwKED
BuUFI1AgqPhgQGXBXNgxusCDnDpGikH+6AmynXceZgF+ERWSNjCUkgY+ZwHdcuz+mwUjgRdNuTqg
MQBF4GuFqDqJGH1RpMYOGIHWE3ScI9Mzdz0vMibSC8OabL9vjj1BUG7GLWwYxBeoC7gavzEceP+Y
wdq6TAuLcrodG0UT1vLdFWAknuZOD4/DBCgy6RsQLBixGEP9+GAYAbG3qxgg/p7c+h7klzMtnMhU
9yBTmJcSeb5gMAujSfCcOFDKwPOm5WHCiJwOroeuqRIvs9U9CDAwJsiOajjqbBiBA7mg4jtGXyLx
fR12ZaGjgf7VrAiAqe4jaGNpewSTaJr7tT34DOjrUS6XX9sjRuAaAcfxRqjFUOWRXZlMKSoSB2On
BMSv4aEf4r44voGfnfwwDEpiPACv8YpihMbxYFQOE862UqwwcI4D48f5PSFKqt9fVz1sLeHcqo6c
eCCgTXAQFUqNY8CiUqreD4EKT6ei+2KCCSOB3S8YzEto44eBSAHc6oLt/CGuCnAPr6PXa8TDEFAC
oGYGpr4ReyFq0A+EzeD2Q+hmJJr8rcjgsQNTGtkKM27nNXCaVcuNk0VP9gpwBSsq2rlZGLMM2IIa
M+JO0TCAKm9nQciYZQgFwJ6oshkQYmQNUYHj1yMuoubhTtlKyBGiqB6ieABqhLKKRMeY3jZEwAy8
T3CijOAIB+xGww/hn2QmDJ1qqzBgCuhF6054jsgWBEv/m84SRKaSMV1ogWDEGq/aboEfAoaMZHOl
4XytIOkt9K3oTwKzaCcBRBmzVHTaCuN5Zz5xioGwMD6HlcDfAs4SdU2SCF9UCCaC2+ip4MbBW6KV
kQSGxOyYKyL2CGGUIGPIBaE8hwsrTtrVnz0D3GHawIGRTV3CUnaa7EnfMmDA68VpVBXRyO6jBgbr
6IyKBcNQiOAKISeGBVF+GBUT4iqdooKJxCUiYC9FCPIJgF05FTxZjbfIyoKJoiEqVjDenAThpGM0
GXlKwBq4jZp3X55Sl4ERKOvsTlP6nvqzlAwQb5LSB+LNUSKa7hyVK8eoFyD0cjIt3gwlEsI9SPfb
JJdF52o9GUrgFk4WXMG7L0MJVs6TfvSnKLGdgizYS0WMFKWue1S2L7mIY1UVKjnCSFECf7gTPv5W
IIaAAQMCopnV9aYo/RD+FCUTxpOi9MN4U5Q6+Jq6E6f7EpQwYkWmJYKRoES6gdSY/MFIUIJLjGlq
QRVN59SXoGRA+BKUbBh3gpIB405QAq5gbOh0nDe3qKPyLVC8xMhQgkgobmfP14oEnCJ7UjauDCVQ
HpC0UWXmKEEX6xAhq5JpLFg5SmgHZk8AR0I3lsB8OUqQcJ81dKcXdUTOZel8SUqUH7eb4YVBKdTB
S9fIV+IqepKUDAhfkpIJ40lS+mG8SUrEFiwYZt9MH9SXpIzU0N6VY7KSp0OvBctBYMSAOEEiOIZm
7pnt4sOswswbGRd2socIou44h8z4DtQGjJ5ei/XDgJIrqGp4vInWXFLd/pQPH3TCRLdl9AaBkfSx
40BQQ7p76cQfCKJvD5ZDNZx7iRkIYjJD9dh9byAY2Ze9tIgCCcEG0QwACNwDxhLCGGvlFvMT8BPQ
XbWcCB9MxQ8DPaGXCMyny9YSubevODCMvrwZCgkYgpc1RTPVBegPSggkEl8DyYARNFkrmHGhBwbT
BgJ4tiSphEILThrPG4EPiQRkMNCyrMsFkzPRgQC7SbkdCAMUllXb7qAKgiZME2hlJ8DzVygSqKgL
VMp+EVQKCpknopYARAJNospmts/IBYCmUwQZl9iQ6XQSVKm2osWMArA4NWLQzaq5k4O0KqDjL1kG
S/YBoPLTOCcDSubU0wavoIG2JxAACpyzYQTx4jF4cMgK8whaGVjbUmtINoVD7aWrvLEC6oOpGDCq
bpFbTxK/1kxHmgEUCo5EJILsAQIAFbewGbkQnGAvAIzf8hHIYBgAMnyyyV7zdyKAFQLEzUYwHARD
rCuyrhQMVwm5Vy/YeGKSC57Kuq6YW3vcz5HmSFLQ6IqZ3vRAELcDmEe1UtmgLDg7Aifroj4IHreL
aBBOK8auMNN5oWEwllCcDJRGphYUDSgec0eRX2Ii5a5mJ8BIVsDMWxGcJVwbUMEzNXJ0hoQqKsXR
PhjQ9ZiRlw2BIxOkcwWJEi+SHnQxmwL+CWhQQTRSimhnvfzoAakYMyCbtCLIQgRn7Bg0rLmGKTZF
tDfd+RGNGm7N1L0kOIN/jZyxZlBQo/ZOfZPlAjA/YF1NdHwwAo/rB4bC1WRnUVYAvFVqaxaRXte+
CHC1/DC8O7bHFSSya1JX7Ux3DBhTa4O7IRp6ruLvKxYM0QWUX8qAQf0IHrAVi+H6o+pkMDQybt1N
MQmX2im6eyFqCRAQXrLNkKr4YUDVySCn5pAJRAEQE0WJKFxcpvFC4GhA9h3/uJjww/ipAqaogJty
bTMZCwbXQACPMBgcE6ZlJJJyBxjQAuA2UZvufLwWxbFkjRvTMtTSmFeHfZN9WjJve02yT8tJ4AiC
EwXibqzPgbMN6gFas/dXiajBQGwNN9vQF2h5zAEjbRkwhG62/cKFXzTjGq8rtjqNBDH4nzL9FX9P
cWAM3QOaWy4UVCOFwsCY52yPgmh3CZSLWrDZEoct04TDWF2kSe96XiObzsDJEiwL5n5dRk3lrGBj
9+CJqAVTXfqewxDAq3JMSzHhBWFRQga/QnPSUrFgJB5cC2DNUBgYDYTxFnlwl6OMXqm520XyW9MI
TiXcDIECRHNuqdCgQV7XDQWDSS1gT4naVsPSbSB+YFGd/SEsGE0Ek6Y5KQRoF/Sss9MNt2xAwCZT
mUpWMyTAtHYdB3WFa6SyGT+zhlWJMXRrOQUIIAuC6a+hSwIK2smufbNgCEYwVpPyxkIH/CBZPncM
ENMUyVSi0ttRDBBUy7iLu2BGXWwYDd1FmBTZXHpEOQJHQBUcXxC8LKlgJPChYxnMEsykia3kh8BE
uYphmqTppmfgg6mwYHBdRpbMzYsWjEINkoAUwBIpqrWNh+T1wU+zghqA0dyjxny7AsxrJLRIKwq6
lsBmVgwROdO47wDJqRRUawEWd6eDkRMh5rHaAX5AW8ljwtEoFQCdAYwpFmRjy2DFC2Dyr7WRxcqi
g2I0t/9qMWHAZ4XA3F7h8XcUAYDOBjw2Y28jXvMAgILmecd0ieBKKCKAO7tEdQzpeQ==
]]>
<![CDATA[
TTJzSkBAkHqFtx1GH0QtgeoP9b4Trvlb0TAYA7ILgh3j6oou8AXZcgnAYQY/yS5DQdlwEgkSBrEI
A8qU6gfdSt2ccUIQBgjGChpNeYQRdKwZks3sGwaoBd5BF2GAScFpdAgDMJJE9YWDBuuoU0GsjCuQ
9KAVzOMD+1lM7IWokTUQY93JmB9fEx52FUnqH4wwbwVxfgggtYhJWMnyNfxM7+ckJAp8CWVHBoyP
rRl9xYDxCqE3j4JFJcAnwEYCM3b9ToD9wASkpfR81lTC3QcQSIH5MdIBvtjUD+GPTX0wvthUwigb
pk6yRcwbeeJYQE9hxkaypcUTm2L1DjQrGasali/ragXLtuzqAk9GCCu2UO2pThjiywghDIRIhEk0
k/c8CSHsQ1Kp3V+MhBDBo+DsDfHngyQJFKjNjxojH4QFVPDAWTXw5nKAJ6ATe4srKx+EahrMDpXZ
9raBDKLAjIvW/hxvPgghqIUJRjpIIrUXqrX6yEwHERhoxCnTI+kg8JOt7L8B41gykg3ioZmCWTDl
fupJBfmeevJA7ufeJBCWGQogwBqvFlhJnihBs9ImPlp5UhWmQBosbnnrVKYCpwtmX7KcCX8eAjGR
6CUrRqYCxQRkz2EtfysQzIFUmEVwIiMxgxQJG0kxcqzWviVczwChV+zUN8iCTvuZfgBU1cApmrMm
6oXBGZaAP0VnQR4sk6Rbc2JYaF1VzeQ5SiluipCwRpY3Vk3RVPEwcFm2w0+Ewd1Jds6YwECPgmRK
A66K8B51D0YRmN1OIyRh6sDaKk6AimYeXAVBMRP5PgASMkpG9YWZyPWBgLgUBN0uFxSxLECkvAsS
SQn0js4CrqGC52CEL7ofokYGrDuiwGxFxd2bTgoP93hLoNrsra4qeOumaTaTm+h/2jMDVMUNFa6A
HfwTVXVqwHDpQ5UlADAXo9CgFKzNKcZzydwJYBotDYMkym0soCOs0+MADw84BuTeWEbDNT5okKey
lcThtsyYROhVAKtXsGpGfBDGtPBen51qQkE+pfwjRFUpWIU1yIU+CHTNJBm9KiMOLSaYMLa9MSjm
B8H0DGBeMK2yqGhYPmjnIYlC1akKSDJeD7PjtnuwEFaBIfIHppc0ZykHc1SOGjc3d8s6UM2q9UXn
WdMtOy4xIdAhp3gZ+/HBEP1jqShj5Ro4jvaE0ZI5IOZqoG5zqg+gRmRXkVzLWd5GcFGsUNDtZQvD
LINLLZrJYxG39fIybyWbcTQuFYETCGqElk1i/2V7gCRnrQhg36Aje1kXUYH3NdmsJ0cYkTNqK83h
KB61qCgcLnPbKo04PMCQol3IB1oCwllHB5AYBJwcydkEifv28LgA3dq67oGoEekCneCOU9yt+JU4
FqnL1n5MiQVB2wGMQkUNmU2xAhDbSaYXNnGd2Iyq2auabgDGcqWvlzgwzCXNq4SezCwmb28SlR3j
3Ijddp2cGpHLJdLps+pH47JXbbYavcRHv/pHI1lttzuD6qDRhSfJj16jP+j0Gsn+Z+dP/OX/G1AL
TLmqqqu/Gy8ASEwTkQ==
]]>
</i:pgf>
</svg>

After

Width:  |  Height:  |  Size: 40 KiB

13
scripts/build.sh

@ -0,0 +1,13 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../src
xelatex -shell-escape main.tex
biber main
# xelatex -shell-escape src/main.tex
xelatex -shell-escape main.tex
xelatex -shell-escape main.tex
mv main.pdf ../main.pdf
)

10
scripts/clean.sh

@ -0,0 +1,10 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../src/
rm -f ./*.log ./*.tuc ./*.out ./*.aux ./*.toc ./*.pyg ./*.bbl ./*.bcf ./*.blg ./*.run.xml
rm -rf ./svg-inkscape/
)

9
scripts/mrproper.sh

@ -0,0 +1,9 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../
rm -f ./*.pdf
)

16
scripts/test.sh

@ -0,0 +1,16 @@
#!/usr/bin/env sh
set -eu
(
cd "$(dirname "$0")"/../
# Testing scripts
# shellcheck disable=SC2185
find -O3 . -type f -name '*.sh' -exec shellcheck {} \;
cd src/
# shellcheck disable=SC2185
find -O3 . -type f -name '*.tex' -exec chktex -q --nowarn 26 --nowarn 15 --nowarn 17 {} \;
# shellcheck disable=SC2185
find -O3 . -type f -name '*.tex' -exec lacheck {} \; # TODO: fix lacheck so it's possible to disable some warnings which are incorrects...
)

3
src/abstract.tex

@ -0,0 +1,3 @@
\begin{abstract}
Ce document est un rapport de mes travaux de recherche sur le sujet \emph{TODO}, effectué dans le cadre de ma formation en Master 1 Informatique à l'Université Paris-Saclay, j'ai été encadré par \href{https://www.lri.fr/~filliatr/}{Jean-Christophe \bsc{Filliâtre}}.
\end{abstract}

1
src/app.tex

@ -0,0 +1 @@
\section{Applications}

1
src/appendix.tex

@ -0,0 +1 @@
\section{Annexes}

91
src/bdd.tex

@ -0,0 +1,91 @@
\section{Les diagrammes de décision binaire}
\subsection{La logique propositionnelle}
\subsubsection{Les propositions}
\paragraph{}
Une proposition est un énoncé pour lequel il fait sens de juger de la valeur de vérité. Par exemple, la phrase \enquote{\bsc{OCaml} est le plus beau langage au monde} est soit vraie, soit fausse. En revanche, pour la phrase \enquote{Ça va ?}, il n'y a aucun sens à dire qu'elle est vraie ou fausse.
\paragraph{}
On notera $\bot$ la proposition correspondant à \emph{faux} et $\top$ celle correspondant à \emph{vrai}. Une proposition est donc un élément de l'ensemble $\{\top, \bot\}$, que l'on notera $\mathbb{B}$.
\subsubsection{Les fonctions}
\paragraph{}
Dès lors, il est possible de définir des fonctions de $\mathbb{B}$ vers $\mathbb{B}$. On a par exemple la \emph{négation}, qui est la fonction qui à $\top$ associe $\bot$ et qui à $\bot$ associe $\top$. La négation d'une proposition $P$ est notée $\neg P$. Par la suite, lorsque l'on écrira $P$ sans plus de précision, $P$ sera tenue pour vraie, et lorsque l'on écrira $\neg P$, elle sera tenue pour fausse.
\paragraph{}
De façon similaire, on peut définir des fonctions de $\mathbb{B}^2$ vers $\mathbb{B}$. Soient $P$ et $Q$ deux propositions, on a notamment la conjonction de $P$ et $Q$, notée $P \land Q$ ; leur disjonction, notée $P \lor Q$ ; l'implication, notée $P \Rightarrow Q$.
\paragraph{}
$P \land Q$ vaut $\top$ si et seulement si $P$ et $Q$ valent tous les deux $\top$. $P \lor Q$ vaut $\top$ si et seulement si au moins $P$ ou $Q$ vaut $\top$. $P \Rightarrow Q$ vaut $\bot$ si et seulement si $P$ vaut $\top$ et que $Q$ vaut $\bot$.
\subsubsection{Encore ?}
\paragraph{}
On ne détaillera pas plus la logique propositionnelle, et l'on considérera par la suite que le reste est connu. Le lecteur souhaitant en savoir plus peut se tourner vers \href{https://www.lri.fr/~paulin/Logique/}{ce cours de logique pour l'informatique}.
\subsection{Représentation graphique}
\paragraph{}
% TODO
En une phrase: les diagrammes de décision binaires permettent de représenter les fonctions de $\mathbb{B}^n$ dans $\mathbb{B}$. Les diagrammes de décision binaires peuvent être représentés graphiquement, ce par quoi on commencera avant toute définition formelle, afin d'en facilitier la compréhension\ldots
\paragraph{}
Représentons tout d'abord la formule $P$:
\begin{center}
\includesvg[width=100pt]{simple_bdd.svg}
\end{center}
\paragraph{}
Un diagramme de décision binaire a donc un sommet \enquote{de départ}, $P$ ici. Un sommet a soit deux arcs sortants, soit aucun. S'il en a deux, alors, il contient une \emph{variable propositionnelle} et dans ce cas, le \enquote{chemin à suivre} dépend de la valeur de vérité de la variable. Si la variable vaut $\bot$, on prend l'arc en pointillés, sinon, on prend l'autre. Si le sommet n'a aucun arc sortant, alors, il contient soit $\top$ soit $\bot$, ce qui correspond à la valeur de vérité de la formule représentée par ce diagramme dans le cas où on assigne aux variables les mêmes valeurs de vérités que celles que l'on a prises sur ce chemin.
\subsubsection{Ordre}
\paragraph{}
Prenons un autre exemple, voilà un diagramme représentant la proposition $P \lor Q$:
\begin{center}
\includesvg[width=100pt]{simple_bdd2.svg}
\end{center}
\paragraph{}
Il aurait aussi été possible de la représenter par celui-ci:
\begin{center}
\includesvg[width=100pt]{simple_bdd3.svg}
\end{center}
\paragraph{}
On va en fait se donner un \emph{ordre} sur les variables et dès que l'on \enquote{aura le choix} entre deux variables, on prendra la plus petite des deux selon cet ordre. Par exemple, si l'on décide d'utiliser l'ordre lexicographique, alors, on aura le premier des deux diagrammes ci-dessus.
\subsubsection{Non-redondance}
\paragraph{}
Une seconde chose à prendre en compte est le fait que l'on va éviter toute redondance dans nos diagrammes. Si deux sommets mènent au même résultat dans tous les cas, on va les fusionner. Sur notre exemple précédent, on peut par exemple fusionner les deux sommets $\top$:
\begin{center}
\includesvg[width=100pt]{simple_bdd4.svg}
\end{center}
\subsubsection{Simplification}
\paragraph{}
Enfin, si les deux arcs sortants d'un sommet mènent à la même chose, on va tout simplement supprimer ce sommet. Par exemple, la proposition $P \lor \neg P$ ne sera pas représentée comme ceci:
\begin{center}
\includesvg[width=50pt]{simple_bdd5.svg}
\end{center}
Mais comme cela:
\begin{center}
\includesvg[width=50pt]{simple_bdd6.svg}
\end{center}
% TODO: ssi tautologie...
En fait, on a en quelque sorte \enquote{calculé} la valeur de la proposition.
\subsection{Représentation formelle}
\subsubsection{Opérateur \texttt{if-then-else}}
On définit l'opérateur \texttt{if-then-else}, de $\mathbb{B}^3$ vers $\mathbb{B}$, et noté $P \rightarrow Q_1, Q_2$ ainsi:
\[P \rightarrow Q_1, Q_2 = (P \land Q_1) \lor (\neg P \land Q_2)\]
Ce qui se lit: \enquote{Si $P$, alors, $Q_1$, sinon, $Q_2$.}.
\subsubsection{Forme normale \texttt{if-then-else}}
On dit qu'une formule propositionnelle est en forme normale \texttt{if-then-else} (FNI) si elle est construite uniquement à partir de l'opérateur \texttt{if-then-else} et des constantes $\top$ et $\bot$ ; et de telle sorte que le premier opérande de l'opérateur \texttt{if-then-else} est toujours une variable.
\subsubsection{Expansion de \bsc{Shannon}}
On note $P[Q_1/Q_2]$ la proposition $P$ dans laquelle on a substitué toutes les occurences de $Q_1$ par $Q_2$. On a alors:
\[P = Q \rightarrow P[Q/\top], P[Q/\bot]\]
C'est ce que l'on appelle l'expansion de \bsc{Shannon} de $P$ par rapport à $Q$.
\subsubsection{Passage en FNI}
\paragraph{}
Pour n'importe quelle proposition, il est possible d'obtenir son équivalent en forme FNI. Il suffit pour cela d'appliquer l'expansion de Shannon de $P$ par rapport à n'importe quelle variable $Q$ de $P$, on aura alors $Q \rightarrow P[Q/\top], P[Q/\bot]$. Puis, on applique la même transformation à $P[Q/\top]$ et à $P[Q/\bot]$ et ce jusqu'à ce qu'il n'y ait plus de variables disponibles, on aura alors forcément soit $\top$ soit $\bot$.
\paragraph{}
Par exemple, la proposition $P \land Q$ peut être mise sous FNI ainsi:
% TODO: align
\[P \land Q = P \rightarrow (\top \land Q), (\bot \land Q) \]
\[= P \rightarrow (Q \rightarrow (\top \land \top), (\top \land \bot)), (Q \rightarrow (\bot \land \top), (\bot \land \bot)) \]
\[= P \rightarrow (Q \rightarrow \top, \bot), (Q \rightarrow \bot, \bot) \]
\subsubsection{Passage en arbre binaire}
...
Ce qui donne le diagramme suivant:
\begin{center}
\includesvg[width=150pt]{simple_bdd7.svg}
\end{center}
\subsubsection{Passage en graphe}
Une proposition en FNI est en fait représentable sous forme d'arbre binaire et donc, sous forme de graphe. Un diagramme de décision binaire pour une proposition $P$ est donc simplement la représentation sous forme de graphe de la FNI obtenue à partir de $P$\ldots~après avoir appliqué quelques transformations à ce graphe ! % TODO: better explanation

86
src/bib.bib

@ -0,0 +1,86 @@
@article{Bryant86,
author = {Bryant, Randal E.},
title = {Graph-Based Algorithms for Boolean Function Manipulation},
journal = {IEEE Trans. Comput.},
issue_date = {August 1986},
volume = {35},
number = {8},
month = aug,
year = {1986},
issn = {0018-9340},
pages = {677--691},
numpages = {15},
url = {http://dx.doi.org/10.1109/TC.1986.1676819},
doi = {10.1109/TC.1986.1676819},
acmid = {6433},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
keywords = {Boolean functions, binary decision diagrams, logic design
verification, symbolic manipulation, symbolic manipulation, Boolean
functions, binary decision diagrams, logic design verification},
}
@misc{Andersen97,
author = {Henrik Reif Andersen},
title = {An Introduction to Binary Decision Diagrams},
howpublished = {Lectures notes from Technical University of Denmark},
year = 1997,
note = {\url{http://www.cs.utexas.edu/~isil/cs389L/bdd.pdf}}
}
@article{Hayes97,
author = {Hayes, Barry},
title = {Ephemerons: A New Finalization Mechanism},
journal = {SIGPLAN Not.},
issue_date = {Oct. 1997},
volume = {32},
number = {10},
month = oct,
year = {1997},
issn = {0362-1340},
pages = {176--183},
numpages = {8},
url = {http://doi.acm.org/10.1145/263700.263733},
doi = {10.1145/263700.263733},
acmid = {263733},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {finzlization, garbage collection, resource management, weak pointers},
}
@article{Leroy00,
author = {Xavier Leroy},
title = {A modular module system},
journal = {Journal of Functional Programming},
volume = 10,
number = 3,
year = 2000,
pages = {269--303},
urllocal = {http://xavierleroy.org/publi/modular-modules-jfp.pdf},
urlpublisher = {http://journals.cambridge.org/action/displayAbstract?aid=54525},
abstract = {A simple implementation of a SML-like module system is presented as a
module parameterized by a base language and its type-checker. This
demonstrates constructively the applicability of that module system to
a wide range of programming languages. Full source code available
in the Web appendix \url{http://gallium.inria.fr/~xleroy/publi/modular-modules-appendix/}},
xtopic = {modules}
}
@InProceedings{ConchonFilliatre06,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Type-Safe Modular Hash-Consing}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
month = sep,
year = 2006,
url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf},
}
@book{Knuth11,
author = {Knuth, Donald E.},
title = {The Art of Computer Programming, volume 4A: Combinatorial
Algorithms, Part 1},
year = 2011,
edition = {1st},
publisher = {Addison-Wesley Professional}
}

1
src/conclusion.tex

@ -0,0 +1 @@
\section{Conclusion}

1
src/implem.tex

@ -0,0 +1 @@
\section{Implémentation}

8
src/introduction.tex

@ -0,0 +1,8 @@
\section{Introduction}
\cite{Leroy00}
\cite{Knuth11}
\cite{Andersen97}
\cite{ConchonFilliatre06}
\cite{Bryant86}
\cite{Hayes97}

27
src/main.tex

@ -0,0 +1,27 @@
\documentclass[a4paper,12pt,titlepage]{article}
\input{packages.tex}
\bibliography{bib}
\begin{document}
\input{title.tex}
\input{abstract.tex}
\tableofcontents
\input{introduction.tex}
\input{bdd.tex}
\input{implem.tex}
\input{app.tex}
\input{conclusion.tex}
\appendix
\input{appendix.tex}
\printbibliography{}
\end{document}

75
src/packages.tex

@ -0,0 +1,75 @@
\usepackage[french]{babel}
\usepackage{euler}
\usepackage{fontspec} % encoding
\setmainfont{Linux Libertine O}
\setsansfont{Linux Biolinum O}
%\setmonofont{Source Code Pro}
%\newfontfamily\unicodemonofont{Everson Mono}
\usepackage{graphicx} % to include img
\usepackage{enumitem} % powerful lists
\usepackage{xspace} % correct quotes printing
\usepackage[np]{numprint} % correct numbers printing
\usepackage{amsmath} % maths and better typo
\usepackage{amssymb} % more maths
\usepackage{dsfont} % and even more maths
\usepackage{color} % color power
\usepackage[dvipsnames, table]{xcolor} % more color power
\definecolor{darkBackground}{HTML}{282c34} % source code background
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background
\usepackage{microtype} % better typo
\usepackage{hyperref} % internal and external links (e.g. mail, www)
\usepackage{cleveref}
\newcommand\myshade{85}
\colorlet{mylinkcolor}{violet}
\colorlet{mycitecolor}{YellowOrange}
\colorlet{myurlcolor}{Aquamarine}
\usepackage[cache=false, draft=false]{minted} % source code
\usemintedstyle{paraiso-dark}
\setminted{bgcolor=lightBackground}
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{12pt}{12pt}, frame=none, stepnumber=2}
\usepackage{placeins} % float displaying
\usepackage{tikz} % .tex figures (e.g. from Dia)
\hypersetup{linkcolor = mylinkcolor!\myshade!black,
citecolor = mycitecolor!\myshade!black,
urlcolor = myurlcolor!\myshade!black,
colorlinks = true,
pdfstartview=FitH
}
\usepackage{csquotes}
\usepackage{ellipsis} % correct ...
\usepackage{svg}
\usepackage[
autolang=other,
backend=biber, % choix de l'outil de traitement
backref=true, % liens dans la bibliographie pour remonter dans le texte
backrefstyle=none, % afficher toutes les utilisations de la référence
bibstyle=alphabetic, % style pour les clés des références dans la bibliographie : [initialesAnnée]
citestyle=alphabetic, % style pour les clés des références dans le texte : [initialesAnnée]
sorting=none, % bibliographie triée par ordre d'utilisation des références
]{biblatex} % support des bibliographies
\usepackage{calligra}
\usepackage{tikz}
\usetikzlibrary{matrix, fit, chains, calc, scopes, positioning}
\usepackage{auto-pst-pdf} %To compile psvectorian directly
\usepackage{psvectorian}
\renewcommand*{\psvectorianDefaultColor}{Red}%
\graphicspath{{./../img/}}
\usepackage[bottom]{footmisc}
\usepackage{wrapfig}
\definecolor{processblue}{cmyk}{0.96,0,0,0}

27
src/title.tex

@ -0,0 +1,27 @@
\begin{titlepage}
\begin{center}
%\vspace*{0.1\textheight}
\fontsize{25}{25}\scshape Partage d'implémentation, implémentation du partage:\\
une bibliothèque fonctorisée de diagrammes de décision binaires
\vspace*{0.1\textheight}
{\fontsize{18}{18}\calligra{Rapport de travaux de recherche par\\}}
{\fontsize{28}{28}\scshape Léo \bsc{Andrès}\\}
\vspace*{0.01\textheight}
{\fontsize{18}{18}\calligra{\today\\}}
\vspace*{0.03\textheight}
{\fontsize{18}{18}\calligra{Master 1 Informatique\\}}
\vspace*{0.03\textheight}
{\includesvg{universite-paris-saclay.svg}}\\
\vspace*{0.1\textheight}
\begin{tikzpicture}[start chain=main going right]
\node[on chain,align=center,draw=none](a1)
{{\fontsize{18}{18}\calligra Sous la direction de} \\
{\Large {Dr.~Jean-Christophe~\bsc{Filliâtre}}}};
\end{tikzpicture}
\end{center}
\end{titlepage}
Loading…
Cancel
Save