Re: HHH(DD) does correctly reject its input as non-halting --- VERIFIED FACT

On 2025-06-12 15:30:05 +0000, olcott said:

int DD()
{
   int Halt_Status = HHH(DD);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}
 It is a verified fact that DD() *is* one of the forms
of the counter-example input as such an input would
be encoded in C. Christopher Strachey wrote his in CPL.
 // rec routine P
//   §L :if T[P] go to L
//     Return §
// https://academic.oup.com/comjnl/article/7/4/313/354243
void Strachey_P()
{
   L: if (HHH(Strachey_P)) goto L;
   return;
}
 https://academic.oup.com/comjnl/article-abstract/7/4/313/354243?redirectedFrom=fulltext 

Strachey only informally presents the idea of the proof. Formalism
and details needed in a rigorous proof is not shown.

It *is* a verified fact DD correctly simulated by HHH
cannot possibly reach its own "return" statement
final halt state.

That "cannot possibly" is not a part of any verifiable fact as
it is not sufficiently well-defined for a verification. What
cannot be stated cearly and unambiguoulsy cannot be a verified
fact.
--
Mikko