<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="markdown-here-wrapper" data-md-url="Thunderbird"
style="">
<p style="margin: 0px 0px 1.2em !important;">Hi Thorsten,</p>
<p style="margin: 0px 0px 1.2em !important;">This looks bad! Have
you tried checking the following code (with the second
definition of <code style="font-size: 0.85em; font-family: Consolas, Inconsolata, Courier, monospace;margin: 0px 0.15em; padding: 0px 0.3em; white-space: pre-wrap; border: 1px solid rgb(234, 234, 234); background-color: rgb(248, 248, 248); border-radius: 3px; display: inline;">_*∞_</code>)?</p>
<pre style="font-size: 0.85em; font-family: Consolas, Inconsolata, Courier, monospace;font-size: 1em; line-height: 1.2em;margin: 1.2em 0px;"><code style="font-size: 0.85em; font-family: Consolas, Inconsolata, Courier, monospace;margin: 0px 0.15em; padding: 0px 0.3em; white-space: pre-wrap; border: 1px solid rgb(234, 234, 234); background-color: rgb(248, 248, 248); border-radius: 3px; display: inline;white-space: pre; overflow: auto; border-radius: 3px; border: 1px solid rgb(204, 204, 204); padding: 0.5em 0.7em; display: block !important;">inf∞ : ℕ∞
prd∞ inf∞ = just inf∞
test : Is-nothing (prd∞ (inf∞ *∞ zero∞))
test = nothing
</code></pre>
<p style="margin: 0px 0px 1.2em !important;">The bug is not that
the first definition is rejected; it’s that the second
definition is accepted. I can’t really say why it’s accepted,
though.</p>
<p style="margin: 0px 0px 1.2em !important;">Conat multiplication
needs some other trick to make it productive. In the test case,
<code style="font-size: 0.85em; font-family: Consolas, Inconsolata, Courier, monospace;margin: 0px 0.15em; padding: 0px 0.3em; white-space: pre-wrap; border: 1px solid rgb(234, 234, 234); background-color: rgb(248, 248, 248); border-radius: 3px; display: inline;">n</code>
is added to itself infinitely many times. If it’s a successor,
that’s okay because the consumer just gets infinitely many
successors. But if it’s 0, the consumer has to wait (forever) as
to whether the result is a zero or a successor.</p>
<p style="margin: 0px 0px 1.2em !important;">Regards,</p>
<p style="margin: 0px 0px 1.2em !important;">James</p>
<p style="margin: 0px 0px 1.2em !important;">On 03/03/2019 12:16,
Thorsten Altenkirch wrote:</p>
<p style="margin: 0px 0px 1.2em !important;"></p>
<div class="markdown-here-exclude">
<p></p>
<blockquote type="cite"
cite="mid:2067A3E1-C1AA-41FD-B00A-7731BA3B4E49@nottingham.ac.uk">
<meta http-equiv="Content-Type" content="text/html;
charset=UTF-8">
<meta name="Generator" content="Microsoft Word 15 (filtered
medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt">Hi,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">I just
set the exercise to define multiplication for conats for
my course on type theory. So please don’t blurt put the
solution – see the attached code. The following is not a
solution because agda doesn’t see that the definition is
productive (even though it is):<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) with prd∞ m
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) | (just pm) = prd∞ (n +∞ (pm *∞ n))<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) | nothing = nothing<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">but
after the following change<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) with prd∞
m
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) | (just pm) with (pm *∞ n)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) | (just pm) | x = prd∞ (n +∞ x)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">prd∞ (m
*∞ n) | nothing = nothing<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">agda
seems to accept is. Actually even if +∞ is not
contractive.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Is this
a known bug? Otherwise can somebody remind e how to
report this?<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Cheers,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt">Thorsten<o:p></o:p></span></p>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<p></p>
</div>
<p style="margin: 0px 0px 1.2em !important;"></p>
<div
title="MDH:PHA+SGkgVGhvcnN0ZW4sPC9wPjxwPlRoaXMgbG9va3MgYmFkISBIYXZlIHlvdSB0cmllZCBjaGVja2luZyB0aGUgZm9sbG93aW5nIGNvZGUgKHdpdGggdGhlIHNlY29uZCBkZWZpbml0aW9uIG9mIGBf
PHNwYW4gc3R5bGU9ImZvbnQtc2l6ZToxMS4wcHQiPiriiJ5fYCk8L3NwYW4+PzwvcD5gYGA8YnI+
aW5m4oieIDog4oSV4oiePGJyPnByZOKIniBpbmbiiJ4gPSBqdXN0IGluZuKInjxicj48YnI+dGVz
dCA6IElzLW5vdGhpbmcgKHByZOKIniAoaW5m4oieICriiJ4gemVyb+KInikpPGJyPnRlc3QgPSBu
b3RoaW5nPGJyPmBgYDxicj48cD5UaGUgYnVnIGlzIG5vdCB0aGF0IHRoZSBmaXJzdCBkZWZpbml0
aW9uIGlzIHJlamVjdGVkOyBpdCdzIHRoYXQgdGhlIHNlY29uZCBkZWZpbml0aW9uPHNwYW4gc3R5
bGU9ImZvbnQtc2l6ZToxMS4wcHQiPiBpcyBhY2NlcHRlZC4gSSBjYW4ndCByZWFsbHkgc2F5IHdo
eSBpdCdzIGFjY2VwdGVkLCB0aG91Z2guPC9zcGFuPjwvcD48cD48c3BhbiBzdHlsZT0iZm9udC1z
aXplOjExLjBwdCI+Q29uYXQgbXVsdGlwbGljYXRpb24gbmVlZHMgc29tZSBvdGhlciB0cmljayB0
byBtYWtlIGl0IHByb2R1Y3RpdmUuIEluIHRoZSB0ZXN0IGNhc2UsIGBuYCBpcyBhZGRlZCB0byBp
dHNlbGYgaW5maW5pdGVseSBtYW55IHRpbWVzLiBJZiBpdCdzIGEgc3VjY2Vzc29yLCB0aGF0J3Mg
b2theSBiZWNhdXNlIHRoZSBjb25zdW1lciBqdXN0IGdldHMgaW5maW5pdGVseSBtYW55IHN1Y2Nl
c3NvcnMuIEJ1dCBpZiBpdCdzIDAsIHRoZSBjb25zdW1lciBoYXMgdG8gd2FpdCAoZm9yZXZlcikg
YXMgdG8gd2hldGhlciB0aGUgcmVzdWx0IGlzIGEgemVybyBvciBhIHN1Y2Nlc3Nvci48YnI+PC9z
cGFuPjwvcD48cD48c3BhbiBzdHlsZT0iZm9udC1zaXplOjExLjBwdCI+UmVnYXJkcyw8L3NwYW4+
PC9wPjxwPjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij5KYW1lczxicj48L3NwYW4+PC9w
PjxkaXYgY2xhc3M9Im1vei1jaXRlLXByZWZpeCI+T24gMDMvMDMvMjAxOSAxMjoxNiwgVGhvcnN0
ZW4gQWx0ZW5raXJjaCB3cm90ZTo8YnI+PC9kaXY+PGJsb2NrcXVvdGUgdHlwZT0iY2l0ZSIgY2l0
ZT0ibWlkOjIwNjdBM0UxLUMxQUEtNDFGRC1CMDBBLTc3MzFCQTNCNEU0OUBub3R0aW5naGFtLmFj
LnVrIj4KPG1ldGEgaHR0cC1lcXVpdj0iQ29udGVudC1UeXBlIiBjb250ZW50PSJ0ZXh0L2h0bWw7
ICI+CjxtZXRhIG5hbWU9IkdlbmVyYXRvciIgY29udGVudD0iTWljcm9zb2Z0IFdvcmQgMTUgKGZp
bHRlcmVkIG1lZGl1bSkiPgo8c3R5bGU+PCEtLQovKiBGb250IERlZmluaXRpb25zICovCkBmb250
LWZhY2UKCXtmb250LWZhbWlseToiQ2FtYnJpYSBNYXRoIjsKCXBhbm9zZS0xOjIgNCA1IDMgNSA0
IDYgMyAyIDQ7fQpAZm9udC1mYWNlCgl7Zm9udC1mYW1pbHk6Q2FsaWJyaTsKCXBhbm9zZS0xOjIg
MTUgNSAyIDIgMiA0IDMgMiA0O30KLyogU3R5bGUgRGVmaW5pdGlvbnMgKi8KcC5Nc29Ob3JtYWws
IGxpLk1zb05vcm1hbCwgZGl2Lk1zb05vcm1hbAoJe21hcmdpbjowY207CgltYXJnaW4tYm90dG9t
Oi4wMDAxcHQ7Cglmb250LXNpemU6MTIuMHB0OwoJZm9udC1mYW1pbHk6IkNhbGlicmkiLHNhbnMt
c2VyaWY7fQphOmxpbmssIHNwYW4uTXNvSHlwZXJsaW5rCgl7bXNvLXN0eWxlLXByaW9yaXR5Ojk5
OwoJY29sb3I6IzA1NjNDMTsKCXRleHQtZGVjb3JhdGlvbjp1bmRlcmxpbmU7fQphOnZpc2l0ZWQs
IHNwYW4uTXNvSHlwZXJsaW5rRm9sbG93ZWQKCXttc28tc3R5bGUtcHJpb3JpdHk6OTk7Cgljb2xv
cjojOTU0RjcyOwoJdGV4dC1kZWNvcmF0aW9uOnVuZGVybGluZTt9CnNwYW4uRW1haWxTdHlsZTE3
Cgl7bXNvLXN0eWxlLXR5cGU6cGVyc29uYWwtY29tcG9zZTsKCWZvbnQtZmFtaWx5OiJDYWxpYnJp
IixzYW5zLXNlcmlmOwoJY29sb3I6d2luZG93dGV4dDt9Ci5Nc29DaHBEZWZhdWx0Cgl7bXNvLXN0
eWxlLXR5cGU6ZXhwb3J0LW9ubHk7Cglmb250LWZhbWlseToiQ2FsaWJyaSIsc2Fucy1zZXJpZjt9
CkBwYWdlIFdvcmRTZWN0aW9uMQoJe3NpemU6NjEyLjBwdCA3OTIuMHB0OwoJbWFyZ2luOjcyLjBw
dCA3Mi4wcHQgNzIuMHB0IDcyLjBwdDt9CmRpdi5Xb3JkU2VjdGlvbjEKCXtwYWdlOldvcmRTZWN0
aW9uMTt9Ci0tPjwvc3R5bGU+CgoKPGRpdiBjbGFzcz0iV29yZFNlY3Rpb24xIj4KPHAgY2xhc3M9
Ik1zb05vcm1hbCI+PHNwYW4gc3R5bGU9ImZvbnQtc2l6ZToxMS4wcHQiPkhpLDxvOnA+PC9vOnA+
PC9zcGFuPjwvcD4KPHAgY2xhc3M9Ik1zb05vcm1hbCI+PHNwYW4gc3R5bGU9ImZvbnQtc2l6ZTox
MS4wcHQiPjxvOnA+Jm5ic3A7PC9vOnA+PC9zcGFuPjwvcD4KPHAgY2xhc3M9Ik1zb05vcm1hbCI+
PHNwYW4gc3R5bGU9ImZvbnQtc2l6ZToxMS4wcHQiPkkganVzdCBzZXQgdGhlIGV4ZXJjaXNlIHRv
IGRlZmluZSBtdWx0aXBsaWNhdGlvbiBmb3IgY29uYXRzIGZvciBteSBjb3Vyc2Ugb24gdHlwZSB0
aGVvcnkuIFNvIHBsZWFzZSBkb27igJl0IGJsdXJ0IHB1dCB0aGUgc29sdXRpb24g4oCTIHNlZSB0
aGUgYXR0YWNoZWQgY29kZS4gVGhlIGZvbGxvd2luZyBpcyBub3QgYSBzb2x1dGlvbiBiZWNhdXNl
IGFnZGEgZG9lc27igJl0CiBzZWUgdGhhdCB0aGUgZGVmaW5pdGlvbiBpcyBwcm9kdWN0aXZlIChl
dmVuIHRob3VnaCBpdCBpcyk6PG86cD48L286cD48L3NwYW4+PC9wPgo8cCBjbGFzcz0iTXNvTm9y
bWFsIj48c3BhbiBzdHlsZT0iZm9udC1zaXplOjExLjBwdCI+PG86cD4mbmJzcDs8L286cD48L3Nw
YW4+PC9wPgo8cCBjbGFzcz0iTXNvTm9ybWFsIj48c3BhbiBzdHlsZT0iZm9udC1zaXplOjExLjBw
dCI+cHJk4oieIChtICriiJ4gbikgd2l0aCBwcmTiiJ4gbSZuYnNwOyZuYnNwOyZuYnNwOyZuYnNw
OyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZu
YnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNw
OyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZuYnNwOyZu
YnNwOyAmbmJzcDsmbmJzcDsmbmJzcDsmbmJzcDsmbmJzcDsmbmJzcDsmbmJzcDsmbmJzcDsmbmJz
cDsmbmJzcDsmbmJzcDs8bzpwPjwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwi
PjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij5wcmTiiJ4gKG0gKuKIniBuKSB8IChqdXN0
IHBtKSA9IHByZOKIniAobiAr4oieIChwbSAq4oieIG4pKTxvOnA+PC9vOnA+PC9zcGFuPjwvcD4K
PHAgY2xhc3M9Ik1zb05vcm1hbCI+PHNwYW4gc3R5bGU9ImZvbnQtc2l6ZToxMS4wcHQiPnByZOKI
niAobSAq4oieIG4pIHwgbm90aGluZyZuYnNwOyZuYnNwOyA9IG5vdGhpbmc8bzpwPjwvbzpwPjwv
c3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEu
MHB0Ij48bzpwPiZuYnNwOzwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxz
cGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij5idXQgYWZ0ZXIgdGhlIGZvbGxvd2luZyBjaGFu
Z2U8bzpwPjwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxl
PSJmb250LXNpemU6MTEuMHB0Ij48bzpwPiZuYnNwOzwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNz
PSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij5wcmTiiJ4gKG0gKuKI
niBuKSB3aXRoIHByZOKIniBtJm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5i
c3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7
Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5i
c3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7
Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Jm5ic3A7Cjxv
OnA+PC9vOnA+PC9zcGFuPjwvcD4KPHAgY2xhc3M9Ik1zb05vcm1hbCI+PHNwYW4gc3R5bGU9ImZv
bnQtc2l6ZToxMS4wcHQiPnByZOKIniAobSAq4oieIG4pIHwgKGp1c3QgcG0pIHdpdGggKHBtICri
iJ4gbik8bzpwPjwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0
eWxlPSJmb250LXNpemU6MTEuMHB0Ij5wcmTiiJ4gKG0gKuKIniBuKSB8IChqdXN0IHBtKSB8IHgg
PSBwcmTiiJ4gKG4gK+KIniB4KTxvOnA+PC9vOnA+PC9zcGFuPjwvcD4KPHAgY2xhc3M9Ik1zb05v
cm1hbCI+PHNwYW4gc3R5bGU9ImZvbnQtc2l6ZToxMS4wcHQiPnByZOKIniAobSAq4oieIG4pIHwg
bm90aGluZyZuYnNwOyZuYnNwOyA9IG5vdGhpbmc8bzpwPjwvbzpwPjwvc3Bhbj48L3A+CjxwIGNs
YXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij48bzpwPiZuYnNw
OzwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250
LXNpemU6MTEuMHB0Ij5hZ2RhIHNlZW1zIHRvIGFjY2VwdCBpcy4gQWN0dWFsbHkgZXZlbiBpZiAr
4oieIGlzIG5vdCBjb250cmFjdGl2ZS48bzpwPjwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJN
c29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij48bzpwPiZuYnNwOzwvbzpw
Pjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6
MTEuMHB0Ij5JcyB0aGlzIGEga25vd24gYnVnPyBPdGhlcndpc2UgY2FuIHNvbWVib2R5IHJlbWlu
ZCBlIGhvdyB0byByZXBvcnQgdGhpcz88bzpwPjwvbzpwPjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJN
c29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6MTEuMHB0Ij48bzpwPiZuYnNwOzwvbzpw
Pjwvc3Bhbj48L3A+CjxwIGNsYXNzPSJNc29Ob3JtYWwiPjxzcGFuIHN0eWxlPSJmb250LXNpemU6
MTEuMHB0Ij5DaGVlcnMsPG86cD48L286cD48L3NwYW4+PC9wPgo8cCBjbGFzcz0iTXNvTm9ybWFs
Ij48c3BhbiBzdHlsZT0iZm9udC1zaXplOjExLjBwdCI+VGhvcnN0ZW48bzpwPjwvbzpwPjwvc3Bh
bj48L3A+CjwvZGl2Pgo8cHJlPlRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGlu
dGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50
aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3NhZ2UgaW4gZXJy
b3IsIHBsZWFzZSBjb250YWN0IHRoZSBzZW5kZXIgYW5kIGRlbGV0ZSB0aGUgZW1haWwgYW5kCmF0
dGFjaG1lbnQuIAoKQW55IHZpZXdzIG9yIG9waW5pb25zIGV4cHJlc3NlZCBieSB0aGUgYXV0aG9y
IG9mIHRoaXMgZW1haWwgZG8gbm90Cm5lY2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9mIHRo
ZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0uIEVtYWlsCmNvbW11bmljYXRpb25zIHdpdGggdGhl
IFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRvcmVkIAp3aGVyZSBwZXJtaXR0
ZWQgYnkgbGF3LgoKCgo8L3ByZT4KCjxicj48ZmllbGRzZXQgY2xhc3M9Im1pbWVBdHRhY2htZW50
SGVhZGVyIj48L2ZpZWxkc2V0PjxwcmUgY2xhc3M9Im1vei1xdW90ZS1wcmUiIHdyYXA9IiI+X19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KQWdkYSBtYWlsaW5n
IGxpc3QKQWdkYUBsaXN0cy5jaGFsbWVycy5zZQpodHRwczovL2xpc3RzLmNoYWxtZXJzLnNlL21h
aWxtYW4vbGlzdGluZm8vYWdkYQo8L3ByZT4KCjwvYmxvY2txdW90ZT4="
style="height:0;width:0;max-height:0;max-width:0;overflow:hidden;font-size:0em;padding:0;margin:0;"></div>
</div>
</body>
</html>