<FONT face="Default Sans Serif,Verdana,Arial,Helvetica,sans-serif" size=2><div>Regarding third challenge: is there available some paper proof of decidability of mentioned relations?<BR>It looks to be not trivial at all, especially taking into account negative result on decidability of subtyping relation<BR>for Fsub (<A href="http://citeseer.ist.psu.edu/pierce93bounded.html" target=blank>http://citeseer.ist.psu.edu/pierce93bounded.html</A>, by Benjamin Pierce,which is one of PoplMark challenge authors). <BR>Does same result is valid also for the calculus described in the challenge problems? <BR>As for AlphaProlog solution suggested by Matthew Fairbairn, there is related question: is there a proof that <BR>used AlphaProlog algorithms always terminates?<BR>Thanks in advance for any highlighting information. <BR>Regards,<BR>Jevgenijs.<BR></div></FONT>