> Interesting! What *is* this problem? > If it's tiny, it should be shown (here, and in Jürgen's talk). It is an encoding of Ackermann’s function using an explicit stack. Larry presented it at this years Isabelle workshop (including a termination proof) and asked me to submit it as TRS to TPDB. Best, René