the MPTC Dilemma (please solve)

[Ross Paterson]

On Tue, Feb 21, 2006 at 03:50:52PM +0800, Martin Sulzmann wrote:
> A depth limit is not enough. For confluence we need that *all*
> derivations for a particular goal terminate. Once we have
> confluence we get completeness of the inference checks.

So without a static test for termination (though just for this goal),
we're still in the no-man's land between proof and counterexample.
Reduction might be confluent, but we have no proof.