
<html><body>

<p><tt>Looks my previous e-mail in html style isn't showing properlly in PoplMark archive, so here is another copy, hope better. I also rechecked mentioned Benjamin's paper and for me it looks exactly same case as described in challenge documentation.<br>

</tt><br>

<tt>Regarding third challenge: is there available some paper proof of decidability of mentioned relations?<br>

</tt><tt>It looks to be not trivial at all, especially taking into account negative result on decidability of subtyping relation<br>

</tt><tt>for Fsub ( <a href="http://citeseer.ist.psu.edu/pierce93bounded.html">http://citeseer.ist.psu.edu/pierce93bounded.html</a> , by Benjamin Pierce,which is one of PoplMark challenge authors).<br>

</tt><tt>Does same result is valid also for the calculus described in the challenge problems?<br>

</tt><tt>As for AlphaProlog solution suggested by Matthew Fairbairn, there is related question: is there a proof that<br>

</tt><tt>used AlphaProlog algorithms always terminates?<br>

</tt><tt>Thanks in advance for any highlighting information.</tt><br>

<tt>Regards, </tt><br>

<tt>Jevgenijs.</tt></body></html>